f: ℝ → ℝ no es monótona syss (∃x,y)[x ≤ y ∧ f(x) > f(y)]
Demostrar con Lean4 que \(f: ℝ → ℝ\) no es monótona syss \((∃x,y)[x ≤ y ∧ f(x) > f(y)]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de equivalencias:
\begin{align}
f \text{ es no monótona } & ↔ ¬(∀ x, y)[x ≤ y → f(x) ≤ f(y)] \\
& ↔ (∃ x, y)[x ≤ y ∧ f(x) > f(y)]
\end{align}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 |
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} -- 1ª demostración -- =============== example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := calc ¬Monotone f ↔ ¬∀ x y, x ≤ y → f x ≤ f y := by rw [Monotone] _ ↔ ∃ x y, x ≤ y ∧ f y < f x := by simp_all only [not_forall, not_le, exists_prop] _ ↔ ∃ x y, x ≤ y ∧ f x > f y := by rfl -- 2ª demostración -- =============== example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := calc ¬Monotone f ↔ ¬∀ x y, x ≤ y → f x ≤ f y := by rw [Monotone] _ ↔ ∃ x y, x ≤ y ∧ f x > f y := by aesop -- 3ª demostración -- =============== example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by rw [Monotone] -- ⊢ (¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b) ↔ ∃ x y, x ≤ y ∧ f x > f y push_neg -- ⊢ (Exists fun ⦃a⦄ => Exists fun ⦃b⦄ => a ≤ b ∧ f b < f a) ↔ ∃ x y, x ≤ y ∧ f x > f y rfl -- 4ª demostración -- =============== lemma not_Monotone_iff : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by rw [Monotone] -- ⊢ (¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b) ↔ ∃ x y, x ≤ y ∧ f x > f y aesop |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
