author  hoelzl 
Fri, 18 Jan 2013 20:01:41 +0100  
changeset 50972  d2c6a0a7fcdf 
parent 50971  5e3d3d690975 
child 50973  4a2c82644889 
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 

50942  31 
(* TODO: Move this to RComplete.thy  would need to include Glb into RComplete *) 
32 
lemma real_isGlb_unique: "[ isGlb R S x; isGlb R S y ] ==> x = (y::real)" 

33 
apply (frule isGlb_isLb) 

34 
apply (frule_tac x = y in isGlb_isLb) 

35 
apply (blast intro!: order_antisym dest!: isGlb_le_isLb) 

36 
done 

37 

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

38 
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

39 
"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

40 
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

41 

50087  42 
subsection {* Topological Basis *} 
43 

44 
context topological_space 

45 
begin 

46 

47 
definition "topological_basis B = 

48 
((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))" 

49 

50 
lemma topological_basis_iff: 

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

52 
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'))" 

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

54 
proof safe 

55 
fix O' and x::'a 

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

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

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

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

60 
next 

61 
assume H: ?rhs 

62 
show "topological_basis B" using assms unfolding topological_basis_def 

63 
proof safe 

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

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

66 
by (force intro: bchoice simp: Bex_def) 

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

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

69 
qed 

70 
qed 

71 

72 
lemma topological_basisI: 

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

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

75 
shows "topological_basis B" 

76 
using assms by (subst topological_basis_iff) auto 

77 

78 
lemma topological_basisE: 

79 
fixes O' 

80 
assumes "topological_basis B" 

81 
assumes "open O'" 

82 
assumes "x \<in> O'" 

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

84 
proof atomize_elim 

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

86 
with topological_basis_iff assms 

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

88 
qed 

89 

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

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

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

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

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

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

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

96 

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

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

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

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

100 
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

101 
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

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

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

104 
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

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

106 
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

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

108 

50087  109 
end 
110 

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

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

112 
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

113 
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

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

115 
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

116 
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

117 
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

118 
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

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

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

121 
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

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

123 
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

124 
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

125 
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

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

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

128 
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

129 

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

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

131 

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

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

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

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

135 
assumes countable_basis: "countable B" 
33175  136 
begin 
137 

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

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

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

141 
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

142 

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

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

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

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

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

147 

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

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

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

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

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

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

154 
by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI) 
50087  155 
qed 
156 

157 
lemma countable_dense_setE: 

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

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

159 
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

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

161 

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

162 
text {* Construction of an increasing sequence approximating open sets, 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

163 
therefore basis which is closed under union. *} 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

164 

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

165 
definition union_closed_basis::"'a set set" where 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

166 
"union_closed_basis = (\<lambda>l. \<Union>set l) ` lists B" 
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 basis_union_closed_basis: "topological_basis union_closed_basis" 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

169 
proof (rule topological_basisI) 
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

170 
fix O' and x::'a assume "open O'" "x \<in> O'" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

171 
from topological_basisE[OF is_basis this] guess B' . note B' = this 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

172 
thus "\<exists>B'\<in>union_closed_basis. x \<in> B' \<and> B' \<subseteq> O'" unfolding union_closed_basis_def 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

173 
by (auto intro!: bexI[where x="[B']"]) 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

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

175 
fix B' assume "B' \<in> union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

176 
thus "open B'" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

177 
using topological_basis_open[OF is_basis] 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

178 
by (auto simp: union_closed_basis_def) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

180 

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

181 
lemma countable_union_closed_basis: "countable union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

182 
unfolding union_closed_basis_def using countable_basis by simp 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

183 

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

184 
lemmas open_union_closed_basis = topological_basis_open[OF basis_union_closed_basis] 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

185 

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

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

187 
assumes X: "X \<in> union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

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

190 
from X obtain l where "\<And>x. x\<in>set l \<Longrightarrow> x\<in>B" "X = \<Union>set l" by (auto simp: union_closed_basis_def) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

191 
thus ?thesis by auto 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

193 

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

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

