author  hoelzl 
Tue, 05 Mar 2013 15:43:14 +0100  
changeset 51343  b61b32f62c78 
parent 51342  763c6872bd10 
child 51344  b3d246c92dfb 
permissions  rwrr 
33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

1 
(* title: HOL/Library/Topology_Euclidian_Space.thy 
33175  2 
Author: Amine Chaieb, University of Cambridge 
3 
Author: Robert Himmelmann, TU Muenchen 

44075  4 
Author: Brian Huffman, Portland State University 
33175  5 
*) 
6 

7 
header {* Elementary topology in Euclidean space. *} 

8 

9 
theory Topology_Euclidean_Space 

50087  10 
imports 
50938  11 
Complex_Main 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

12 
"~~/src/HOL/Library/Countable_Set" 
50087  13 
"~~/src/HOL/Library/Glbs" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

14 
"~~/src/HOL/Library/FuncSet" 
50938  15 
Linear_Algebra 
50087  16 
Norm_Arith 
17 
begin 

18 

50972  19 
lemma dist_0_norm: 
20 
fixes x :: "'a::real_normed_vector" 

21 
shows "dist 0 x = norm x" 

22 
unfolding dist_norm by simp 

23 

50943
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset

24 
lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d" 
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset

25 
using dist_triangle[of y z x] by (simp add: dist_commute) 
88a00a1c7c2c
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
hoelzl
parents:
50942
diff
changeset

26 

50972  27 
(* LEGACY *) 
28 
lemma lim_subseq: "subseq r \<Longrightarrow> s > l \<Longrightarrow> (s o r) > l" 

29 
by (rule LIMSEQ_subseq_LIMSEQ) 

30 

51342  31 
lemmas real_isGlb_unique = isGlb_unique[where 'a=real] 
50942  32 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

33 
lemma countable_PiE: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

34 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

35 
by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

36 

50087  37 
subsection {* Topological Basis *} 
38 

39 
context topological_space 

40 
begin 

41 

42 
definition "topological_basis B = 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

43 
((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x)))" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

44 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

45 
lemma topological_basis: 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

46 
"topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" 
50998  47 
unfolding topological_basis_def 
48 
apply safe 

49 
apply fastforce 

50 
apply fastforce 

51 
apply (erule_tac x="x" in allE) 

52 
apply simp 

53 
apply (rule_tac x="{x}" in exI) 

54 
apply auto 

55 
done 

56 

50087  57 
lemma topological_basis_iff: 
58 
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'" 

59 
shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))" 

60 
(is "_ \<longleftrightarrow> ?rhs") 

61 
proof safe 

62 
fix O' and x::'a 

63 
assume H: "topological_basis B" "open O'" "x \<in> O'" 

64 
hence "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def) 

65 
then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto 

66 
thus "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto 

67 
next 

68 
assume H: ?rhs 

69 
show "topological_basis B" using assms unfolding topological_basis_def 

70 
proof safe 

71 
fix O'::"'a set" assume "open O'" 

72 
with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'" 

73 
by (force intro: bchoice simp: Bex_def) 

74 
thus "\<exists>B'\<subseteq>B. \<Union>B' = O'" 

75 
by (auto intro: exI[where x="{f x x. x \<in> O'}"]) 

76 
qed 

77 
qed 

78 

79 
lemma topological_basisI: 

80 
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'" 

81 
assumes "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" 

82 
shows "topological_basis B" 

83 
using assms by (subst topological_basis_iff) auto 

84 

85 
lemma topological_basisE: 

86 
fixes O' 

87 
assumes "topological_basis B" 

88 
assumes "open O'" 

89 
assumes "x \<in> O'" 

90 
obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'" 

91 
proof atomize_elim 

92 
from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'" by (simp add: topological_basis_def) 

93 
with topological_basis_iff assms 

94 
show "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" using assms by (simp add: Bex_def) 

95 
qed 

96 

50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

97 
lemma topological_basis_open: 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

98 
assumes "topological_basis B" 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

99 
assumes "X \<in> B" 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

100 
shows "open X" 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

101 
using assms 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

102 
by (simp add: topological_basis_def) 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

103 

51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

104 
lemma topological_basis_imp_subbasis: 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

105 
assumes B: "topological_basis B" shows "open = generate_topology B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

106 
proof (intro ext iffI) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

107 
fix S :: "'a set" assume "open S" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

108 
with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

109 
unfolding topological_basis_def by blast 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

110 
then show "generate_topology B S" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

111 
by (auto intro: generate_topology.intros dest: topological_basis_open) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

112 
next 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

113 
fix S :: "'a set" assume "generate_topology B S" then show "open S" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

114 
by induct (auto dest: topological_basis_open[OF B]) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

115 
qed 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

116 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

117 
lemma basis_dense: 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

118 
fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

119 
assumes "topological_basis B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

120 
assumes choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

121 
shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

122 
proof (intro allI impI) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

123 
fix X::"'a set" assume "open X" "X \<noteq> {}" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

124 
from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]] 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

125 
guess B' . note B' = this 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

126 
thus "\<exists>B'\<in>B. f B' \<in> X" by (auto intro!: choosefrom_basis) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

127 
qed 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

128 

50087  129 
end 
130 

50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

131 
lemma topological_basis_prod: 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

132 
assumes A: "topological_basis A" and B: "topological_basis B" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

133 
shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

134 
unfolding topological_basis_def 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

135 
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric]) 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

136 
fix S :: "('a \<times> 'b) set" assume "open S" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

137 
then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

138 
proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"]) 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

139 
fix x y assume "(x, y) \<in> S" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

140 
from open_prod_elim[OF `open S` this] 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

141 
obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

142 
by (metis mem_Sigma_iff) 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

143 
moreover from topological_basisE[OF A a] guess A0 . 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

144 
moreover from topological_basisE[OF B b] guess B0 . 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

145 
ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

146 
by (intro UN_I[of "(A0, B0)"]) auto 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

147 
qed auto 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

148 
qed (metis A B topological_basis_open open_Times) 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

149 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

