Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y
Demostrar con Lean4 que si \(x, y ∈ ℝ\) tales que \((∀ z)[y < z → x ≤ z]\), entonces \(x ≤ y\).
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : ∀ z, y < z → x ≤ z) : x ≤ y := by sorry |
1. Demostración en lenguaje natural
Lo demostraremos por reducción al absurdo. Para ello, supongamos que
\[ x ≰ y \]
Entonces
\[ y < x \]
y, por la densidad de \(ℝ\), existe un \(a\) tal que
\[ y < a < x \]
Puesto que \(y < a\), por la hipótesis, se tiene que
\[ x ≤ a \]
en contradicción con
\[ a < x \]
2. 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 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : ∀ z, y < z → x ≤ z) : x ≤ y := by by_contra h1 -- h1 : ¬x ≤ y -- ⊢ False have hxy : x > y := not_le.mp h1 -- ⊢ ¬x > y cases' (exists_between hxy) with a ha -- a : ℝ -- ha : y < a ∧ a < x apply (lt_irrefl a) -- ⊢ a < a calc a < x := ha.2 _ ≤ a := h a ha.1 -- 2ª demostración -- =============== example (h : ∀ z, y < z → x ≤ z) : x ≤ y := by apply le_of_not_gt -- ⊢ ¬x > y intro hxy -- hxy : x > y -- ⊢ False cases' (exists_between hxy) with a ha -- a : ℝ -- ha : y < a ∧ a < x apply (lt_irrefl a) -- ⊢ a < a calc a < x := ha.2 _ ≤ a := h a ha.1 -- 3ª demostración -- =============== example (h : ∀ z, y < z → x ≤ z) : x ≤ y := by apply le_of_not_gt -- ⊢ ¬x > y intro hxy -- hxy : x > y -- ⊢ False cases' (exists_between hxy) with a ha -- ha : y < a ∧ a < x apply (lt_irrefl a) -- ⊢ a < a exact lt_of_lt_of_le ha.2 (h a ha.1) -- 4ª demostración -- =============== example (h : ∀ z, y < z → x ≤ z) : x ≤ y := by apply le_of_not_gt -- ⊢ ¬x > y intro hxy -- hxy : x > y -- ⊢ False cases' (exists_between hxy) with a ha -- a : ℝ -- ha : y < a ∧ a < x exact (lt_irrefl a) (lt_of_lt_of_le ha.2 (h a ha.1)) -- 5ª demostración -- =============== example (h : ∀ z, y < z → x ≤ z) : x ≤ y := by apply le_of_not_gt -- ⊢ ¬x > y intro hxy -- hxy : x > y -- ⊢ False rcases (exists_between hxy) with ⟨a, hya, hax⟩ -- a : ℝ -- hya : y < a -- hax : a < x exact (lt_irrefl a) (lt_of_lt_of_le hax (h a hya)) -- 6ª demostración -- =============== example (h : ∀ z, y < z → x ≤ z) : x ≤ y := le_of_forall_le_of_dense h -- Lemas usados -- ============ -- variable (z : ℝ) -- #check (exists_between : x < y → ∃ z, x < z ∧ z < y) -- #check (le_of_forall_le_of_dense : (∀ z, y < z → x ≤ z) → x ≤ y) -- #check (le_of_not_gt : ¬x > y → x ≤ y) -- #check (lt_irrefl x : ¬x < x) -- #check (lt_of_lt_of_le : x < y → y ≤ z → x < z) -- #check (not_le : ¬x ≤ y ↔ y < x) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
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 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 |
theory Propiedad_de_la_densidad_de_los_reales imports Main HOL.Real begin (* 1ª demostración *) lemma fixes x y :: real assumes "∀ z. y < z ⟶ x ≤ z" shows "x ≤ y" proof (rule linorder_class.leI; intro notI) assume "y < x" then have "∃z. y < z ∧ z < x" by (rule dense) then obtain a where ha : "y < a ∧ a < x" by (rule exE) have "¬ a < a" by (rule order.irrefl) moreover have "a < a" proof - have "y < a ⟶ x ≤ a" using assms by (rule allE) moreover have "y < a" using ha by (rule conjunct1) ultimately have "x ≤ a" by (rule mp) moreover have "a < x" using ha by (rule conjunct2) ultimately show "a < a" by (simp only: less_le_trans) qed ultimately show False by (rule notE) qed (* 2ª demostración *) lemma fixes x y :: real assumes "⋀ z. y < z ⟹ x ≤ z" shows "x ≤ y" proof (rule linorder_class.leI; intro notI) assume "y < x" then have "∃z. y < z ∧ z < x" by (rule dense) then obtain a where hya : "y < a" and hax : "a < x" by auto have "¬ a < a" by (rule order.irrefl) moreover have "a < a" proof - have "a < x" using hax . also have "… ≤ a" using assms[OF hya] . finally show "a < a" . qed ultimately show False by (rule notE) qed (* 3ª demostración *) lemma fixes x y :: real assumes "⋀ z. y < z ⟹ x ≤ z" shows "x ≤ y" proof (rule linorder_class.leI; intro notI) assume "y < x" then have "∃z. y < z ∧ z < x" by (rule dense) then obtain a where hya : "y < a" and hax : "a < x" by auto have "¬ a < a" by (rule order.irrefl) moreover have "a < a" using hax assms[OF hya] by (rule less_le_trans) ultimately show False by (rule notE) qed (* 4ª demostración *) lemma fixes x y :: real assumes "⋀ z. y < z ⟹ x ≤ z" shows "x ≤ y" by (meson assms dense not_less) (* 5ª demostración *) lemma fixes x y :: real assumes "⋀ z. y < z ⟹ x ≤ z" shows "x ≤ y" using assms by (rule dense_ge) (* 6ª demostración *) lemma fixes x y :: real assumes "∀ z. y < z ⟶ x ≤ z" shows "x ≤ y" using assms by (simp only: dense_ge) end |