En ℝ, si x ≤ y, entonces y ≰ x ↔ x ≠ y
Demostrar con Lean4 que si \(x\) e \(y\) son números reales tales que \(x ≤ y\), entonces \(y ≰ x ↔ x ≠ y\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by sorry |
Demostración en lenguaje natural
Para demostrar la equivalencia, demostraremos cada una de las implicaciones.
Para demostrar la primera, supongamos que \(y ≰ x\) y que \(x = y\). Entonces, \(y ≤ x\) que es una contradicción.
Para demostrar la segunda, supongamos que \(x ≠ y\) y que \(y ≤ x\). Entonces, por la hipótesis y la antisimetría, se tiene que \(x = y\) lo que es una contradicción.
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . show ¬y ≤ x → x ≠ y { intro h1 -- h1 : ¬y ≤ x -- ⊢ x ≠ y intro h2 -- h2 : x = y -- ⊢ False have h3 : y ≤ x := by rw [h2] show False exact h1 h3 } . show x ≠ y → ¬y ≤ x { intro h1 -- h1 : x ≠ y -- ⊢ ¬y ≤ x intro h2 -- h2 : y ≤ x -- ⊢ False have h3 : x = y := le_antisymm h h2 show False exact h1 h3 } -- 2ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . show ¬y ≤ x → x ≠ y { intro h1 -- h1 : ¬y ≤ x -- ⊢ x ≠ y intro h2 -- h2 : x = y -- ⊢ False show False exact h1 (by rw [h2]) } . show x ≠ y → ¬y ≤ x { intro h1 -- h1 : x ≠ y -- ⊢ ¬y ≤ x intro h2 -- h2 : y ≤ x -- ⊢ False show False exact h1 (le_antisymm h h2) } -- 3ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . show ¬y ≤ x → x ≠ y { intro h1 h2 exact h1 (by rw [h2]) } . show x ≠ y → ¬y ≤ x { intro h1 h2 exact h1 (le_antisymm h h2) } -- 4ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . intro h1 h2 exact h1 (by rw [h2]) . intro h1 h2 exact h1 (le_antisymm h h2) -- 5ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . exact fun h1 h2 ↦ h1 (by rw [h2]) . exact fun h1 h2 ↦ h1 (le_antisymm h h2) -- 6ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := ⟨fun h1 h2 ↦ h1 (by rw [h2]), fun h1 h2 ↦ h1 (le_antisymm h h2)⟩ -- 7ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . show ¬y ≤ x → x ≠ y { intro h1 -- h1 : ¬y ≤ x -- ⊢ x ≠ y contrapose! h1 -- h1 : x = y -- ⊢ y ≤ x calc y = x := h1.symm _ ≤ x := by rfl } . show x ≠ y → ¬y ≤ x { intro h2 -- h2 : x ≠ y -- ⊢ ¬y ≤ x contrapose! h2 -- h2 : y ≤ x -- ⊢ x = y show x = y exact le_antisymm h h2 } -- 8ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor · -- ⊢ ¬y ≤ x → x ≠ y contrapose! -- ⊢ x = y → y ≤ x rintro rfl -- ⊢ x ≤ x rfl . -- ⊢ x ≠ y → ¬y ≤ x contrapose! -- ⊢ y ≤ x → x = y exact le_antisymm h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