150 
subsection {* Countable Basis *} 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

151 

dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

152 
locale countable_basis = 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

153 
fixes B::"'a::topological_space set set" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

154 
assumes is_basis: "topological_basis B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

155 
assumes countable_basis: "countable B" 
33175  156 
begin 
157 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

158 
lemma open_countable_basis_ex: 
50087  159 
assumes "open X" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

160 
shows "\<exists>B' \<subseteq> B. X = Union B'" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

161 
using assms countable_basis is_basis unfolding topological_basis_def by blast 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

162 

dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

163 
lemma open_countable_basisE: 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

164 
assumes "open X" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

165 
obtains B' where "B' \<subseteq> B" "X = Union B'" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

166 
using assms open_countable_basis_ex by (atomize_elim) simp 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

167 

dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

168 
lemma countable_dense_exists: 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

169 
shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))" 
50087  170 
proof  
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

171 
let ?f = "(\<lambda>B'. SOME x. x \<in> B')" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

172 
have "countable (?f ` B)" using countable_basis by simp 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

173 
with basis_dense[OF is_basis, of ?f] show ?thesis 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

174 
by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI) 
50087  175 
qed 
176 

177 
lemma countable_dense_setE: 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

178 
obtains D :: "'a set" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

179 
where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

180 
using countable_dense_exists by blast 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

181 

50087  182 
end 
183 

50883  184 
class first_countable_topology = topological_space + 
185 
assumes first_countable_basis: 

186 
"\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))" 

187 

188 
lemma (in first_countable_topology) countable_basis_at_decseq: 

189 
obtains A :: "nat \<Rightarrow> 'a set" where 

190 
"\<And>i. open (A i)" "\<And>i. x \<in> (A i)" 

191 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially" 

192 
proof atomize_elim 

193 
from first_countable_basis[of x] obtain A 

194 
where "countable A" 

195 
and nhds: "\<And>a. a \<in> A \<Longrightarrow> open a" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" 

196 
and incl: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" by auto 

197 
then have "A \<noteq> {}" by auto 

198 
with `countable A` have r: "A = range (from_nat_into A)" by auto 

199 
def F \<equiv> "\<lambda>n. \<Inter>i\<le>n. from_nat_into A i" 

200 
show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> 

201 
(\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)" 

202 
proof (safe intro!: exI[of _ F]) 

203 
fix i 

204 
show "open (F i)" using nhds(1) r by (auto simp: F_def intro!: open_INT) 

205 
show "x \<in> F i" using nhds(2) r by (auto simp: F_def) 

206 
next 

207 
fix S assume "open S" "x \<in> S" 

208 
from incl[OF this] obtain i where "F i \<subseteq> S" 

209 
by (subst (asm) r) (auto simp: F_def) 

210 
moreover have "\<And>j. i \<le> j \<Longrightarrow> F j \<subseteq> F i" 

211 
by (auto simp: F_def) 

212 
ultimately show "eventually (\<lambda>i. F i \<subseteq> S) sequentially" 

213 
by (auto simp: eventually_sequentially) 

214 
qed 

215 
qed 

216 

217 
lemma (in first_countable_topology) first_countable_basisE: 

218 
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" 

219 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" 

220 
using first_countable_basis[of x] 

221 
by atomize_elim auto 

222 

51105  223 
lemma (in first_countable_topology) first_countable_basis_Int_stableE: 
224 
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" 

225 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" 

226 
"\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A" 

227 
proof atomize_elim 

228 
from first_countable_basisE[of x] guess A' . note A' = this 

229 
def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)" 

230 
thus "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and> 

231 
(\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" 

232 
proof (safe intro!: exI[where x=A]) 

233 
show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite) 

234 
fix a assume "a \<in> A" 

235 
thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) 

236 
next 

237 
let ?int = "\<lambda>N. \<Inter>from_nat_into A' ` N" 

238 
fix a b assume "a \<in> A" "b \<in> A" 

239 
then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def) 

240 
thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) 

241 
next 

242 
fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast 

243 
thus "\<exists>a\<in>A. a \<subseteq> S" using a A' 

244 
by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"]) 

245 
qed 

246 
qed 

247 

50883  248 
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology 
249 
proof 

250 
fix x :: "'a \<times> 'b" 

251 
from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this 

252 
from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this 

253 
show "\<exists>A::('a\<times>'b) set set. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))" 

254 
proof (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe) 

255 
fix a b assume x: "a \<in> A" "b \<in> B" 

256 
with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)" 

257 
unfolding mem_Times_iff by (auto intro: open_Times) 

258 
next 

259 
fix S assume "open S" "x \<in> S" 

260 
from open_prod_elim[OF this] guess a' b' . 

261 
moreover with A(4)[of a'] B(4)[of b'] 

262 
obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto 

263 
ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S" 

264 
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) 

265 
qed (simp add: A B) 

266 
qed 

267 

268 
instance metric_space \<subseteq> first_countable_topology 

269 
proof 

270 
fix x :: 'a 

271 
show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))" 

272 
proof (intro exI, safe) 

273 
fix S assume "open S" "x \<in> S" 

274 
then obtain r where "0 < r" "{y. dist x y < r} \<subseteq> S" 

275 
by (auto simp: open_dist dist_commute subset_eq) 

276 
moreover from reals_Archimedean[OF `0 < r`] guess n .. 

277 
moreover 

278 
then have "{y. dist x y < inverse (Suc n)} \<subseteq> {y. dist x y < r}" 

279 
by (auto simp: inverse_eq_divide) 

280 
ultimately show "\<exists>a\<in>range (\<lambda>n. {y. dist x y < inverse (Suc n)}). a \<subseteq> S" 

281 
by auto 

282 
qed (auto intro: open_ball) 

283 
qed 

284 

50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset

285 
class second_countable_topology = topological_space + 
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

286 
assumes ex_countable_subbasis: "\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

287 
begin 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

288 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

289 
lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

290 
proof  
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

291 
from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" by blast 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

292 
let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

293 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

294 
show ?thesis 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

295 
proof (intro exI conjI) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

