En los órdenes parciales, a < b ↔ a ≤ b ∧ a ≠ b
Demostrar con Lean4 que en los órdenes parciales,
\[a < b ↔ a ≤ b ∧ a ≠ b\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (a b : α) example : a < b ↔ a ≤ b ∧ a ≠ b := by sorry |
Demostración en lenguaje natural
Usaremos los siguientes lemas
\begin{align}
&(∀ a, b)[a < b ↔ a ≤ b ∧ b ≰ a] \tag{L1} \\
&(∀ a, b)[a ≤ b → b ≤ a → a = b] \tag{L2}
\end{align}
Por el lema L1, lo que tenemos que demostrar es
\[ a ≤ b ∧ b ≰ a ↔ a ≤ b ∧ a ≠ b \]
Lo haremos demostrando las dos implicaciones.
(⇒) Supongamos que \(a ≤ b\) y \(b ≰ a\). Tenemos que demostrar que \(a ≠ b\). Lo haremos por reducción al absurdo. Para ello, supongamos que \(a = b\). Entonces, \(b ≤ a\) que es una contradicicción con \(b ≰ a\).
(⇐) Supongamos que \(a ≤ b\) y \(a ≠ b\). Tenemos que demostrar que \(b ≰ a\). Lo haremos por reducción al absurdo. Para ello, supongamos que \(b ≤ a\). Entonces, junto con \(a ≤ b\), se tiene que \(a = b\) que es una contradicicción con \(a ≠ b\).
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 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 |
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (a b : α) -- 1ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b rintro ⟨h1 : a ≤ b, h2 : ¬b ≤ a⟩ -- ⊢ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b exact h1 . -- ⊢ a ≠ b rintro (h3 : a = b) -- ⊢ False have h4: b = a := h3.symm have h5: b ≤ a := le_of_eq h4 show False exact h2 h5 . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a rintro ⟨h5 : a ≤ b , h6 : a ≠ b⟩ -- ⊢ a ≤ b ∧ ¬b ≤ a constructor . -- ⊢ a ≤ b exact h5 . -- ⊢ ¬b ≤ a rintro (h7 : b ≤ a) have h8 : a = b := le_antisymm h5 h7 show False exact h6 h8 -- 2ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b rintro ⟨h1 : a ≤ b, h2 : ¬b ≤ a⟩ -- ⊢ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b exact h1 . -- ⊢ a ≠ b rintro (h3 : a = b) -- ⊢ False exact h2 (le_of_eq h3.symm) . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a rintro ⟨h4 : a ≤ b , h5 : a ≠ b⟩ -- ⊢ a ≤ b ∧ ¬b ≤ a constructor . -- ⊢ a ≤ b exact h4 . -- ⊢ ¬b ≤ a rintro (h6 : b ≤ a) exact h5 (le_antisymm h4 h6) -- 3ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b rintro ⟨h1 : a ≤ b, h2 : ¬b ≤ a⟩ -- ⊢ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b exact h1 . -- ⊢ a ≠ b exact fun h3 ↦ h2 (le_of_eq h3.symm) . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a rintro ⟨h4 : a ≤ b , h5 : a ≠ b⟩ -- ⊢ a ≤ b ∧ ¬b ≤ a constructor . -- ⊢ a ≤ b exact h4 . -- ⊢ ¬b ≤ a exact fun h6 ↦ h5 (le_antisymm h4 h6) -- 4ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b rintro ⟨h1 : a ≤ b, h2 : ¬b ≤ a⟩ -- ⊢ a ≤ b ∧ a ≠ b exact ⟨h1, fun h3 ↦ h2 (le_of_eq h3.symm)⟩ . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a rintro ⟨h4 : a ≤ b , h5 : a ≠ b⟩ -- ⊢ a ≤ b ∧ ¬b ≤ a exact ⟨h4, fun h6 ↦ h5 (le_antisymm h4 h6)⟩ -- 5ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b exact fun ⟨h1, h2⟩ ↦ ⟨h1, fun h3 ↦ h2 (le_of_eq h3.symm)⟩ . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a exact fun ⟨h4, h5⟩ ↦ ⟨h4, fun h6 ↦ h5 (le_antisymm h4 h6)⟩ -- 6ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b exact ⟨fun ⟨h1, h2⟩ ↦ ⟨h1, fun h3 ↦ h2 (le_of_eq h3.symm)⟩, fun ⟨h4, h5⟩ ↦ ⟨h4, fun h6 ↦ h5 (le_antisymm h4 h6)⟩⟩ -- 7ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by constructor . -- ⊢ a < b → a ≤ b ∧ a ≠ b intro h -- h : a < b -- ⊢ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b exact le_of_lt h . -- ⊢ a ≠ b exact ne_of_lt h . -- ⊢ a ≤ b ∧ a ≠ b → a < b rintro ⟨h1, h2⟩ -- h1 : a ≤ b -- h2 : a ≠ b -- ⊢ a < b exact lt_of_le_of_ne h1 h2 -- 8ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := ⟨fun h ↦ ⟨le_of_lt h, ne_of_lt h⟩, fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h1 h2⟩ -- 9ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := lt_iff_le_and_ne -- Lemas usados -- ============ -- #check (le_antisymm : a ≤ b → b ≤ a → a = b) -- #check (le_of_eq : a = b → a ≤ b) -- #check (lt_iff_le_and_ne : a < b ↔ a ≤ b ∧ a ≠ b) -- #check (lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a) -- #check (lt_of_le_of_ne : a ≤ b → a ≠ b → 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. 37.
