DAO: La semana en Calculemus (21 de octubre de 2022)
Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:
- 1. Si R es un retículo y x, y ∈ R, entonces x ⊔ y = y ⊔ x
- 2. Si R es un retículo y x, y, z ∈ R, entonces (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)
- 3. Si R es un retículo y x, y, z ∈ R, entonces (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)
- 4. Si R es un retículo y x, y ∈ R, entonces x ⊓ (x ⊔ y) = x
- 5. Si R es un retículo y x, y ∈ R, entonces x ⊔ (x ⊓ y) = x
A continuación se muestran las soluciones.
1. Si R es un retículo y x, y ∈ R, entonces x ⊔ y = y ⊔ x
Demostrar que si R es un retículo y x, y ∈ R, entonces x ⊔ y = y ⊔ x.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] variables x y : R example : x ⊔ y = 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 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 |
import order.lattice variables {R : Type*} [lattice R] variables x y : R -- 1ª demostración -- =============== lemma aux1 : x ⊔ y ≤ y ⊔ x := begin have h1 : x ≤ y ⊔ x, by exact le_sup_right, have h2 : y ≤ y ⊔ x, by exact le_sup_left, show x ⊔ y ≤ y ⊔ x, by exact sup_le h1 h2, end example : x ⊔ y = y ⊔ x := begin have h1 : x ⊔ y ≤ y ⊔ x, by exact aux1 x y, have h2 : y ⊔ x ≤ x ⊔ y, by exact aux1 y x, show x ⊔ y = y ⊔ x, by exact le_antisymm h1 h2, end -- 2ª demostración -- =============== lemma aux2 : x ⊔ y ≤ y ⊔ x := sup_le le_sup_right le_sup_left example : x ⊔ y = y ⊔ x := le_antisymm (aux2 x y) (aux2 y x) -- 3ª demostración -- =============== lemma aux : x ⊔ y ≤ y ⊔ x := begin apply sup_le, apply le_sup_right, apply le_sup_left, end example : x ⊔ y = y ⊔ x := begin apply le_antisymm, apply aux, apply aux, end -- 4ª demostración -- =============== example : x ⊔ y = y ⊔ x := by apply le_antisymm; simp -- 5ª demostración -- =============== example : x ⊔ y = y ⊔ x := -- by library_search sup_comm -- 6ª demostración -- =============== example : x ⊔ y = y ⊔ x := -- by hint by finish |
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.
2. Si R es un retículo y x, y, z ∈ R, entonces (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)
Demostrar que si R es un retículo y x, y, z ∈ R, entonces
|
1 |
(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] variables x y z : R example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := 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 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 |
import order.lattice variables {R : Type*} [lattice R] variables x y z : R -- 1ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := begin have h1 : (x ⊓ y) ⊓ z ≤ x ⊓ (y ⊓ z), { have h1a : (x ⊓ y) ⊓ z ≤ x, calc (x ⊓ y) ⊓ z ≤ x ⊓ y : inf_le_left ... ≤ x : inf_le_left, have h1b : (x ⊓ y) ⊓ z ≤ y ⊓ z, { have h1b1 : (x ⊓ y) ⊓ z ≤ y, calc (x ⊓ y) ⊓ z ≤ x ⊓ y : inf_le_left ... ≤ y : inf_le_right, have h1b2 : (x ⊓ y) ⊓ z ≤ z := inf_le_right, show (x ⊓ y) ⊓ z ≤ y ⊓ z, by exact le_inf h1b1 h1b2, }, show (x ⊓ y) ⊓ z ≤ x ⊓ (y ⊓ z), by exact le_inf h1a h1b, }, have h2 : x ⊓ (y ⊓ z) ≤ (x ⊓ y) ⊓ z, { have h2a : x ⊓ (y ⊓ z) ≤ x ⊓ y, { have h2a1 : x ⊓ (y ⊓ z) ≤ x, by exact inf_le_left, have h2a2 : x ⊓ (y ⊓ z) ≤ y, calc x ⊓ (y ⊓ z) ≤ y ⊓ z : inf_le_right ... ≤ y : inf_le_left, show x ⊓ (y ⊓ z) ≤ x ⊓ y, by exact le_inf h2a1 h2a2, }, have h2b : x ⊓ (y ⊓ z) ≤ z, calc x ⊓ (y ⊓ z) ≤ y ⊓ z : inf_le_right ... ≤ z : inf_le_right, show x ⊓ (y ⊓ z) ≤ (x ⊓ y) ⊓ z, by exact le_inf h2a h2b, }, show (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z), by exact le_antisymm h1 h2, end -- 2ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := begin apply le_antisymm, { apply le_inf, { apply inf_le_of_left_le inf_le_left, }, { apply le_inf (inf_le_of_left_le inf_le_right) inf_le_right}}, {apply le_inf, { apply le_inf inf_le_left (inf_le_of_right_le inf_le_left), }, { apply inf_le_of_right_le inf_le_right, },}, end -- 3ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := le_antisymm (le_inf (inf_le_of_left_le inf_le_left) (le_inf (inf_le_of_left_le inf_le_right) inf_le_right)) (le_inf (le_inf inf_le_left (inf_le_of_right_le inf_le_left)) (inf_le_of_right_le inf_le_right)) -- 4ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := -- by library_search inf_assoc -- 5ª demostración -- =============== example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := -- by hint by finish |
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.
3. Si R es un retículo y x, y, z ∈ R, entonces (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)
Demostrar que si R es un retículo y x, y, z ∈ R, entonces
|
1 |
(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] variables x y z : R example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := 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 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 |
import order.lattice variables {R : Type*} [lattice R] variables x y z : R -- 1ª demostración -- =============== example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := begin have h1 : (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z), { have h1a : x ⊔ y ≤ x ⊔ (y ⊔ z), by finish, have h1b : z ≤ x ⊔ (y ⊔ z), by finish, show (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z), by exact sup_le h1a h1b, }, have h2 : x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z, { have h2a : x ≤ (x ⊔ y) ⊔ z, by finish, have h2b : y ⊔ z ≤ (x ⊔ y) ⊔ z, by finish, show x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z, by exact sup_le h2a h2b, }, show (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z), by exact le_antisymm h1 h2, end -- 2ª demostración -- =============== example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := begin have h1 : (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z), { have h1a : x ⊔ y ≤ x ⊔ (y ⊔ z), { have h1a1 : x ≤ x ⊔ (y ⊔ z) := le_sup_left, have h1a2 : y ≤ x ⊔ (y ⊔ z), calc y ≤ y ⊔ z : le_sup_left ... ≤ x ⊔ (y ⊔ z) : le_sup_right, show x ⊔ y ≤ x ⊔ (y ⊔ z), by exact sup_le h1a1 h1a2, }, have h1b : z ≤ x ⊔ (y ⊔ z), calc z ≤ y ⊔ z : le_sup_right ... ≤ x ⊔ (y ⊔ z) : le_sup_right, show (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z), by exact sup_le h1a h1b, }, have h2 : x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z, { have h2a : x ≤ (x ⊔ y) ⊔ z, calc x ≤ x ⊔ y : le_sup_left ... ≤ (x ⊔ y) ⊔ z : le_sup_left, have h2b : y ⊔ z ≤ (x ⊔ y) ⊔ z, { have h2b1 : y ≤ (x ⊔ y) ⊔ z, calc y ≤ x ⊔ y : le_sup_right ... ≤ (x ⊔ y) ⊔ z : le_sup_left, have h2b2 : z ≤ (x ⊔ y) ⊔ z := le_sup_right, show y ⊔ z ≤ (x ⊔ y) ⊔ z, by exact sup_le h2b1 h2b2, }, show x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z, by exact sup_le h2a h2b, }, show (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z), by exact le_antisymm h1 h2, end -- 3ª demostración -- =============== example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := begin apply le_antisymm, { apply sup_le, { apply sup_le le_sup_left (le_sup_of_le_right le_sup_left)}, { apply le_sup_of_le_right le_sup_right}}, { apply sup_le, { apply le_sup_of_le_left le_sup_left}, { apply sup_le (le_sup_of_le_left le_sup_right) le_sup_right}}, end -- 4ª demostración -- =============== example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := le_antisymm (sup_le (sup_le le_sup_left (le_sup_of_le_right le_sup_left)) (le_sup_of_le_right le_sup_right)) (sup_le (le_sup_of_le_left le_sup_left) (sup_le (le_sup_of_le_left le_sup_right) le_sup_right)) -- 5ª demostración -- =============== example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := -- by library_search sup_assoc -- 6ª demostración -- =============== example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := -- by hint by finish |
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.
4. 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 |
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 := inf_le_left, have h2 : x ≤ x ⊓ (x ⊔ y), { have h2a : x ≤ x := rfl.ge, have h2b : x ≤ x ⊔ y := le_sup_left, show x ≤ x ⊓ (x ⊔ y), by exact le_inf h2a h2b, }, 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 inf_le_left }, { apply le_inf, { apply le_refl }, { apply le_sup_left }}, end -- 4ª demostración example : x ⊓ (x ⊔ y) = x := -- by library_search inf_sup_self -- 5ª 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.
5. 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.