En ℝ, x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x
Demostrar con Lean4 que. en \(ℝ\), \(x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by sorry |
Demostración en lenguaje natural
Supongamos que
\begin{align}
x ≤ y \tag{1} \\
x ≠ y \tag{2}
\end{align}
Entonces, se tiene \(x ≤ y\) (por (1)) y, para probar \(y ≰ x\), supongamos que
\[ y ≤ x \tag{3}\]
Aplicando la propiedad antimétrica a (1) y (3), se obtiene que \(x = y\), en contradicción con (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 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) -- 1ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1 : x ≤ y, h2 : x ≠ y⟩ constructor . show x ≤ y exact h1 . show ¬ y ≤ x rintro h3 : y ≤ x -- ⊢ False have h4 : x = y := le_antisymm h1 h3 show False exact h2 h4 -- 2ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1 : x ≤ y, h2 : x ≠ y⟩ -- ⊢ x ≤ y ∧ ¬y ≤ x constructor . show x ≤ y exact h1 . show ¬ y ≤ x rintro h3 : y ≤ x -- ⊢ False show False exact h2 (le_antisymm h1 h3) -- 3ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1 : x ≤ y, h2 : x ≠ y⟩ constructor . show x ≤ y exact h1 . show ¬ y ≤ x exact fun h3 ↦ h2 (le_antisymm h1 h3) -- 4ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1, h2⟩ exact ⟨h1, fun h3 ↦ h2 (le_antisymm h1 h3)⟩ -- 5ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := fun ⟨h1, h2⟩ ↦ ⟨h1, fun h3 ↦ h2 (le_antisymm h1 h3)⟩ -- 6ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1 : x ≤ y, h2 : x ≠ y⟩ use h1 exact fun h3 ↦ h2 (le_antisymm h1 h3) -- 7ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1, h2⟩ -- h1 : x ≤ y -- h2 : x ≠ y -- ⊢ x ≤ y ∧ ¬y ≤ x use h1 -- ¬y ≤ x contrapose! h2 -- h2 : y ≤ x -- ⊢ x = y apply le_antisymm h1 h2 -- Lemas usados -- ============ -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
