-
Notifications
You must be signed in to change notification settings - Fork 0
/
Asociatividad_del_infimo.lean
170 lines (153 loc) · 5.87 KB
/
Asociatividad_del_infimo.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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
-- Asociatividad_del_infimo.lean
-- En los retículos, (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z).
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 19-septiembre-2023
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que en los retículos se verifica que
-- (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- En la demostración se usarán los siguientes lemas
-- le_antisymm : x ≤ y → y ≤ x → x = y
-- le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y
-- inf_le_left : x ⊓ y ≤ x
-- inf_le_right : x ⊓ y ≤ y)
--
-- Por le_antisym, es suficiente demostrar las siguientes relaciones:
-- (x ⊓ y) ⊓ z ≤ x ⊓ (y ⊓ z) (1)
-- x ⊓ (y ⊓ z) ≤ (x ⊓ y) ⊓ z (2)
--
-- Para demostrar (1), por le_inf, basta probar que
-- (x ⊓ y) ⊓ z ≤ x (1a)
-- (x ⊓ y) ⊓ z ≤ y ⊓ z (1b)
--
-- La (1a) se demuestra por la siguiente cadena de desigualdades
-- (x ⊓ y) ⊓ z ≤ x ⊓ y [por inf_le_left]
-- ≤ x [por inf_le_left]
--
-- Para demostrar (1b), por le_inf, basta probar que
-- (x ⊓ y) ⊓ z ≤ y (1b1)
-- (x ⊓ y) ⊓ z ≤ z (1b2)
--
-- La (1b1) se demuestra por la siguiente cadena de desigualdades
-- (x ⊓ y) ⊓ z ≤ x ⊓ y [por inf_le_left]
-- ≤ y [por inf_le_right]
--
-- La (1b2) se tiene por inf_le_right.
--
-- Para demostrar (2), por le_inf, basta probar que
-- x ⊓ (y ⊓ z) ≤ x ⊓ y (2a)
-- x ⊓ (y ⊓ z) ≤ z (2b)
--
-- Para demostrar (2a), por le_inf, basta probar que
-- x ⊓ (y ⊓ z) ≤ x (2a1)
-- x ⊓ (y ⊓ z) ≤ y (2a2)
--
-- La (2a1) se tiene por inf_le_left.
--
-- La (2a2) se demuestra por la siguiente cadena de desigualdades
-- x ⊓ (y ⊓ z) ≤ y ⊓ z [por inf_le_right]
-- ≤ y [por inf_le_left]
--
-- La (2b) se demuestra por la siguiente cadena de desigualdades
-- x ⊓ (y ⊓ z) ≤ y ⊓ z [por inf_le_right]
-- ≤ z [por inf_le_right]
-- Demostraciones con Lean4
-- ========================
import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (x y z : α)
-- 1ª demostración
-- ===============
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by
have h1 : (x ⊓ y) ⊓ z ≤ x ⊓ (y ⊓ z) := by
{ have h1a : (x ⊓ y) ⊓ z ≤ x := calc
(x ⊓ y) ⊓ z ≤ x ⊓ y := by exact inf_le_left
_ ≤ x := by exact inf_le_left
have h1b : (x ⊓ y) ⊓ z ≤ y ⊓ z := by
{ have h1b1 : (x ⊓ y) ⊓ z ≤ y := calc
(x ⊓ y) ⊓ z ≤ x ⊓ y := by exact inf_le_left
_ ≤ y := by exact inf_le_right
have h1b2 : (x ⊓ y) ⊓ z ≤ z :=
inf_le_right
show (x ⊓ y) ⊓ z ≤ y ⊓ z
exact le_inf h1b1 h1b2 }
show (x ⊓ y) ⊓ z ≤ x ⊓ (y ⊓ z)
exact le_inf h1a h1b }
have h2 : x ⊓ (y ⊓ z) ≤ (x ⊓ y) ⊓ z := by
{ have h2a : x ⊓ (y ⊓ z) ≤ x ⊓ y := by
{ have h2a1 : x ⊓ (y ⊓ z) ≤ x :=
inf_le_left
have h2a2 : x ⊓ (y ⊓ z) ≤ y := calc
x ⊓ (y ⊓ z) ≤ y ⊓ z := by exact inf_le_right
_ ≤ y := by exact inf_le_left
show x ⊓ (y ⊓ z) ≤ x ⊓ y
exact le_inf h2a1 h2a2 }
have h2b : x ⊓ (y ⊓ z) ≤ z := by calc
x ⊓ (y ⊓ z) ≤ y ⊓ z := by exact inf_le_right
_ ≤ z := by exact inf_le_right
show x ⊓ (y ⊓ z) ≤ (x ⊓ y) ⊓ z
exact le_inf h2a h2b }
show (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)
exact le_antisymm h1 h2
-- 2ª demostración
-- ===============
example : x ⊓ y ⊓ z = x ⊓ (y ⊓ z) := by
apply le_antisymm
· apply le_inf
· apply le_trans
apply inf_le_left
apply inf_le_left
. apply le_inf
· apply le_trans
apply inf_le_left
apply inf_le_right
. apply inf_le_right
. apply le_inf
· apply le_inf
· apply inf_le_left
. apply le_trans
apply inf_le_right
apply inf_le_left
. apply le_trans
apply inf_le_right
apply inf_le_right
-- 3ª demostración
-- ===============
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by
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
-- 4ª 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))
-- 5ª demostración
-- ===============
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
-- by apply?
inf_assoc x y z
-- Lemas usados
-- ============
-- #check (inf_assoc x y z : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z))
-- #check (inf_le_left : x ⊓ y ≤ x)
-- #check (inf_le_of_left_le : x ≤ z → x ⊓ y ≤ z)
-- #check (inf_le_of_right_le : y ≤ z → x ⊓ y ≤ z)
-- #check (inf_le_right : x ⊓ y ≤ y)
-- #check (le_antisymm : x ≤ y → y ≤ x → x = y)
-- #check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y)
-- #check (le_trans : x ≤ y → y ≤ z → x ≤ z)