296 
show "countable ?B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

297 
by (intro countable_image countable_Collect_finite_subset B) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

298 
{ fix S assume "open S" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

299 
then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

300 
unfolding B 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

301 
proof induct 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

302 
case UNIV show ?case by (intro exI[of _ "{{}}"]) simp 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

303 
next 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

304 
case (Int a b) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

305 
then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

306 
and y: "b = UNION y Inter" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

307 
by blast 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

308 
show ?case 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

309 
unfolding x y Int_UN_distrib2 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

310 
by (intro exI[of _ "{i \<union> j i j. i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2)) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

311 
next 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

312 
case (UN K) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

313 
then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

314 
then guess k unfolding bchoice_iff .. 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

315 
then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

316 
by (intro exI[of _ "UNION K k"]) auto 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

317 
next 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

318 
case (Basis S) then show ?case 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

319 
by (intro exI[of _ "{{S}}"]) auto 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

320 
qed 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

321 
then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

322 
unfolding subset_image_iff by blast } 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

323 
then show "topological_basis ?B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

324 
unfolding topological_space_class.topological_basis_def 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

325 
by (safe intro!: topological_space_class.open_Inter) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

326 
(simp_all add: B generate_topology.Basis subset_eq) 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

327 
qed 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

328 
qed 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

329 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

330 
end 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

331 

b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

332 
sublocale second_countable_topology < 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

333 
countable_basis "SOME B. countable B \<and> topological_basis B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

334 
using someI_ex[OF ex_countable_basis] 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

335 
by unfold_locales safe 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

336 

50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

337 
instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

338 
proof 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

339 
obtain A :: "'a set set" where "countable A" "topological_basis A" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

340 
using ex_countable_basis by auto 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

341 
moreover 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

342 
obtain B :: "'b set set" where "countable B" "topological_basis B" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

343 
using ex_countable_basis by auto 
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

344 
ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> open = generate_topology B" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

345 
by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset

346 
topological_basis_imp_subbasis) 
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

347 
qed 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

348 

50883  349 
instance second_countable_topology \<subseteq> first_countable_topology 
350 
proof 

351 
fix x :: 'a 

352 
def B \<equiv> "SOME B::'a set set. countable B \<and> topological_basis B" 

353 
then have B: "countable B" "topological_basis B" 

354 
using countable_basis is_basis 

355 
by (auto simp: countable_basis is_basis) 

356 
then show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))" 

357 
by (intro exI[of _ "{b\<in>B. x \<in> b}"]) 

358 
(fastforce simp: topological_space_class.topological_basis_def) 

359 
qed 

360 

50087  361 
subsection {* Polish spaces *} 
362 

363 
text {* Textbooks define Polish spaces as completely metrizable. 

364 
We assume the topology to be complete for a given metric. *} 

365 

50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset

366 
class polish_space = complete_space + second_countable_topology 
50087  367 

44517  368 
subsection {* General notion of a topology as a value *} 
33175  369 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

370 
definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))" 
49834  371 
typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" 
33175  372 
morphisms "openin" "topology" 
373 
unfolding istopology_def by blast 

374 

375 
lemma istopology_open_in[intro]: "istopology(openin U)" 

376 
using openin[of U] by blast 

377 

378 
lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

379 
using topology_inverse[unfolded mem_Collect_eq] . 
33175  380 

381 
lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U" 

382 
using topology_inverse[of U] istopology_open_in[of "topology U"] by auto 

383 

384 
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)" 

385 
proof 

49711  386 
{ assume "T1=T2" 
387 
hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp } 

33175  388 
moreover 
49711  389 
{ assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

390 
hence "openin T1 = openin T2" by (simp add: fun_eq_iff) 
33175  391 
hence "topology (openin T1) = topology (openin T2)" by simp 
49711  392 
hence "T1 = T2" unfolding openin_inverse . 
393 
} 

33175  394 
ultimately show ?thesis by blast 
395 
qed 

396 

397 
text{* Infer the "universe" from union of all sets in the topology. *} 

398 

399 
definition "topspace T = \<Union>{S. openin T S}" 

400 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

401 
subsubsection {* Main properties of open sets *} 
33175  402 

403 
lemma openin_clauses: 

404 
fixes U :: "'a topology" 

405 
shows "openin U {}" 

406 
"\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)" 

407 
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

408 
using openin[of U] unfolding istopology_def mem_Collect_eq 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

409 
by fast+ 
33175  410 

411 
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U" 

412 
unfolding topspace_def by blast 

413 
lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses) 

414 

415 
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)" 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

416 
using openin_clauses by simp 
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

417 

06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

418 
lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)" 
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36360
diff
changeset

419 
using openin_clauses by simp 
33175  420 

421 
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)" 

422 
using openin_Union[of "{S,T}" U] by auto 

423 

424 
lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def) 

425 

49711  426 
lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)" 
427 
(is "?lhs \<longleftrightarrow> ?rhs") 

36584  428 
proof 
49711  429 
assume ?lhs 
430 
then show ?rhs by auto 

36584  431 
next 
432 
assume H: ?rhs 

433 
let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}" 

434 
have "openin U ?t" by (simp add: openin_Union) 

435 
also have "?t = S" using H by auto 

436 
finally show "openin U S" . 

33175  437 
qed 
438 

49711  439 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

440 
subsubsection {* Closed sets *} 
33175  441 

442 
definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U  S)" 

443 

444 
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" by (metis closedin_def) 

445 
lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def) 

446 
lemma closedin_topspace[intro,simp]: 

447 
"closedin U (topspace U)" by (simp add: closedin_def) 

448 
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)" 

449 
by (auto simp add: Diff_Un closedin_def) 

450 

451 
lemma Diff_Inter[intro]: "A  \<Inter>S = \<Union> {A  ss. s\<in>S}" by auto 

452 
lemma closedin_Inter[intro]: assumes Ke: "K \<noteq> {}" and Kc: "\<forall>S \<in>K. closedin U S" 

453 
shows "closedin U (\<Inter> K)" using Ke Kc unfolding closedin_def Diff_Inter by auto 

