En los retículos, x ⊓ (x ⊔ y) = x
Demostrar con Lean4 que en los retículos se verifica que
\[ x ⊓ (x ⊔ y) = x \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y : α) example : x ⊓ (x ⊔ y) = x := by sorry |
Demostración en lenguaje natural
En la demostración se usarán los siguientes lemas
\begin{align}
&x ≤ y → y ≤ x → x = y \tag{L1} \\
&x ⊓ y ≤ x \tag{L2} \\
&z ≤ x → z ≤ y → z ≤ x ⊓ y \tag{L3} \\
&x ≤ x \tag{L4} \\
&x ≤ x ⊔ y \tag{L5} \\
\end{align}
Por L1, basta demostrar las siguientes relaciones:
\begin{align}
&x ⊓ (x ⊔ y) ≤ x \tag{1} \\
&x ≤ x ⊓ (x ⊔ y) \tag{2}
\end{align}
La (1) se tiene por L2.
Para demostrar la (2), por L3, basta probar las relaciones:
\begin{align}
x &≤ x \tag{2a} \\
x &≤ x ⊔ y \tag{2b}
\end{align}
La (2a) se tiene por L4.
La (2b) se tiene por L5
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 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y : α) -- 1ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := by have h1 : x ⊓ (x ⊔ y) ≤ x := inf_le_left have h2 : x ≤ x ⊓ (x ⊔ y) { have h2a : x ≤ x := le_rfl have h2b : x ≤ x ⊔ y := le_sup_left show x ≤ x ⊓ (x ⊔ y) exact le_inf h2a h2b } show x ⊓ (x ⊔ y) = x exact le_antisymm h1 h2 -- 2ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := by have h1 : x ⊓ (x ⊔ y) ≤ x := by simp have h2 : x ≤ x ⊓ (x ⊔ y) := by simp show x ⊓ (x ⊔ y) = x exact le_antisymm h1 h2 -- 3ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := by apply le_antisymm . -- x ⊓ (x ⊔ y) ≤ x apply inf_le_left . -- x ≤ x ⊓ (x ⊔ y) apply le_inf . -- x ≤ x apply le_rfl . -- x ≤ x ⊔ y apply le_sup_left -- 4ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := le_antisymm inf_le_left (le_inf le_rfl le_sup_left) -- 5ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := -- by apply? inf_sup_self -- 6ª demostración -- =============== example : x ⊓ (x ⊔ y) = x := by simp -- Lemas usados -- ============ -- variable (z : α) -- #check (inf_le_left : x ⊓ y ≤ x) -- #check (inf_sup_self : x ⊓ (x ⊔ y) = x) -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y) -- #check (le_rfl : x ≤ x) -- #check (le_sup_left : 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. 21.