195 
assumes "X \<in> union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

196 
obtains B' where "finite B'" "X = \<Union>B'" "B' \<subseteq> B" using union_closed_basis_ex[OF assms] by blast 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

197 

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

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

199 
assumes "finite B'" "X = \<Union>B'" "B' \<subseteq> B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

200 
shows "X \<in> union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

202 
from finite_list[OF `finite B'`] guess l .. 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

203 
thus ?thesis using assms unfolding union_closed_basis_def by (auto intro!: image_eqI[where x=l]) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

205 

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

206 
lemma empty_basisI[intro]: "{} \<in> union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

207 
by (rule union_closed_basisI[of "{}"]) auto 
50087  208 

209 
lemma union_basisI[intro]: 

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

210 
assumes "X \<in> union_closed_basis" "Y \<in> union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

211 
shows "X \<union> Y \<in> union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

212 
using assms by (auto intro: union_closed_basisI elim!:union_closed_basisE) 
50087  213 

214 
lemma open_imp_Union_of_incseq: 

215 
assumes "open X" 

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

216 
shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> union_closed_basis" 
50087  217 
proof  
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

218 
from open_countable_basis_ex[OF `open X`] 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

220 
from this(1) countable_basis have "countable B'" by (rule countable_subset) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

221 
show ?thesis 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

223 
assume "B' \<noteq> {}" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

224 
def S \<equiv> "\<lambda>n. \<Union>i\<in>{0..n}. from_nat_into B' i" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

225 
have S:"\<And>n. S n = \<Union>{from_nat_into B' ii. i\<in>{0..n}}" unfolding S_def by force 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

226 
have "incseq S" by (force simp: S_def incseq_Suc_iff) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

228 
have "(\<Union>j. S j) = X" unfolding B' 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

230 
fix x X assume "X \<in> B'" "x \<in> X" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

231 
then obtain n where "X = from_nat_into B' n" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

232 
by (metis `countable B'` from_nat_into_surj) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

233 
also have "\<dots> \<subseteq> S n" by (auto simp: S_def) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

234 
finally show "x \<in> (\<Union>j. S j)" using `x \<in> X` by auto 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

236 
fix x n 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

237 
assume "x \<in> S n" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

238 
also have "\<dots> = (\<Union>i\<in>{0..n}. from_nat_into B' i)" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

239 
by (simp add: S_def) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

240 
also have "\<dots> \<subseteq> (\<Union>i. from_nat_into B' i)" by auto 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

241 
also have "\<dots> \<subseteq> \<Union>B'" using `B' \<noteq> {}` by (auto intro: from_nat_into) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

242 
finally show "x \<in> \<Union>B'" . 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

244 
moreover have "range S \<subseteq> union_closed_basis" using B' 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

245 
by (auto intro!: union_closed_basisI[OF _ S] simp: from_nat_into `B' \<noteq> {}`) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

246 
ultimately show ?thesis by auto 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

247 
qed (auto simp: B') 
50087  248 
qed 
249 

250 
lemma open_incseqE: 

251 
assumes "open X" 

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

252 
obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> union_closed_basis" 
50087  253 
using open_imp_Union_of_incseq assms by atomize_elim 
254 

255 
end 

256 

50883  257 
class first_countable_topology = topological_space + 
258 
assumes first_countable_basis: 

259 
"\<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))" 

260 

261 
lemma (in first_countable_topology) countable_basis_at_decseq: 

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

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

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

265 
proof atomize_elim 

266 
from first_countable_basis[of x] obtain A 

267 
where "countable A" 

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

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

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

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

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

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

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

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

276 
fix i 

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

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

279 
next 

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

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

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

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

284 
by (auto simp: F_def) 

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

286 
by (auto simp: eventually_sequentially) 

287 
qed 

288 
qed 

289 

290 
lemma (in first_countable_topology) first_countable_basisE: 

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

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

293 
using first_countable_basis[of x] 

294 
by atomize_elim auto 

295 

296 
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology 

297 
proof 

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

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

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

301 
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))" 

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

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

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