454 

455 
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" 

456 
using closedin_Inter[of "{S,T}" U] by auto 

457 

458 
lemma Diff_Diff_Int: "A  (A  B) = A \<inter> B" by blast 

459 
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U  S)" 

460 
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) 

461 
apply (metis openin_subset subset_eq) 

462 
done 

463 

464 
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U  S))" 

465 
by (simp add: openin_closedin_eq) 

466 

467 
lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S  T)" 

468 
proof 

469 
have "S  T = S \<inter> (topspace U  T)" using openin_subset[of U S] oS cT 

470 
by (auto simp add: topspace_def openin_subset) 

471 
then show ?thesis using oS cT by (auto simp add: closedin_def) 

472 
qed 

473 

474 
lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S  T)" 

475 
proof 

476 
have "S  T = S \<inter> (topspace U  T)" using closedin_subset[of U S] oS cT 

477 
by (auto simp add: topspace_def ) 

478 
then show ?thesis using oS cT by (auto simp add: openin_closedin_eq) 

479 
qed 

480 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

481 
subsubsection {* Subspace topology *} 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

482 

510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

483 
definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

484 

510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

485 
lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

486 
(is "istopology ?L") 
33175  487 
proof 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

488 
have "?L {}" by blast 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

489 
{fix A B assume A: "?L A" and B: "?L B" 
33175  490 
from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" by blast 
491 
have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" using Sa Sb by blast+ 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

492 
then have "?L (A \<inter> B)" by blast} 
33175  493 
moreover 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

494 
{fix K assume K: "K \<subseteq> Collect ?L" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

495 
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

496 
apply (rule set_eqI) 
33175  497 
apply (simp add: Ball_def image_iff) 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

498 
by metis 
33175  499 
from K[unfolded th0 subset_image_iff] 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

500 
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast 
33175  501 
have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

502 
moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq) 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

503 
ultimately have "?L (\<Union>K)" by blast} 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

504 
ultimately show ?thesis 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

505 
unfolding subset_eq mem_Collect_eq istopology_def by blast 
33175  506 
qed 
507 

508 
lemma openin_subtopology: 

509 
"openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))" 

510 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

511 
by auto 
33175  512 

513 
lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V" 

514 
by (auto simp add: topspace_def openin_subtopology) 

515 

516 
lemma closedin_subtopology: 

517 
"closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" 

518 
unfolding closedin_def topspace_subtopology 

519 
apply (simp add: openin_subtopology) 

520 
apply (rule iffI) 

521 
apply clarify 

522 
apply (rule_tac x="topspace U  T" in exI) 

523 
by auto 

524 

525 
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U" 

526 
unfolding openin_subtopology 

527 
apply (rule iffI, clarify) 

528 
apply (frule openin_subset[of U]) apply blast 

529 
apply (rule exI[where x="topspace U"]) 

49711  530 
apply auto 
531 
done 

532 

533 
lemma subtopology_superset: 

534 
assumes UV: "topspace U \<subseteq> V" 

33175  535 
shows "subtopology U V = U" 
536 
proof 

537 
{fix S 

538 
{fix T assume T: "openin U T" "S = T \<inter> V" 

539 
from T openin_subset[OF T(1)] UV have eq: "S = T" by blast 

540 
have "openin U S" unfolding eq using T by blast} 

541 
moreover 

542 
{assume S: "openin U S" 

543 
hence "\<exists>T. openin U T \<and> S = T \<inter> V" 

544 
using openin_subset[OF S] UV by auto} 

545 
ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" by blast} 

546 
then show ?thesis unfolding topology_eq openin_subtopology by blast 

547 
qed 

548 

549 
lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" 

550 
by (simp add: subtopology_superset) 

551 

552 
lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" 

553 
by (simp add: subtopology_superset) 

554 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

555 
subsubsection {* The standard Euclidean topology *} 
33175  556 

557 
definition 

558 
euclidean :: "'a::topological_space topology" where 

559 
"euclidean = topology open" 

560 

561 
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S" 

562 
unfolding euclidean_def 

563 
apply (rule cong[where x=S and y=S]) 

564 
apply (rule topology_inverse[symmetric]) 

565 
apply (auto simp add: istopology_def) 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

566 
done 
33175  567 

568 
lemma topspace_euclidean: "topspace euclidean = UNIV" 

569 
apply (simp add: topspace_def) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

570 
apply (rule set_eqI) 
33175  571 
by (auto simp add: open_openin[symmetric]) 
572 

573 
lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S" 

574 
by (simp add: topspace_euclidean topspace_subtopology) 

575 

576 
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S" 

577 
by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV) 

578 

579 
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" 

580 
by (simp add: open_openin openin_subopen[symmetric]) 

581 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

