-
Notifications
You must be signed in to change notification settings - Fork 0
/
El_conjunto_de_las_clases_de_equivalencia_es_una_particion.lean
92 lines (83 loc) · 2.19 KB
/
El_conjunto_de_las_clases_de_equivalencia_es_una_particion.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
-- El_conjunto_de_las_clases_de_equivalencia_es_una_particion.lean
-- El conjunto de las clases de equivalencia es una partición.
-- José A. Alonso Jiménez
-- Sevilla, 24 de agosto de 2021
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que si R es una relación de equivalencia en X, entonces las
-- clases de equivalencia de R es una partición de X.
-- ---------------------------------------------------------------------
import tactic
variable {X : Type}
variables {x y: X}
variable {R : X → X → Prop}
def clase (R : X → X → Prop) (x : X) :=
{y : X | R x y}
def particion (A : set (set X)) : Prop :=
(∀ x, (∃ B ∈ A, x ∈ B ∧ ∀ C ∈ A, x ∈ C → B = C)) ∧ ∅ ∉ A
lemma aux
(h : equivalence R)
(hxy : R x y)
: clase R y ⊆ clase R x :=
λ z hz, h.2.2 hxy hz
-- 1ª demostración
example
(h : equivalence R)
: particion {a : set X | ∃ s : X, a = clase R s} :=
begin
split,
{ simp,
intro y,
use (clase R y),
split,
{ use y, },
{ split,
{ exact h.1 y, },
{ intros x hx,
apply le_antisymm,
{ exact aux h hx, },
{ exact aux h (h.2.1 hx), }}}},
{ simp,
intros x hx,
have h1 : x ∈ clase R x := h.1 x,
rw ← hx at h1,
exact set.not_mem_empty x h1, },
end
-- 2ª demostración
example
(h : equivalence R)
: particion {a : set X | ∃ s : X, a = clase R s} :=
begin
split,
{ simp,
intro y,
use (clase R y),
split,
{ use y, },
{ split,
{ exact h.1 y, },
{ intros x hx,
exact le_antisymm (aux h hx) (aux h (h.2.1 hx)), }}},
{ simp,
intros x hx,
have h1 : x ∈ clase R x := h.1 x,
rw ← hx at h1,
exact set.not_mem_empty x h1, },
end
-- 3ª demostración
example
(h : equivalence R)
: particion {a : set X | ∃ s : X, a = clase R s} :=
begin
split,
{ simp,
intro y,
use [clase R y,
⟨by use y,
⟨h.1 y, λ x hx, le_antisymm (aux h hx) (aux h (h.2.1 hx))⟩⟩], },
{ simp,
intros x hx,
have h1 : x ∈ clase R x := h.1 x,
rw ← hx at h1,
exact set.not_mem_empty x h1, },
end