-
Notifications
You must be signed in to change notification settings - Fork 0
/
Propiedad_distributiva_1.lean
50 lines (41 loc) · 1.79 KB
/
Propiedad_distributiva_1.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
-- Propiedad_distributiva_1.lean
-- En los retículos, una distributiva del ínfimo implica la otra.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 25-septiembre-2023
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que si α es un retículo tal que
-- ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))
-- entonces
-- (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)
-- para todos los elementos de α.
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Se demuestra por la siguiente cadena de igualdades
-- (a ⊔ b) ⊓ c = c ⊓ (a ⊔ b) [por conmutatividad de ⊓]
-- = (c ⊓ a) ⊔ (c ⊓ b) [por la hipótesis]
-- = (a ⊓ c) ⊔ (c ⊓ b) [por conmutatividad de ⊓]
-- = (a ⊓ c) ⊔ (b ⊓ c) [por conmutatividad de ⊓]
-- Demostraciones con Lean4
-- ========================
import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (a b c : α)
-- 1ª demostración
example
(h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))
: (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) :=
calc
(a ⊔ b) ⊓ c = c ⊓ (a ⊔ b) := by rw [inf_comm]
_ = (c ⊓ a) ⊔ (c ⊓ b) := by rw [h]
_ = (a ⊓ c) ⊔ (c ⊓ b) := by rw [@inf_comm _ _ c a]
_ = (a ⊓ c) ⊔ (b ⊓ c) := by rw [@inf_comm _ _ c b]
-- 2ª demostración
example
(h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))
: (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) :=
by simp [h, inf_comm]
-- Lemas usados
-- ============
-- #check (inf_comm : a ⊓ b = b ⊓ a)