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:
|
|
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:
¬(∀x)P(x)↔(∃x)¬P(x)¬(p→q)↔p∧¬q(∀a,b∈ℝ)[¬b≤a→a<b]
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
