-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDiferencia_de_diferencia_de_conjuntos_2.lean
132 lines (112 loc) · 3.23 KB
/
Diferencia_de_diferencia_de_conjuntos_2.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
-- Diferencia_de_diferencia_de_conjuntos_2.lean
-- s \ (t ∪ u) ⊆ (s \ t) \ u
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 26-febrero-2024
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que
-- s \ (t ∪ u) ⊆ (s \ t) \ u
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Sea x ∈ s \ (t ∪ u). Entonces,
-- x ∈ s (1)
-- x ∉ t ∪ u (2)
-- Tenemos que demostrar que x ∈ (s \ t) \ u; es decir, que se verifican
-- las relaciones
-- x ∈ s \ t (3)
-- x ∉ u (4)
-- Para demostrar (3) tenemos que demostrar las relaciones
-- x ∈ s (5)
-- x ∉ t (6)
-- La (5) se tiene por la (1). Para demostrar la (6), supongamos que
-- x ∈ t; entonces, x ∈ t ∪ u, en contracción con (2). Para demostrar la
-- (4), supongamos que x ∈ u; entonces, x ∈ t ∪ u, en contracción con
-- (2).
-- Demostraciones con Lean4
-- ========================
import Mathlib.Data.Set.Basic
open Set
variable {α : Type}
variable (s t u : Set α)
-- 1ª demostración
-- ===============
example : s \ (t ∪ u) ⊆ (s \ t) \ u :=
by
intros x hx
-- x : α
-- hx : x ∈ s \ (t ∪ u)
-- ⊢ x ∈ (s \ t) \ u
constructor
. -- ⊢ x ∈ s \ t
constructor
. -- ⊢ x ∈ s
exact hx.1
. -- ⊢ ¬x ∈ t
intro xt
-- xt : x ∈ t
-- ⊢ False
apply hx.2
-- ⊢ x ∈ t ∪ u
left
-- ⊢ x ∈ t
exact xt
. -- ⊢ ¬x ∈ u
intro xu
-- xu : x ∈ u
-- ⊢ False
apply hx.2
-- ⊢ x ∈ t ∪ u
right
-- ⊢ x ∈ u
exact xu
-- 2ª demostración
-- ===============
example : s \ (t ∪ u) ⊆ (s \ t) \ u :=
by
rintro x ⟨xs, xntu⟩
-- x : α
-- xs : x ∈ s
-- xntu : ¬x ∈ t ∪ u
-- ⊢ x ∈ (s \ t) \ u
constructor
. -- ⊢ x ∈ s \ t
constructor
. -- ⊢ x ∈ s
exact xs
. -- ¬x ∈ t
intro xt
-- xt : x ∈ t
-- ⊢ False
exact xntu (Or.inl xt)
. -- ⊢ ¬x ∈ u
intro xu
-- xu : x ∈ u
-- ⊢ False
exact xntu (Or.inr xu)
-- 2ª demostración
-- ===============
example : s \ (t ∪ u) ⊆ (s \ t) \ u :=
fun _ ⟨xs, xntu⟩ ↦ ⟨⟨xs, fun xt ↦ xntu (Or.inl xt)⟩,
fun xu ↦ xntu (Or.inr xu)⟩
-- 4ª demostración
-- ===============
example : s \ (t ∪ u) ⊆ (s \ t) \ u :=
by
rintro x ⟨xs, xntu⟩
-- x : α
-- xs : x ∈ s
-- xntu : ¬x ∈ t ∪ u
-- ⊢ x ∈ (s \ t) \ u
aesop
-- 5ª demostración
-- ===============
example : s \ (t ∪ u) ⊆ (s \ t) \ u :=
by intro ; aesop
-- 6ª demostración
-- ===============
example : s \ (t ∪ u) ⊆ (s \ t) \ u :=
by rw [diff_diff]
-- Lema usado
-- ==========
-- #check (diff_diff : (s \ t) \ u = s \ (t ∪ u))