x ≤ y ∧ x ≠ y ⊢ y ≰ x
Demostrar con Lean4 que
\[x ≤ y ∧ x ≠ y ⊢ y ≰ x\]
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 : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by sorry |
Demostración en lenguaje natural
Supongamos que \(y ≤ x\). Entonces, por la antisimetría y la primera parte de la hipótesis, se tiene que \(x = y\) que contradice la segunda parte de la hipótesis.
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by intro h1 cases' h with h2 h3 -- h2 : x ≤ y -- h3 : x ≠ y have h4 : x = y := le_antisymm h2 h1 show False exact h3 h4 -- 2ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by intro h1 have h4 : x = y := le_antisymm h.1 h1 show False exact h.2 h4 -- 3ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by intro h1 show False exact h.2 (le_antisymm h.1 h1) -- 4ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := fun h1 ↦ h.2 (le_antisymm h.1 h1) -- 5ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by intro h' -- h' : y ≤ x -- ⊢ False apply h.right -- ⊢ x = y exact le_antisymm h.left h' -- 6ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by cases' h with h1 h2 -- h1 : x ≤ y -- h2 : x ≠ y contrapose! h2 -- h2 : y ≤ x -- ⊢ x = y exact le_antisymm h1 h2 -- 7ª demostración -- =============== example : x ≤ y ∧ x ≠ y → ¬ y ≤ x := by rintro ⟨h1, h2⟩ h' -- h1 : x ≤ y -- h2 : x ≠ y -- h' : y ≤ x -- ⊢ False exact h2 (le_antisymm h1 h') -- 8ª demostración -- =============== example : x ≤ y ∧ x ≠ y → ¬ y ≤ x := fun ⟨h1, h2⟩ h' ↦ h2 (le_antisymm h1 h') -- 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. 35.