305 
unfolding mem_Times_iff by (auto intro: open_Times) 

306 
next 

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

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

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

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

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

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

313 
qed (simp add: A B) 

314 
qed 

315 

316 
instance metric_space \<subseteq> first_countable_topology 

317 
proof 

318 
fix x :: 'a 

319 
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))" 

320 
proof (intro exI, safe) 

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

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

323 
by (auto simp: open_dist dist_commute subset_eq) 

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

325 
moreover 

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

327 
by (auto simp: inverse_eq_divide) 

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

329 
by auto 

330 
qed (auto intro: open_ball) 

331 
qed 

332 

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

333 
class second_countable_topology = topological_space + 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

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

335 
"\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

336 

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

337 
sublocale second_countable_topology < countable_basis "SOME B. countable B \<and> topological_basis B" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

338 
using someI_ex[OF ex_countable_basis] by unfold_locales safe 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

339 

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

340 
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

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

342 
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

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

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

345 
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

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

347 
ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B" 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

348 
by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod) 
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

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

350 

50883  351 
instance second_countable_topology \<subseteq> first_countable_topology 
352 
proof 

353 
fix x :: 'a 

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

355 
then have B: "countable B" "topological_basis B" 

356 
using countable_basis is_basis 

357 
by (auto simp: countable_basis is_basis) 

358 
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))" 

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

360 
(fastforce simp: topological_space_class.topological_basis_def) 

361 
qed 

362 

50087  363 
subsection {* Polish spaces *} 
364 

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

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

367 

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

368 
class polish_space = complete_space + second_countable_topology 
50087  369 

44517  370 
subsection {* General notion of a topology as a value *} 
33175  371 

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

372 
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  373 
typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" 
33175  374 
morphisms "openin" "topology" 
375 
unfolding istopology_def by blast 

376 

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

378 
using openin[of U] by blast 

379 

380 
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

381 
using topology_inverse[unfolded mem_Collect_eq] . 
33175  382 

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

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

385 

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

387 
proof 

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

33175  390 
moreover 
49711  391 
{ 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

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

33175  396 
ultimately show ?thesis by blast 
397 
qed 

398 

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

400 

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

402 

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

403 
subsubsection {* Main properties of open sets *} 
33175  404 

405 
lemma openin_clauses: 

406 
fixes U :: "'a topology" 

407 
shows "openin U {}" 

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

409 
"\<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

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

411 
by fast+ 
33175  412 

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

414 
unfolding topspace_def by blast 

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

416 

417 
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

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

419 

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

420 
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

421 
using openin_clauses by simp 
33175  422 

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

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

425 

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

427 

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

36584  430 
proof 
49711  431 
assume ?lhs 
432 
then show ?rhs by auto 

36584  433 
next 
434 
assume H: ?rhs 

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

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

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

438 
finally show "openin U S" . 

33175  439 
qed 
440 

49711  441 

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

442 
subsubsection {* Closed sets *} 
33175  443 

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

445 

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

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

448 
lemma closedin_topspace[intro,simp]: 

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

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

451 
by (auto simp add: Diff_Un closedin_def) 

452 

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

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

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

456 

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

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

459 

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

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

462 
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) 

463 
apply (metis openin_subset subset_eq) 

464 
done 

465 

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

467 
by (simp add: openin_closedin_eq) 

468 

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

470 
proof 

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

472 
by (auto simp add: topspace_def openin_subset) 

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

474 
qed 

475 

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

477 
proof 

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

479 
by (auto simp add: topspace_def ) 

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

481 
qed 

482 

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

483 
subsubsection {* Subspace topology *} 
44170
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 
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

486 

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

487 
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

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

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

