-
Notifications
You must be signed in to change notification settings - Fork 0
/
Interseccion_de_intersecciones.thy
128 lines (119 loc) · 3.93 KB
/
Interseccion_de_intersecciones.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
(* Interseccion_de_intersecciones.thy
Intersección de intersecciones
José A. Alonso Jiménez
Sevilla, 3 de junio de 2021
---------------------------------------------------------------------
*)
text \<open>------------------------------------------------------------------
Demostrar que
(\<Inter> i, A i \<inter> B i) = (\<Inter> i, A i) \<inter> (\<Inter> i, B i)
---------------------------------------------------------------------\<close>
theory Interseccion_de_intersecciones
imports Main
begin
section \<open>1\<ordfeminine> demostración\<close>
lemma "(\<Inter> i \<in> I. A i \<inter> B i) = (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
proof (rule equalityI)
show "(\<Inter> i \<in> I. A i \<inter> B i) \<subseteq> (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
proof (rule subsetI)
fix x
assume h1 : "x \<in> (\<Inter> i \<in> I. A i \<inter> B i)"
have "x \<in> (\<Inter> i \<in> I. A i)"
proof (rule INT_I)
fix i
assume "i \<in> I"
with h1 have "x \<in> A i \<inter> B i"
by (rule INT_D)
then show "x \<in> A i"
by (rule IntD1)
qed
moreover
have "x \<in> (\<Inter> i \<in> I. B i)"
proof (rule INT_I)
fix i
assume "i \<in> I"
with h1 have "x \<in> A i \<inter> B i"
by (rule INT_D)
then show "x \<in> B i"
by (rule IntD2)
qed
ultimately show "x \<in> (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
by (rule IntI)
qed
next
show "(\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i) \<subseteq> (\<Inter> i \<in> I. A i \<inter> B i)"
proof (rule subsetI)
fix x
assume h2 : "x \<in> (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
show "x \<in> (\<Inter> i \<in> I. A i \<inter> B i)"
proof (rule INT_I)
fix i
assume "i \<in> I"
have "x \<in> A i"
proof -
have "x \<in> (\<Inter> i \<in> I. A i)"
using h2 by (rule IntD1)
then show "x \<in> A i"
using \<open>i \<in> I\<close> by (rule INT_D)
qed
moreover
have "x \<in> B i"
proof -
have "x \<in> (\<Inter> i \<in> I. B i)"
using h2 by (rule IntD2)
then show "x \<in> B i"
using \<open>i \<in> I\<close> by (rule INT_D)
qed
ultimately show "x \<in> A i \<inter> B i"
by (rule IntI)
qed
qed
qed
section \<open>2\<ordfeminine> demostración\<close>
lemma "(\<Inter> i \<in> I. A i \<inter> B i) = (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
proof
show "(\<Inter> i \<in> I. A i \<inter> B i) \<subseteq> (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
proof
fix x
assume h1 : "x \<in> (\<Inter> i \<in> I. A i \<inter> B i)"
have "x \<in> (\<Inter> i \<in> I. A i)"
proof
fix i
assume "i \<in> I"
then show "x \<in> A i"
using h1 by simp
qed
moreover
have "x \<in> (\<Inter> i \<in> I. B i)"
proof
fix i
assume "i \<in> I"
then show "x \<in> B i"
using h1 by simp
qed
ultimately show "x \<in> (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
by simp
qed
next
show "(\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i) \<subseteq> (\<Inter> i \<in> I. A i \<inter> B i)"
proof
fix x
assume h2 : "x \<in> (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
show "x \<in> (\<Inter> i \<in> I. A i \<inter> B i)"
proof
fix i
assume "i \<in> I"
then have "x \<in> A i"
using h2 by simp
moreover
have "x \<in> B i"
using \<open>i \<in> I\<close> h2 by simp
ultimately show "x \<in> A i \<inter> B i"
by simp
qed
qed
qed
section \<open>3\<ordfeminine> demostración\<close>
lemma "(\<Inter> i \<in> I. A i \<inter> B i) = (\<Inter> i \<in> I. A i) \<inter> (\<Inter> i \<in> I. B i)"
by auto
end