582 
text {* Basic "localization" results are handy for connectedness. *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

583 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

584 
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

585 
by (auto simp add: openin_subtopology open_openin[symmetric]) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

586 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

587 
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

588 
by (auto simp add: openin_open) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

589 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

590 
lemma open_openin_trans[trans]: 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

591 
"open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

592 
by (metis Int_absorb1 openin_open_Int) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

593 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

594 
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

595 
by (auto simp add: openin_open) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

596 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

597 
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

598 
by (simp add: closedin_subtopology closed_closedin Int_ac) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

599 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

600 
lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

601 
by (metis closedin_closed) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

602 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

603 
lemma closed_closedin_trans: "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

604 
apply (subgoal_tac "S \<inter> T = T" ) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

605 
apply auto 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

606 
apply (frule closedin_closed_Int[of T S]) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

607 
by simp 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

608 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

609 
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

610 
by (auto simp add: closedin_closed) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

611 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

612 
lemma openin_euclidean_subtopology_iff: 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

613 
fixes S U :: "'a::metric_space set" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

614 
shows "openin (subtopology euclidean U) S 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

615 
\<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs") 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

616 
proof 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

617 
assume ?lhs thus ?rhs unfolding openin_open open_dist by blast 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

618 
next 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

619 
def T \<equiv> "{x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

620 
have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

621 
unfolding T_def 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

622 
apply clarsimp 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

623 
apply (rule_tac x="d  dist x a" in exI) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

624 
apply (clarsimp simp add: less_diff_eq) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

625 
apply (erule rev_bexI) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

626 
apply (rule_tac x=d in exI, clarify) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

627 
apply (erule le_less_trans [OF dist_triangle]) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

628 
done 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

629 
assume ?rhs hence 2: "S = U \<inter> T" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

630 
unfolding T_def 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

631 
apply auto 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

632 
apply (drule (1) bspec, erule rev_bexI) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

633 
apply auto 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

634 
done 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

635 
from 1 2 show ?lhs 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

636 
unfolding openin_open open_dist by fast 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

637 
qed 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

638 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

639 
text {* These "transitivity" results are handy too *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

640 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

641 
lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

642 
\<Longrightarrow> openin (subtopology euclidean U) S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

643 
unfolding open_openin openin_open by blast 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

644 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

645 
lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

646 
by (auto simp add: openin_open intro: openin_trans) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

647 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

648 
lemma closedin_trans[trans]: 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

649 
"closedin (subtopology euclidean T) S \<Longrightarrow> 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

650 
closedin (subtopology euclidean U) T 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

651 
==> closedin (subtopology euclidean U) S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

652 
by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

653 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

654 
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S" 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

655 
by (auto simp add: closedin_closed intro: closedin_trans) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

656 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

657 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

658 
subsection {* Open and closed balls *} 
33175  659 

660 
definition 

661 
ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where 

662 
"ball x e = {y. dist x y < e}" 

663 

664 
definition 

665 
cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where 

666 
"cball x e = {y. dist x y \<le> e}" 

667 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

668 
lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

669 
by (simp add: ball_def) 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

670 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

671 
lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

672 
by (simp add: cball_def) 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

673 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

674 
lemma mem_ball_0: 
33175  675 
fixes x :: "'a::real_normed_vector" 
676 
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e" 

677 
by (simp add: dist_norm) 

678 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

679 
lemma mem_cball_0: 
33175  680 
fixes x :: "'a::real_normed_vector" 
681 
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" 

682 
by (simp add: dist_norm) 

683 

45776
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

684 
lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

685 
by simp 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

686 

714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

687 
lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e" 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

688 
by simp 
714100f5fda4
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman
parents:
45548
diff
changeset

689 

33175  690 
lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq) 
691 
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq) 

692 
lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq) 

693 
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

694 
by (simp add: set_eq_iff) arith 
33175  695 

696 
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

697 
by (simp add: set_eq_iff) 
33175  698 

699 
lemma diff_less_iff: "(a::real)  b > 0 \<longleftrightarrow> a > b" 

700 
"(a::real)  b < 0 \<longleftrightarrow> a < b" 

701 
"a  b < c \<longleftrightarrow> a < c +b" "a  b > c \<longleftrightarrow> a > c +b" by arith+ 

702 
lemma diff_le_iff: "(a::real)  b \<ge> 0 \<longleftrightarrow> a \<ge> b" "(a::real)  b \<le> 0 \<longleftrightarrow> a \<le> b" 

703 
"a  b \<le> c \<longleftrightarrow> a \<le> c +b" "a  b \<ge> c \<longleftrightarrow> a \<ge> c +b" by arith+ 

704 

705 
lemma open_ball[intro, simp]: "open (ball x e)" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

706 
unfolding open_dist ball_def mem_Collect_eq Ball_def 
33175  707 
unfolding dist_commute 
708 
apply clarify 

709 
apply (rule_tac x="e  dist xa x" in exI) 

710 
using dist_triangle_alt[where z=x] 

711 
apply (clarsimp simp add: diff_less_iff) 

712 
apply atomize 

713 
apply (erule_tac x="y" in allE) 

714 
apply (erule_tac x="xa" in allE) 

715 
by arith 

716 

717 
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)" 

718 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. 

719 

33714
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

720 
lemma openE[elim?]: 
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

721 
assumes "open S" "x\<in>S" 
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

722 
obtains e where "e>0" "ball x e \<subseteq> S" 
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

723 
using assms unfolding open_contains_ball by auto 
eb2574ac4173
Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents:
33324
diff
changeset

724 

33175  725 
lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)" 
726 
by (metis open_contains_ball subset_eq centre_in_ball) 

727 

728 
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

729 
unfolding mem_ball set_eq_iff 
33175  730 
apply (simp add: not_less) 
731 
by (metis zero_le_dist order_trans dist_self) 

732 

733 
lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp 

734 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

735 
lemma euclidean_dist_l2: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

736 
fixes x y :: "'a :: euclidean_space" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

737 
shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

738 
unfolding dist_norm norm_eq_sqrt_inner setL2_def 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

739 
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

740 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

741 
definition "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

742 

50087  743 
lemma rational_boxes: 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

744 
fixes x :: "'a\<Colon>euclidean_space" 
50087  745 
assumes "0 < e" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

746 
shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e" 
50087  747 
proof  
748 
def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

749 
then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos simp: DIM_positive) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

750 
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i  y < e'" (is "\<forall>i. ?th i") 
50087  751 
proof 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

752 
fix i from Rats_dense_in_real[of "x \<bullet> i  e'" "x \<bullet> i"] e show "?th i" by auto 
50087  753 
qed 
754 
from choice[OF this] guess a .. note a = this 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

755 
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y  x \<bullet> i < e'" (is "\<forall>i. ?th i") 
50087  756 
proof 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

757 
fix i from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e show "?th i" by auto 
50087  758 
qed 
759 
from choice[OF this] guess b .. note b = this 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

760 
let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

761 
show ?thesis 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

762 
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

763 
fix y :: 'a assume *: "y \<in> box ?a ?b" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

764 
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<twosuperior>)" 
50087  765 
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

766 
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))" 
50087  767 
proof (rule real_sqrt_less_mono, rule setsum_strict_mono) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

768 
fix i :: "'a" assume i: "i \<in> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