491 
{fix A B assume A: "?L A" and B: "?L B" 
33175  492 
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 
493 
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

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

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

497 
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

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

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

502 
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast 
33175  503 
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

504 
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

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

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

507 
unfolding subset_eq mem_Collect_eq istopology_def by blast 
33175  508 
qed 
509 

510 
lemma openin_subtopology: 

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

512 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 

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

513 
by auto 
33175  514 

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

516 
by (auto simp add: topspace_def openin_subtopology) 

517 

518 
lemma closedin_subtopology: 

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

520 
unfolding closedin_def topspace_subtopology 

521 
apply (simp add: openin_subtopology) 

522 
apply (rule iffI) 

523 
apply clarify 

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

525 
by auto 

526 

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

528 
unfolding openin_subtopology 

529 
apply (rule iffI, clarify) 

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

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

49711  532 
apply auto 
533 
done 

534 

535 
lemma subtopology_superset: 

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

33175  537 
shows "subtopology U V = U" 
538 
proof 

539 
{fix S 

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

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

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

543 
moreover 

544 
{assume S: "openin U S" 

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

546 
using openin_subset[OF S] UV by auto} 

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

548 
then show ?thesis unfolding topology_eq openin_subtopology by blast 

549 
qed 

550 

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

552 
by (simp add: subtopology_superset) 

553 

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

555 
by (simp add: subtopology_superset) 

556 

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

557 
subsubsection {* The standard Euclidean topology *} 
33175  558 

559 
definition 

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

561 
"euclidean = topology open" 

562 

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

564 
unfolding euclidean_def 

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

566 
apply (rule topology_inverse[symmetric]) 

567 
apply (auto simp add: istopology_def) 

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

568 
done 
33175  569 

570 
lemma topspace_euclidean: "topspace euclidean = UNIV" 

571 
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

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

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

576 
by (simp add: topspace_euclidean topspace_subtopology) 

577 

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

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

580 

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

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

583 

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

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

585 

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

586 
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

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

588 

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

589 
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

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

591 

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

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

593 
"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

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

595 

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

596 
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

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

598 

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

599 
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

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

601 

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

602 
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

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

604 

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

605 
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

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

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

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

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

610 

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

611 
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

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

613 

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

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

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

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

617 
\<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

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

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

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

621 
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

622 
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

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

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

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

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

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

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

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

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

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

632 
unfolding T_def 
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 
apply (drule (1) bspec, erule rev_bexI) 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

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

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

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

639 
qed 
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 
text {* These "transitivity" results are handy too *} 
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

642 

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

643 
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

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

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

646 

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

647 
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

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

649 

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

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

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

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

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

654 
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

655 

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

656 
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

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

658 

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

659 

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

660 
subsection {* Open and closed balls *} 
33175  661 

662 
definition 

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

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

665 

666 
definition 

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

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

669 

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

670 
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

671 
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

672 

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 
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

674 
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

675 

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

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

679 
by (simp add: dist_norm) 

680 

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

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

684 
by (simp add: dist_norm) 

685 

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

686 
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

687 
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

688 

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 
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

690 
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

691 

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

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

695 
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

696 
by (simp add: set_eq_iff) arith 
33175  697 

698 
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

699 
by (simp add: set_eq_iff) 
33175  700 

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

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

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

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

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

706 

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

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

708 
unfolding open_dist ball_def mem_Collect_eq Ball_def 
33175  709 
unfolding dist_commute 
710 
apply clarify 

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

712 
using dist_triangle_alt[where z=x] 

713 
apply (clarsimp simp add: diff_less_iff) 

714 
apply atomize 

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

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

717 
by arith 

718 

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

720 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. 

721 

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

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

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

724 
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

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

726 

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

729 

730 
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

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

734 

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

736 

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

737 
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

738 
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

739 
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

740 
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

741 
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

742 

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

743 
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

744 

50087  745 
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

746 
fixes x :: "'a\<Colon>euclidean_space" 
50087  747 
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

748 
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  749 
proof  
750 
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

751 
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

752 
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  753 
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

754 
fix i from Rats_dense_in_real[of "x \<bullet> i  e'" "x \<bullet> i"] e show "?th i" by auto 
50087  755 
qed 
756 
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

757 
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  758 
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

759 
fix i from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e show "?th i" by auto 
50087  760 
qed 
761 
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

762 
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

763 
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

764 
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

765 
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

766 
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<twosuperior>)" 
50087  767 
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

768 
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))" 
50087  769 
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

