-
Notifications
You must be signed in to change notification settings - Fork 0
/
El_cociente_aplica_relaciones_de_equivalencia_en_particiones.lean
91 lines (76 loc) · 2.51 KB
/
El_cociente_aplica_relaciones_de_equivalencia_en_particiones.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
-- El_cociente_aplica_relaciones_de_equivalencia_en_particiones.lean
-- El cociente aplica relaciones de equivalencia en particiones
-- José A. Alonso Jiménez
-- Sevilla, 8 de octubre de 2021
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Definir la función
-- cociente : {R : A → A → Prop // equivalence R} → particion A
-- tal que (cociente R) es la partición de A formada por las clases de
-- equivalencia de la relación de equivalencia R.
-- ---------------------------------------------------------------------
import tactic
@[ext] structure particion (A : Type) :=
(Bloques : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)
namespace particion
variable {A : Type}
variable {P : particion A}
variables {X Y : set A}
variable (R : A → A → Prop)
def clase (a : A) :=
{b : A | R b a}
def clases : (A → A → Prop) → set (set A) :=
λ R, {B : set A | ∃ x : A, B = clase R x}
lemma pertenece_clase_syss
{a b : A}
: b ∈ clase R a ↔ R b a :=
by refl
lemma clases_no_vacias
(hR: equivalence R)
: ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
rintros _ ⟨a, rfl⟩,
use a,
rw pertenece_clase_syss,
apply hR.1,
end
lemma clases_recubren
(hR: equivalence R)
: ∀ a, ∃ X ∈ clases R, a ∈ X :=
begin
intro a,
use clase R a,
split,
{ use a, },
{ exact hR.1 a, },
end
lemma subclase_si_pertenece
{R : A → A → Prop}
(hR: equivalence R)
{a b : A}
: a ∈ clase R b → clase R a ⊆ clase R b :=
λ hab z hza, hR.2.2 hza hab
lemma clases_iguales_si_pertenece
{R : A → A → Prop}
(hR: equivalence R)
{a b : A}
: a ∈ clase R b → clase R a = clase R b :=
λ hab, set.subset.antisymm
(subclase_si_pertenece hR hab)
(subclase_si_pertenece hR (hR.2.1 hab))
lemma clases_disjuntas
(hR: equivalence R)
: ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=
begin
rintros X ⟨a, rfl⟩ Y ⟨b, rfl⟩ ⟨c, hca, hcb⟩,
exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),
end
def cociente : {R : A → A → Prop // equivalence R} → particion A :=
λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x},
Hno_vacios := clases_no_vacias R.1 R.2,
Hrecubren := clases_recubren R.1 R.2,
Hdisjuntos := clases_disjuntas R.1 R.2, }
end particion