769 
have "a i < y\<bullet>i \<and> y\<bullet>i < b i" using * i by (auto simp: box_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

770 
moreover have "a i < x\<bullet>i" "x\<bullet>i  a i < e'" using a by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

771 
moreover have "x\<bullet>i < b i" "b i  x\<bullet>i < e'" using b by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

772 
ultimately have "\<bar>x\<bullet>i  y\<bullet>i\<bar> < 2 * e'" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

773 
then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" 
50087  774 
unfolding e'_def by (auto simp: dist_real_def) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

775 
then have "(dist (x \<bullet> i) (y \<bullet> i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>" 
50087  776 
by (rule power_strict_mono) auto 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

777 
then show "(dist (x \<bullet> i) (y \<bullet> i))\<twosuperior> < e\<twosuperior> / real DIM('a)" 
50087  778 
by (simp add: power_divide) 
779 
qed auto 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

780 
also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

781 
finally show "y \<in> ball x e" by (auto simp: ball_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

782 
qed (insert a b, auto simp: box_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

783 
qed 
51103  784 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

785 
lemma open_UNION_box: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

786 
fixes M :: "'a\<Colon>euclidean_space set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

787 
assumes "open M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

788 
defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

789 
defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

790 
defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^isub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

791 
shows "M = (\<Union>f\<in>I. box (a' f) (b' f))" 
50087  792 
proof safe 
793 
fix x assume "x \<in> M" 

794 
obtain e where e: "e > 0" "ball x e \<subseteq> M" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

795 
using openE[OF `open M` `x \<in> M`] by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

796 
moreover then obtain a b where ab: "x \<in> box a b" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

797 
"\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>" "box a b \<subseteq> ball x e" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

798 
using rational_boxes[OF e(1)] by metis 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

799 
ultimately show "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

800 
by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

801 
(auto simp: euclidean_representation I_def a'_def b'_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset

802 
qed (auto simp: I_def) 
33175  803 

804 
subsection{* Connectedness *} 

805 

806 
definition "connected S \<longleftrightarrow> 

807 
~(\<exists>e1 e2. open e1 \<and> open e2 \<and> S \<subseteq> (e1 \<union> e2) \<and> (e1 \<inter> e2 \<inter> S = {}) 

808 
\<and> ~(e1 \<inter> S = {}) \<and> ~(e2 \<inter> S = {}))" 

809 

810 
lemma connected_local: 

811 
"connected S \<longleftrightarrow> ~(\<exists>e1 e2. 

812 
openin (subtopology euclidean S) e1 \<and> 

813 
openin (subtopology euclidean S) e2 \<and> 

814 
S \<subseteq> e1 \<union> e2 \<and> 

815 
e1 \<inter> e2 = {} \<and> 

816 
~(e1 = {}) \<and> 

817 
~(e2 = {}))" 

818 
unfolding connected_def openin_open by (safe, blast+) 

819 

34105  820 
lemma exists_diff: 
821 
fixes P :: "'a set \<Rightarrow> bool" 

822 
shows "(\<exists>S. P( S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs") 

33175  823 
proof 
824 
{assume "?lhs" hence ?rhs by blast } 

825 
moreover 

826 
{fix S assume H: "P S" 

34105  827 
have "S =  ( S)" by auto 
828 
with H have "P ( ( S))" by metis } 

33175  829 
ultimately show ?thesis by metis 
830 
qed 

831 

832 
lemma connected_clopen: "connected S \<longleftrightarrow> 

833 
(\<forall>T. openin (subtopology euclidean S) T \<and> 

834 
closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs") 

835 
proof 

34105  836 
have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open ( e2) \<and> S \<subseteq> e1 \<union> ( e2) \<and> e1 \<inter> ( e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> ( e2) \<inter> S \<noteq> {})" 
33175  837 
unfolding connected_def openin_open closedin_closed 
838 
apply (subst exists_diff) by blast 

34105  839 
hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> ( e2) \<and> e1 \<inter> ( e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> ( e2) \<inter> S \<noteq> {})" 
840 
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis 

33175  841 

842 
have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))" 

843 
(is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)") 

844 
unfolding connected_def openin_open closedin_closed by auto 

845 
{fix e2 

846 
{fix e1 have "?P e2 e1 \<longleftrightarrow> (\<exists>t. closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t\<noteq>S)" 

847 
by auto} 

848 
then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by metis} 

849 
then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by blast 

850 
then show ?thesis unfolding th0 th1 by simp 

851 
qed 

852 

853 
lemma connected_empty[simp, intro]: "connected {}" 

854 
by (simp add: connected_def) 

855 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

856 

33175  857 
subsection{* Limit points *} 
858 

44207
ea99698c2070
localeize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
huffman
parents:
44170
diff
changeset

859 
definition (in topological_space) 
ea99698c2070
localeize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
huffman
parents:
44170
diff
changeset

860 
islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where 
33175  861 
"x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))" 
862 

863 
lemma islimptI: 

864 
assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" 

865 
shows "x islimpt S" 

866 
using assms unfolding islimpt_def by auto 

867 

868 
lemma islimptE: 

869 
assumes "x islimpt S" and "x \<in> T" and "open T" 

870 
obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x" 

871 
using assms unfolding islimpt_def by auto 

872 

44584  873 
lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)" 
874 
unfolding islimpt_def eventually_at_topological by auto 

875 

876 
lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T" 

877 
unfolding islimpt_def by fast 

33175  878 

879 
lemma islimpt_approachable: 

880 
fixes x :: "'a::metric_space" 

881 
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)" 

44584  882 
unfolding islimpt_iff_eventually eventually_at by fast 
33175  883 

884 
lemma islimpt_approachable_le: 

885 
fixes x :: "'a::metric_space" 

886 
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)" 

887 
unfolding islimpt_approachable 

44584  888 
using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x", 
889 
THEN arg_cong [where f=Not]] 

890 
by (simp add: Bex_def conj_commute conj_left_commute) 

33175  891 

44571  892 
lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}" 
893 
unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast) 

894 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

