Si f no es monótona, entonces ∃x∃y[x ≤ y ∧ f(y) < f(x)]
Demostrar con Lean4 que si \(f\) no es monótona, entonces \(∃x∃y[x ≤ y ∧ f(y) < f(x)]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable (f : ℝ → ℝ) example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by sorry |
Demostración en lenguaje natural
Usaremos los siguientes lemas:
\begin{align}
&¬(∀x)P(x) ↔ (∃ x)¬P(x) \tag{L1} \\
&¬(p → q) ↔ p ∧ ¬q \tag{L2} \\
&(∀a, b ∈ ℝ)[¬b ≤ a → a < b] \tag{L3}
\end{align}
Por la definición de función monótona,
\[ ¬(∀x)(∀y)[x ≤ y → f(x) ≤ f(y)] \]
Aplicando L1 se tiene
\[ (∃x)¬(∀y)[x ≤ y → f(x) ≤ f(y)] \]
Sea \(a\) tal que
\[ ¬(∀y)[a ≤ y → f(a) ≤ f(y)] \]
Aplicando L1 se tiene
\[ (∃y)¬[a ≤ y → f(a) ≤ f(y)] \]
Sea \(b\) tal que
\[ ¬[a ≤ b → f(a) ≤ f(b)] \]
Aplicando L2 se tiene que
\[ a ≤ b ∧ ¬(f(a) ≤ f(b)) \]
Aplicando L3 se tiene que
\[ a ≤ b ∧ f(b) < f(a) \]
Por tanto,
\[ (∃x,y)[x ≤ y ∧ f(y) < f(x)] \]
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 |
import Mathlib.Tactic variable (f : ℝ → ℝ) -- 1ª demostración -- =============== example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by have h1 : ¬∀ x y, x ≤ y → f x ≤ f y := h have h2 : ∃ x, ¬(∀ y, x ≤ y → f x ≤ f y) := not_forall.mp h1 rcases h2 with ⟨a, ha : ¬∀ y, a ≤ y → f a ≤ f y⟩ have h3 : ∃ y, ¬(a ≤ y → f a ≤ f y) := not_forall.mp ha rcases h3 with ⟨b, hb : ¬(a ≤ b → f a ≤ f b)⟩ have h4 : a ≤ b ∧ ¬(f a ≤ f b) := not_imp.mp hb have h5 : a ≤ b ∧ f b < f a := ⟨h4.1, lt_of_not_le h4.2⟩ use a, b -- ⊢ a ≤ b ∧ f b < f a exact h5 -- 2ª demostración -- =============== example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by simp only [Monotone] at h -- h : ¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b push_neg at h -- h : Exists fun ⦃a⦄ => Exists fun ⦃b⦄ => a ≤ b ∧ f b < f a exact h -- Lemas usados -- ============ -- variable {α : Type _} -- variable (P : α → Prop) -- variable (p q : Prop) -- variable (a b : ℝ) -- #check (not_forall : (¬∀ x, P x) ↔ ∃ x, ¬P x) -- #check (not_imp : ¬(p → q) ↔ p ∧ ¬q) -- #check (lt_of_not_le : ¬b ≤ a → a < b) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 34.