770 
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

771 
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

772 
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

773 
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

774 
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

775 
then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" 
50087  776 
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

777 
then have "(dist (x \<bullet> i) (y \<bullet> i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>" 
50087  778 
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

779 
then show "(dist (x \<bullet> i) (y \<bullet> i))\<twosuperior> < e\<twosuperior> / real DIM('a)" 
50087  780 
by (simp add: power_divide) 
781 
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

782 
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

783 
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

784 
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

785 
qed 
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 

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 
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

788 
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

789 
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

790 
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

791 
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

792 
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

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

796 
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

797 
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

798 
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

799 
"\<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

800 
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

801 
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

802 
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

803 
(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

804 
qed (auto simp: I_def) 
33175  805 

806 
subsection{* Connectedness *} 

807 

808 
definition "connected S \<longleftrightarrow> 

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

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

811 

812 
lemma connected_local: 

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

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

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

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

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

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

819 
~(e2 = {}))" 

820 
unfolding connected_def openin_open by (safe, blast+) 

821 

34105  822 
lemma exists_diff: 
823 
fixes P :: "'a set \<Rightarrow> bool" 

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

33175  825 
proof 
826 
{assume "?lhs" hence ?rhs by blast } 

827 
moreover 

828 
{fix S assume H: "P S" 

34105  829 
have "S =  ( S)" by auto 
830 
with H have "P ( ( S))" by metis } 

33175  831 
ultimately show ?thesis by metis 
832 
qed 

833 

834 
lemma connected_clopen: "connected S \<longleftrightarrow> 

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

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

837 
proof 

34105  838 
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  839 
unfolding connected_def openin_open closedin_closed 
840 
apply (subst exists_diff) by blast 

34105  841 
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> {})" 
842 
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis 

33175  843 

844 
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'))" 

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

846 
unfolding connected_def openin_open closedin_closed by auto 

847 
{fix e2 

848 
{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)" 

849 
by auto} 

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

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

852 
then show ?thesis unfolding th0 th1 by simp 

853 
qed 

854 

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

856 
by (simp add: connected_def) 

857 

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

858 

33175  859 
subsection{* Limit points *} 
860 

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

861 
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

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

865 
lemma islimptI: 

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

867 
shows "x islimpt S" 

868 
using assms unfolding islimpt_def by auto 

869 

870 
lemma islimptE: 

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

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

873 
using assms unfolding islimpt_def by auto 

874 

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

877 

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

879 
unfolding islimpt_def by fast 

33175  880 

881 
lemma islimpt_approachable: 

882 
fixes x :: "'a::metric_space" 

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

44584  884 
unfolding islimpt_iff_eventually eventually_at by fast 
33175  885 

886 
lemma islimpt_approachable_le: 

887 
fixes x :: "'a::metric_space" 

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

889 
unfolding islimpt_approachable 

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

892 
by (simp add: Bex_def conj_commute conj_left_commute) 

33175  893 

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

896 

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

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

898 

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

33175  901 

902 
lemma perfect_choose_dist: 

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

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

906 
by (simp add: islimpt_approachable) 

907 

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

909 
unfolding closed_def 

910 
apply (subst open_subopen) 

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

912 
by (metis ComplE ComplI) 
33175  913 

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

915 
unfolding islimpt_def by auto 

916 

917 
lemma finite_set_avoid: 

918 
fixes a :: "'a::metric_space" 

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

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

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

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

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

926 
moreover 

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

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

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

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

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

932 
ultimately show ?case by blast 

933 
qed 

934 

935 
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

936 
by (simp add: islimpt_iff_eventually eventually_conj_iff) 
33175  937 

938 
lemma discrete_imp_closed: 

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

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

941 
shows "closed S" 

942 
proof 

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

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

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

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

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

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

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

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

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

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

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

954 
qed 

955 

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

956 

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

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

958 

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

961 
lemma interiorI [intro?]: 

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

963 
shows "x \<in> interior S" 

964 
using assms unfolding interior_def by fast 