895 
text {* A perfect space has no isolated points. *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

896 

44571  897 
lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV" 
898 
unfolding islimpt_UNIV_iff by (rule not_open_singleton) 

33175  899 

900 
lemma perfect_choose_dist: 

44072
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

901 
fixes x :: "'a::{perfect_space, metric_space}" 
33175  902 
shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r" 
903 
using islimpt_UNIV [of x] 

904 
by (simp add: islimpt_approachable) 

905 

906 
lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)" 

907 
unfolding closed_def 

908 
apply (subst open_subopen) 

34105  909 
apply (simp add: islimpt_def subset_eq) 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

910 
by (metis ComplE ComplI) 
33175  911 

912 
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" 

913 
unfolding islimpt_def by auto 

914 

915 
lemma finite_set_avoid: 

916 
fixes a :: "'a::metric_space" 

917 
assumes fS: "finite S" shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x" 

918 
proof(induct rule: finite_induct[OF fS]) 

41863  919 
case 1 thus ?case by (auto intro: zero_less_one) 
33175  920 
next 
921 
case (2 x F) 

922 
from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" by blast 

923 
{assume "x = a" hence ?case using d by auto } 

924 
moreover 

925 
{assume xa: "x\<noteq>a" 

926 
let ?d = "min d (dist a x)" 

927 
have dp: "?d > 0" using xa d(1) using dist_nz by auto 

928 
from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" by auto 

929 
with dp xa have ?case by(auto intro!: exI[where x="?d"]) } 

930 
ultimately show ?case by blast 

931 
qed 

932 

933 
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T" 

50897
078590669527
generalize lemma islimpt_finite to class t1_space
huffman
parents:
50884
diff
changeset

934 
by (simp add: islimpt_iff_eventually eventually_conj_iff) 
33175  935 

936 
lemma discrete_imp_closed: 

937 
fixes S :: "'a::metric_space set" 

938 
assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x" 

939 
shows "closed S" 

940 
proof 

941 
{fix x assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" 

942 
from e have e2: "e/2 > 0" by arith 

943 
from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" by blast 

944 
let ?m = "min (e/2) (dist x y) " 

945 
from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym]) 

946 
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast 

947 
have th: "dist z y < e" using z y 

948 
by (intro dist_triangle_lt [where z=x], simp) 

949 
from d[rule_format, OF y(1) z(1) th] y z 

950 
have False by (auto simp add: dist_commute)} 

951 
then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) 

952 
qed 

953 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

954 

eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

955 
subsection {* Interior of a Set *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

956 

44519  957 
definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}" 
958 

959 
lemma interiorI [intro?]: 

960 
assumes "open T" and "x \<in> T" and "T \<subseteq> S" 

961 
shows "x \<in> interior S" 

962 
using assms unfolding interior_def by fast 

963 

964 
lemma interiorE [elim?]: 

965 
assumes "x \<in> interior S" 

966 
obtains T where "open T" and "x \<in> T" and "T \<subseteq> S" 

967 
using assms unfolding interior_def by fast 

968 

969 
lemma open_interior [simp, intro]: "open (interior S)" 

970 
by (simp add: interior_def open_Union) 

971 

972 
lemma interior_subset: "interior S \<subseteq> S" 

973 
by (auto simp add: interior_def) 

974 

975 
lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S" 

976 
by (auto simp add: interior_def) 

977 

978 
lemma interior_open: "open S \<Longrightarrow> interior S = S" 

979 
by (intro equalityI interior_subset interior_maximal subset_refl) 

33175  980 

981 
lemma interior_eq: "interior S = S \<longleftrightarrow> open S" 

44519  982 
by (metis open_interior interior_open) 
983 

984 
lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T" 

33175  985 
by (metis interior_maximal interior_subset subset_trans) 
986 

44519  987 
lemma interior_empty [simp]: "interior {} = {}" 
988 
using open_empty by (rule interior_open) 

989 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

990 
lemma interior_UNIV [simp]: "interior UNIV = UNIV" 
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

991 
using open_UNIV by (rule interior_open) 
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

992 

44519  993 
lemma interior_interior [simp]: "interior (interior S) = interior S" 
994 
using open_interior by (rule interior_open) 

995 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

996 
lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T" 
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

997 
by (auto simp add: interior_def) 
44519  998 

999 
lemma interior_unique: 

1000 
assumes "T \<subseteq> S" and "open T" 

1001 
assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T" 

1002 
shows "interior S = T" 

1003 
by (intro equalityI assms interior_subset open_interior interior_maximal) 

1004 

1005 
lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T" 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1006 
by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1 
44519  1007 
Int_lower2 interior_maximal interior_subset open_Int open_interior) 
1008 

1009 
lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)" 

1010 
using open_contains_ball_eq [where S="interior S"] 

1011 
by (simp add: open_subset_interior) 

33175  1012 

1013 
lemma interior_limit_point [intro]: 

1014 
fixes x :: "'a::perfect_space" 

1015 
assumes x: "x \<in> interior S" shows "x islimpt S" 

