{x ≤ y, y ≰ x} ⊢ x ≤ y ∧ x ≠ y
Demostrar con Lean4 que
\[\{x ≤ y, y ≰ x\} ⊢ x ≤ y ∧ x ≠ y\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by sorry |
Demostración en lenguaje natural
Como la conclusión es una conjunción, tenemos que desmostrar sus partes. La primera parte (\(x ≤ y\)) coincide con la hipótesis. Para demostrar la segunda parte (\(x ≠ y\)), supongamos que \(x = y\); entonces \(y ≤ x\) en contradicción con la segunda 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 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by constructor . -- ⊢ x ≤ y exact h1 . -- ⊢ x ≠ y intro h3 -- h3 : x = y -- ⊢ False have h4 : y ≤ x := h3.symm.le show False exact h2 h4 -- 2ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by constructor . -- ⊢ x ≤ y exact h1 . -- ⊢ x ≠ y intro h3 -- h3 : x = y -- ⊢ False exact h2 (h3.symm.le) -- 3ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := ⟨h1, fun h3 ↦ h2 (h3.symm.le)⟩ -- 4ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by constructor . -- ⊢ x ≤ y exact h1 . -- ⊢ x ≠ y intro h3 -- h3 : x = y -- ⊢ False apply h2 -- ⊢ y ≤ x rw [h3] -- 5ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by constructor . -- ⊢ x ≤ y exact h1 . -- ⊢ x ≠ y intro h3 -- h3 : x = y -- ⊢ False exact h2 (by rw [h3]) -- 6ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := ⟨h1, fun h ↦ h2 (by rw [h])⟩ -- 7ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := by have h3 : x ≠ y . contrapose! h2 -- ⊢ y ≤ x rw [h2] exact ⟨h1, h3⟩ -- 8ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := by aesop |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 35.
