Si R es un retículo y x, y ∈ R, entonces x ⊔ (x ⊓ y) = x
Demostrar que si R es un retículo y x, y ∈ R, entonces
1 |
x ⊔ (x ⊓ y) = x |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 |
import order.lattice variables {R : Type*} [lattice R] variables x y : R example : x ⊔ (x ⊓ y) = x := sorry |
Soluciones con Lean
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 |
import order.lattice variables {R : Type*} [lattice R] variables x y : R -- 1ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := begin have h1 : x ⊔ (x ⊓ y) ≤ x, finish, have h2 : x ≤ x ⊔ (x ⊓ y), finish, show x ⊔ (x ⊓ y) = x, by exact le_antisymm h1 h2, end -- 2ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := begin have h1 : x ⊔ (x ⊓ y) ≤ x, { have h1a : x ≤ x := le_rfl, have h1b : x ⊓ y ≤ x := inf_le_left, show x ⊔ (x ⊓ y) ≤ x, by exact sup_le h1a h1b, }, have h2 : x ≤ x ⊔ (x ⊓ y) := le_sup_left, show x ⊔ (x ⊓ y) = x, by exact le_antisymm h1 h2, end -- 3ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := begin apply le_antisymm, { apply sup_le, { apply le_refl }, { apply inf_le_left }}, { apply le_sup_left }, end -- 4ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := -- by library_search sup_inf_self -- 4ª demostración -- =============== example : x ⊔ (x ⊓ y) = x := -- by hint by simp |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 22.