-
Notifications
You must be signed in to change notification settings - Fork 0
/
Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.thy
138 lines (129 loc) · 4.02 KB
/
Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.thy
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
133
134
135
136
137
138
(* Propiedad_semidistributiva_de_la_interseccion_sobre_la_union.thy
Propiedad semidistributiva de la intersección sobre la unión
José A. Alonso Jiménez
Sevilla, 18 de mayo de 2021
---------------------------------------------------------------------
*)
(* ---------------------------------------------------------------------
-- Demostrar que
-- s \<inter> (t \<union> u) \<subseteq> (s \<inter> t) \<union> (s \<inter> u)
-- ------------------------------------------------------------------ *)
theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union
imports Main
begin
(* 1\<ordfeminine> demostración *)
lemma "s \<inter> (t \<union> u) \<subseteq> (s \<inter> t) \<union> (s \<inter> u)"
proof (rule subsetI)
fix x
assume hx : "x \<in> s \<inter> (t \<union> u)"
then have xs : "x \<in> s"
by (simp only: IntD1)
have xtu: "x \<in> t \<union> u"
using hx
by (simp only: IntD2)
then have "x \<in> t \<or> x \<in> u"
by (simp only: Un_iff)
then show " x \<in> s \<inter> t \<union> s \<inter> u"
proof (rule disjE)
assume xt : "x \<in> t"
have xst : "x \<in> s \<inter> t"
using xs xt by (simp only: Int_iff)
then show "x \<in> (s \<inter> t) \<union> (s \<inter> u)"
by (simp only: UnI1)
next
assume xu : "x \<in> u"
have xst : "x \<in> s \<inter> u"
using xs xu by (simp only: Int_iff)
then show "x \<in> (s \<inter> t) \<union> (s \<inter> u)"
by (simp only: UnI2)
qed
qed
(* 2\<ordfeminine> demostración *)
lemma "s \<inter> (t \<union> u) \<subseteq> (s \<inter> t) \<union> (s \<inter> u)"
proof
fix x
assume hx : "x \<in> s \<inter> (t \<union> u)"
then have xs : "x \<in> s"
by simp
have xtu: "x \<in> t \<union> u"
using hx
by simp
then have "x \<in> t \<or> x \<in> u"
by simp
then show " x \<in> s \<inter> t \<union> s \<inter> u"
proof
assume xt : "x \<in> t"
have xst : "x \<in> s \<inter> t"
using xs xt
by simp
then show "x \<in> (s \<inter> t) \<union> (s \<inter> u)"
by simp
next
assume xu : "x \<in> u"
have xst : "x \<in> s \<inter> u"
using xs xu
by simp
then show "x \<in> (s \<inter> t) \<union> (s \<inter> u)"
by simp
qed
qed
(* 3\<ordfeminine> demostración *)
lemma "s \<inter> (t \<union> u) \<subseteq> (s \<inter> t) \<union> (s \<inter> u)"
proof (rule subsetI)
fix x
assume hx : "x \<in> s \<inter> (t \<union> u)"
then have xs : "x \<in> s"
by (simp only: IntD1)
have xtu: "x \<in> t \<union> u"
using hx
by (simp only: IntD2)
then show " x \<in> s \<inter> t \<union> s \<inter> u"
proof (rule UnE)
assume xt : "x \<in> t"
have xst : "x \<in> s \<inter> t"
using xs xt
by (simp only: Int_iff)
then show "x \<in> (s \<inter> t) \<union> (s \<inter> u)"
by (simp only: UnI1)
next
assume xu : "x \<in> u"
have xst : "x \<in> s \<inter> u"
using xs xu
by (simp only: Int_iff)
then show "x \<in> (s \<inter> t) \<union> (s \<inter> u)"
by (simp only: UnI2)
qed
qed
(* 4\<ordfeminine> demostración *)
lemma "s \<inter> (t \<union> u) \<subseteq> (s \<inter> t) \<union> (s \<inter> u)"
proof
fix x
assume hx : "x \<in> s \<inter> (t \<union> u)"
then have xs : "x \<in> s"
by simp
have xtu: "x \<in> t \<union> u"
using hx
by simp
then show " x \<in> s \<inter> t \<union> s \<inter> u"
proof (rule UnE)
assume xt : "x \<in> t"
have xst : "x \<in> s \<inter> t"
using xs xt
by simp
then show "x \<in> (s \<inter> t) \<union> (s \<inter> u)"
by simp
next
assume xu : "x \<in> u"
have xst : "x \<in> s \<inter> u"
using xs xu by simp
then show "x \<in> (s \<inter> t) \<union> (s \<inter> u)"
by simp
qed
qed
(* 5\<ordfeminine> demostración *)
lemma "s \<inter> (t \<union> u) \<subseteq> (s \<inter> t) \<union> (s \<inter> u)"
by (simp only: Int_Un_distrib)
(* 6\<ordfeminine> demostración *)
lemma "s \<inter> (t \<union> u) \<subseteq> (s \<inter> t) \<union> (s \<inter> u)"
by auto
end