-
Notifications
You must be signed in to change notification settings - Fork 0
/
Las_relaciones_definidas_por_particiones_son_transitivas.lean
71 lines (60 loc) · 1.65 KB
/
Las_relaciones_definidas_por_particiones_son_transitivas.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
-- Las_relaciones_definidas_por_particiones_son_transitivas.lean
-- Las relaciones definidas por particiones son transitivas
-- José A. Alonso Jiménez
-- Sevilla, 11 de octubre de 2021
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que la relación correspondiente a una partición es
-- transitiva.
-- ---------------------------------------------------------------------
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}
def relacion : (particion A) → (A → A → Prop) :=
λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X
-- 1ª demostración
example
(P : particion A)
: transitive (relacion P) :=
begin
unfold transitive,
intros a b c hab hbc,
unfold relacion at *,
intros X hX haX,
apply hbc,
{ exact hX, },
{ apply hab,
{ exact hX, },
{ exact haX, }},
end
-- 2ª demostración
example
(P : particion A)
: transitive (relacion P) :=
begin
intros a b c hab hbc,
intros X hX haX,
apply hbc X hX,
apply hab X hX,
exact haX,
end
-- 3ª demostración
example
(P : particion A)
: transitive (relacion P) :=
begin
intros a b c hab hbc X hX haX,
exact hbc X hX (hab X hX haX),
end
-- 4ª demostración
lemma transitiva
(P : particion A)
: transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)
end particion