44072
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1016 
using x islimpt_UNIV [of x] 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1017 
unfolding interior_def islimpt_def 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1018 
apply (clarsimp, rename_tac T T') 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1019 
apply (drule_tac x="T \<inter> T'" in spec) 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1020 
apply (auto simp add: open_Int) 
5b970711fb39
class perfect_space inherits from topological_space;
huffman
parents:
43338
diff
changeset

1021 
done 
33175  1022 

1023 
lemma interior_closed_Un_empty_interior: 

1024 
assumes cS: "closed S" and iT: "interior T = {}" 

44519  1025 
shows "interior (S \<union> T) = interior S" 
33175  1026 
proof 
44519  1027 
show "interior S \<subseteq> interior (S \<union> T)" 
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1028 
by (rule interior_mono, rule Un_upper1) 
33175  1029 
next 
1030 
show "interior (S \<union> T) \<subseteq> interior S" 

1031 
proof 

1032 
fix x assume "x \<in> interior (S \<union> T)" 

44519  1033 
then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" .. 
33175  1034 
show "x \<in> interior S" 
1035 
proof (rule ccontr) 

1036 
assume "x \<notin> interior S" 

1037 
with `x \<in> R` `open R` obtain y where "y \<in> R  S" 

44519  1038 
unfolding interior_def by fast 
33175  1039 
from `open R` `closed S` have "open (R  S)" by (rule open_Diff) 
1040 
from `R \<subseteq> S \<union> T` have "R  S \<subseteq> T" by fast 

1041 
from `y \<in> R  S` `open (R  S)` `R  S \<subseteq> T` `interior T = {}` 

1042 
show "False" unfolding interior_def by fast 

1043 
qed 

1044 
qed 

1045 
qed 

1046 

44365  1047 
lemma interior_Times: "interior (A \<times> B) = interior A \<times> interior B" 
1048 
proof (rule interior_unique) 

1049 
show "interior A \<times> interior B \<subseteq> A \<times> B" 

1050 
by (intro Sigma_mono interior_subset) 

1051 
show "open (interior A \<times> interior B)" 

1052 
by (intro open_Times open_interior) 

44519  1053 
fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B" 
1054 
proof (safe) 

1055 
fix x y assume "(x, y) \<in> T" 

1056 
then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D" 

1057 
using `open T` unfolding open_prod_def by fast 

1058 
hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D" 

1059 
using `T \<subseteq> A \<times> B` by auto 

1060 
thus "x \<in> interior A" and "y \<in> interior B" 

1061 
by (auto intro: interiorI) 

1062 
qed 

44365  1063 
qed 
1064 

33175  1065 

44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1066 
subsection {* Closure of a Set *} 
33175  1067 

1068 
definition "closure S = S \<union> {x  x. x islimpt S}" 

1069 

44518  1070 
lemma interior_closure: "interior S =  (closure ( S))" 
1071 
unfolding interior_def closure_def islimpt_def by auto 

1072 

34105  1073 
lemma closure_interior: "closure S =  interior ( S)" 
44518  1074 
unfolding interior_closure by simp 
33175  1075 

1076 
lemma closed_closure[simp, intro]: "closed (closure S)" 

44518  1077 
unfolding closure_interior by (simp add: closed_Compl) 
1078 

1079 
lemma closure_subset: "S \<subseteq> closure S" 

1080 
unfolding closure_def by simp 

33175  1081 

1082 
lemma closure_hull: "closure S = closed hull S" 

44519  1083 
unfolding hull_def closure_interior interior_def by auto 
33175  1084 

1085 
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S" 

44519  1086 
unfolding closure_hull using closed_Inter by (rule hull_eq) 
1087 

1088 
lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S" 

1089 
unfolding closure_eq . 

1090 

1091 
lemma closure_closure [simp]: "closure (closure S) = closure S" 

44518  1092 
unfolding closure_hull by (rule hull_hull) 
33175  1093 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1094 
lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T" 
44518  1095 
unfolding closure_hull by (rule hull_mono) 
33175  1096 

44519  1097 
lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T" 
44518  1098 
unfolding closure_hull by (rule hull_minimal) 
33175  1099 

44519  1100 
lemma closure_unique: 
1101 
assumes "S \<subseteq> T" and "closed T" 

1102 
assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'" 

1103 
shows "closure S = T" 

1104 
using assms unfolding closure_hull by (rule hull_unique) 

1105 

1106 
lemma closure_empty [simp]: "closure {} = {}" 

44518  1107 
using closed_empty by (rule closure_closed) 
33175  1108 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44519
diff
changeset

1109 
lemma closure_UNIV [simp]: "closure UNIV = UNIV" 
44518  1110 
using closed_UNIV by (rule closure_closed) 
1111 

1112 
lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T" 

1113 
unfolding closure_interior by simp 

33175  1114 

1115 
lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}" 

1116 
using closure_empty closure_subset[of S] 

1117 
by blast 

1118 

1119 
lemma closure_subset_eq: "closure S \<subseteq> S \<longleftrightarrow> closed S" 

1120 
using closure_eq[of S] closure_subset[of S] 

1121 
by simp 

1122 

1123 
lemma open_inter_closure_eq_empty: 

1124 
"open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}" 

34105  1125 
using open_subset_interior[of S " T"] 
1126 
using interior_subset[of " T"] 

33175  1127 
unfolding closure_interior 
1128 
by auto 

1129 

1130 
lemma open_inter_closure_subset: 

1131 
"open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)" 

1132 
proof 

1133 
fix x 

1134 
assume as: "open S" "x \<in> S \<inter> closure T" 

1135 
{ assume *:"x islimpt T" 

1136 
have "x islimpt (S \<inter> T)" 

1137 
proof (rule islimptI) 

1138 
fix A 

1139 
assume "x \<in> A" "open A" 

1140 
with as have "x \<in> A \<inter> S" "open (A \<inter> S)" 

1141 
by (simp_all add: open_Int) 

1142 
with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x" 

1143 
by (rule islimptE) 

1144 
hence "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x" 

1145 
by simp_all 

1146 
thus "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" .. 

1147 
qed 

1148 
} 

1149 
then show "x \<in> closure (S \<inter> T)" using as 

1150 
unfolding closure_def 

1151 
by blast 

1152 
qed 

1153 

44519  1154 
lemma closure_complement: "closure ( S) =  interior S" 
44518  1155 
unfolding closure_interior by simp 
33175  1156 

44519  1157 
lemma interior_complement: "interior ( S) =  closure S" 
44518  1158 
unfolding closure_interior by simp 
33175  1159 

44365  1160 
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B" 
44519  1161 
proof (rule closure_unique) 
44365  1162 
show "A \<times> B \<subseteq> closure A \<times> closure B" 
1163 
by (intro Sigma_mono closure_subset) 

1164 
show "closed (closure A \<times> closure B)" 

1165 
by (intro closed_Times closed_closure) 

44519  1166 
fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T" 
44365  1167 
apply (simp add: closed_def open_prod_def, clarify) 
1168 
apply (rule ccontr) 

1169 
apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D) 

1170 
apply (simp add: closure_interior interior_def) 

1171 
apply (drule_tac x=C in spec) 

5daa55003649
add le 