-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPropiedad_semidistributiva_de_la_interseccion_sobre_la_union.lean
119 lines (102 loc) · 2.76 KB
/
Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.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
-- Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.lean
-- s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 21-febrero-2024
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que
-- s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Sea x ∈ s ∩ (t ∪ u). Entonces se tiene que
-- x ∈ s (1)
-- x ∈ t ∪ u (2)
-- La relación (2) da lugar a dos casos.
--
-- Caso 1: Supongamos que x ∈ t. Entonces, por (1), x ∈ s ∩ t y, por
-- tanto, x ∈ (s ∩ t) ∪ (s ∩ u).
--
-- Caso 2: Supongamos que x ∈ u. Entonces, por (1), x ∈ s ∩ u y, por
-- tanto, x ∈ (s ∩ t) ∪ (s ∩ u).
-- Demostraciones con Lean4
-- ========================
import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t u : Set α)
-- 1ª demostración
-- ===============
example :
s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by
intros x hx
-- x : α
-- hx : x ∈ s ∩ (t ∪ u)
-- ⊢ x ∈ s ∩ t ∪ s ∩ u
rcases hx with ⟨hxs, hxtu⟩
-- hxs : x ∈ s
-- hxtu : x ∈ t ∪ u
rcases hxtu with (hxt | hxu)
. -- hxt : x ∈ t
left
-- ⊢ x ∈ s ∩ t
constructor
. -- ⊢ x ∈ s
exact hxs
. -- hxt : x ∈ t
exact hxt
. -- hxu : x ∈ u
right
-- ⊢ x ∈ s ∩ u
constructor
. -- ⊢ x ∈ s
exact hxs
. -- ⊢ x ∈ u
exact hxu
-- 2ª demostración
-- ===============
example :
s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by
rintro x ⟨hxs, hxt | hxu⟩
-- x : α
-- hxs : x ∈ s
-- ⊢ x ∈ s ∩ t ∪ s ∩ u
. -- hxt : x ∈ t
left
-- ⊢ x ∈ s ∩ t
exact ⟨hxs, hxt⟩
. -- hxu : x ∈ u
right
-- ⊢ x ∈ s ∩ u
exact ⟨hxs, hxu⟩
-- 3ª demostración
-- ===============
example :
s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by
rintro x ⟨hxs, hxt | hxu⟩
-- x : α
-- hxs : x ∈ s
-- ⊢ x ∈ s ∩ t ∪ s ∩ u
. -- hxt : x ∈ t
exact Or.inl ⟨hxs, hxt⟩
. -- hxu : x ∈ u
exact Or.inr ⟨hxs, hxu⟩
-- 4ª demostración
-- ===============
example :
s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by
intro x hx
-- x : α
-- hx : x ∈ s ∩ (t ∪ u)
-- ⊢ x ∈ s ∩ t ∪ s ∩ u
aesop
-- 5ª demostración
-- ===============
example :
s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by rw [inter_union_distrib_left]