965 

966 
lemma interiorE [elim?]: 

967 
assumes "x \<in> interior S" 

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

969 
using assms unfolding interior_def by fast 

970 

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

972 
by (simp add: interior_def open_Union) 

973 

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

975 
by (auto simp add: interior_def) 

976 

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

978 
by (auto simp add: interior_def) 

979 

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

981 
by (intro equalityI interior_subset interior_maximal subset_refl) 

33175  982 

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

44519  984 
by (metis open_interior interior_open) 
985 

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

33175  987 
by (metis interior_maximal interior_subset subset_trans) 
988 

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

991 

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

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

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

994 

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

997 

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

998 
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

999 
by (auto simp add: interior_def) 
44519  1000 

1001 
lemma interior_unique: 

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

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

1004 
shows "interior S = T" 

1005 
by (intro equalityI assms interior_subset open_interior interior_maximal) 

1006 

1007 
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

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

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

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

1013 
by (simp add: open_subset_interior) 

33175  1014 

1015 
lemma interior_limit_point [intro]: 

1016 
fixes x :: "'a::perfect_space" 

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

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

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

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

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

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

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

1023 
done 
33175  1024 

1025 
lemma interior_closed_Un_empty_interior: 

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

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

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

1033 
proof 

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

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

1038 
assume "x \<notin> interior S" 

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

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

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

1044 
show "False" unfolding interior_def by fast 

1045 
qed 

1046 
qed 

1047 
qed 

1048 

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

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

1052 
by (intro Sigma_mono interior_subset) 

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

1054 
by (intro open_Times open_interior) 

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

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

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

1059 
using `open T` unfolding open_prod_def by fast 

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

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

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

1063 
by (auto intro: interiorI) 

1064 
qed 

44365  1065 
qed 
1066 

33175  1067 

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

1068 
subsection {* Closure of a Set *} 
33175  1069 

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

1071 

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

1074 

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

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

44518  1079 
unfolding closure_interior by (simp add: closed_Compl) 
1080 

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

1082 
unfolding closure_def by simp 

33175  1083 

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

44519  1085 
unfolding hull_def closure_interior interior_def by auto 
33175  1086 

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

44519  1088 
unfolding closure_hull using closed_Inter by (rule hull_eq) 
1089 

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

1091 
unfolding closure_eq . 

1092 

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

44518  1094 
unfolding closure_hull by (rule hull_hull) 
33175  1095 

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

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

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

44519  1102 
lemma closure_unique: 
1103 
assumes "S \<subseteq> T" and "closed T" 

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

1105 
shows "closure S = T" 

1106 
using assms unfolding closure_hull by (rule hull_unique) 

1107 

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

44518  1109 
using closed_empty by (rule closure_closed) 
33175  1110 

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

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

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

1115 
unfolding closure_interior by simp 

33175  1116 

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

1118 
using closure_empty closure_subset[of S] 

1119 
by blast 

1120 

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

1122 
using closure_eq[of S] closure_subset[of S] 

1123 
by simp 

1124 

1125 
lemma open_inter_closure_eq_empty: 

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

34105  1127 
using open_subset_interior[of S " T"] 
1128 
using interior_subset[of " T"] 

33175  1129 
unfolding closure_interior 
1130 
by auto 

1131 

1132 
lemma open_inter_closure_subset: 

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

1134 
proof 

1135 
fix x 

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

1137 
{ assume *:"x islimpt T" 

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

1139 
proof (rule islimptI) 

1140 
fix A 

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

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

1143 
by (simp_all add: open_Int) 

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

1145 
by (rule islimptE) 

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

1147 
by simp_all 

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

1149 
qed 

1150 
} 

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

1152 
unfolding closure_def 

1153 
by blast 

1154 
qed 

1155 

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

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

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

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

1167 
by (intro closed_Times closed_closure) 

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

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

1172 
apply (simp add: closure_interior interior_def) 

1173 
apply (drule_tac x=C in spec) 

1174 
apply (drule_tac x=D in spec) 

1175 
apply auto 
