author  paulson <lp15@cam.ac.uk> 
Mon, 09 Oct 2017 16:14:18 +0100  
changeset 66794  83bf64da6938 
parent 66793  deabce3ccf1f 
child 66827  c94531b5007d 
permissions  rwrr 
63938  1 
(* Author: L C Paulson, University of Cambridge 
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 

60420  7 
section \<open>Elementary topology in Euclidean space.\<close> 
33175  8 

9 
theory Topology_Euclidean_Space 

50087  10 
imports 
66453
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
66447
diff
changeset

11 
"HOLLibrary.Indicator_Function" 
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
66447
diff
changeset

12 
"HOLLibrary.Countable_Set" 
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
66447
diff
changeset

13 
"HOLLibrary.FuncSet" 
50938  14 
Linear_Algebra 
50087  15 
Norm_Arith 
16 
begin 

17 

63593
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

18 
(* FIXME: move elsewhere *) 
63928
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63881
diff
changeset

19 

64122  20 
lemma Times_eq_image_sum: 
21 
fixes S :: "'a :: comm_monoid_add set" and T :: "'b :: comm_monoid_add set" 

22 
shows "S \<times> T = {u + v u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T}" 

23 
by force 

24 

63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63957
diff
changeset

25 
lemma halfspace_Int_eq: 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63957
diff
changeset

26 
"{x. a \<bullet> x \<le> b} \<inter> {x. b \<le> a \<bullet> x} = {x. a \<bullet> x = b}" 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63957
diff
changeset

27 
"{x. b \<le> a \<bullet> x} \<inter> {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}" 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63957
diff
changeset

28 
by auto 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63957
diff
changeset

29 

63593
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

30 
definition (in monoid_add) support_on :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'b set" 
64539  31 
where "support_on s f = {x\<in>s. f x \<noteq> 0}" 
63593
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

32 

bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

33 
lemma in_support_on: "x \<in> support_on s f \<longleftrightarrow> x \<in> s \<and> f x \<noteq> 0" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

34 
by (simp add: support_on_def) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

35 

bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

36 
lemma support_on_simps[simp]: 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

37 
"support_on {} f = {}" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

38 
"support_on (insert x s) f = 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

39 
(if f x = 0 then support_on s f else insert x (support_on s f))" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

40 
"support_on (s \<union> t) f = support_on s f \<union> support_on t f" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

41 
"support_on (s \<inter> t) f = support_on s f \<inter> support_on t f" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

42 
"support_on (s  t) f = support_on s f  support_on t f" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

43 
"support_on (f ` s) g = f ` (support_on s (g \<circ> f))" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

44 
unfolding support_on_def by auto 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

45 

bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

46 
lemma support_on_cong: 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

47 
"(\<And>x. x \<in> s \<Longrightarrow> f x = 0 \<longleftrightarrow> g x = 0) \<Longrightarrow> support_on s f = support_on s g" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

48 
by (auto simp: support_on_def) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

49 

bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

50 
lemma support_on_if: "a \<noteq> 0 \<Longrightarrow> support_on A (\<lambda>x. if P x then a else 0) = {x\<in>A. P x}" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

51 
by (auto simp: support_on_def) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

52 

bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

53 
lemma support_on_if_subset: "support_on A (\<lambda>x. if P x then a else 0) \<subseteq> {x \<in> A. P x}" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

54 
by (auto simp: support_on_def) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

55 

bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

56 
lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support_on s f)" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

57 
unfolding support_on_def by auto 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

58 

64267  59 
(* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *) 
60 
definition (in comm_monoid_add) supp_sum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a" 

64539  61 
where "supp_sum f s = (\<Sum>x\<in>support_on s f. f x)" 
64267  62 

63 
lemma supp_sum_empty[simp]: "supp_sum f {} = 0" 

64 
unfolding supp_sum_def by auto 

65 

66 
lemma supp_sum_insert[simp]: 

63593
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

67 
"finite (support_on s f) \<Longrightarrow> 
64267  68 
supp_sum f (insert x s) = (if x \<in> s then supp_sum f s else f x + supp_sum f s)" 
69 
by (simp add: supp_sum_def in_support_on insert_absorb) 

70 

71 
lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\<lambda>n. f n / r) A" 

63593
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

72 
by (cases "r = 0") 
64267  73 
(auto simp: supp_sum_def sum_divide_distrib intro!: sum.cong support_on_cong) 
63305
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

74 

3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

75 
(*END OF SUPPORT, ETC.*) 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

76 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

77 
lemma image_affinity_interval: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

78 
fixes c :: "'a::ordered_real_vector" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

79 
shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {} 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

80 
else if 0 <= m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

81 
else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

82 
apply (case_tac "m=0", force) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

83 
apply (auto simp: scaleR_left_mono) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

84 
apply (rule_tac x="inverse m *\<^sub>R (xc)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

85 
apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

86 
apply (rule_tac x="inverse m *\<^sub>R (xc)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

87 
using le_diff_eq scaleR_le_cancel_left_neg 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

88 
apply fastforce 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

89 
done 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

90 

53282  91 
lemma countable_PiE: 
64910  92 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)" 
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

93 
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

94 

64845  95 
lemma open_sums: 
96 
fixes T :: "('b::real_normed_vector) set" 

97 
assumes "open S \<or> open T" 

98 
shows "open (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})" 

99 
using assms 

100 
proof 

101 
assume S: "open S" 

102 
show ?thesis 

103 
proof (clarsimp simp: open_dist) 

104 
fix x y 

105 
assume "x \<in> S" "y \<in> T" 

106 
with S obtain e where "e > 0" and e: "\<And>x'. dist x' x < e \<Longrightarrow> x' \<in> S" 

107 
by (auto simp: open_dist) 

108 
then have "\<And>z. dist z (x + y) < e \<Longrightarrow> \<exists>x\<in>S. \<exists>y\<in>T. z = x + y" 

109 
by (metis \<open>y \<in> T\<close> diff_add_cancel dist_add_cancel2) 

110 
then show "\<exists>e>0. \<forall>z. dist z (x + y) < e \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>T. z = x + y)" 

111 
using \<open>0 < e\<close> \<open>x \<in> S\<close> by blast 

112 
qed 

113 
next 

114 
assume T: "open T" 

115 
show ?thesis 

116 
proof (clarsimp simp: open_dist) 

117 
fix x y 

118 
assume "x \<in> S" "y \<in> T" 

119 
with T obtain e where "e > 0" and e: "\<And>x'. dist x' y < e \<Longrightarrow> x' \<in> T" 

120 
by (auto simp: open_dist) 

121 
then have "\<And>z. dist z (x + y) < e \<Longrightarrow> \<exists>x\<in>S. \<exists>y\<in>T. z = x + y" 

122 
by (metis \<open>x \<in> S\<close> add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm) 

123 
then show "\<exists>e>0. \<forall>z. dist z (x + y) < e \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>T. z = x + y)" 

124 
using \<open>0 < e\<close> \<open>y \<in> T\<close> by blast 

125 
qed 

126 
qed 

127 

53255  128 

60420  129 
subsection \<open>Topological Basis\<close> 
50087  130 

131 
context topological_space 

132 
begin 

133 

53291  134 
definition "topological_basis B \<longleftrightarrow> 
135 
(\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" 

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

136 

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

137 
lemma topological_basis: 
53291  138 
"topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" 
50998  139 
unfolding topological_basis_def 
140 
apply safe 

141 
apply fastforce 

142 
apply fastforce 

66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

143 
apply (erule_tac x=x in allE, simp) 
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

144 
apply (rule_tac x="{x}" in exI, auto) 
50998  145 
done 
146 

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

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

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

151 
proof safe 

152 
fix O' and x::'a 

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

53282  154 
then have "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def) 
50087  155 
then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto 
53282  156 
then show "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto 
50087  157 
next 
158 
assume H: ?rhs 

53282  159 
show "topological_basis B" 
160 
using assms unfolding topological_basis_def 

50087  161 
proof safe 
53640  162 
fix O' :: "'a set" 
53282  163 
assume "open O'" 
50087  164 
with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'" 
165 
by (force intro: bchoice simp: Bex_def) 

53282  166 
then show "\<exists>B'\<subseteq>B. \<Union>B' = O'" 
50087  167 
by (auto intro: exI[where x="{f x x. x \<in> O'}"]) 
168 
qed 

169 
qed 

170 

171 
lemma topological_basisI: 

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

53282  173 
and "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" 
50087  174 
shows "topological_basis B" 
175 
using assms by (subst topological_basis_iff) auto 

176 

177 
lemma topological_basisE: 

178 
fixes O' 

179 
assumes "topological_basis B" 

53282  180 
and "open O'" 
181 
and "x \<in> O'" 

50087  182 
obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'" 
183 
proof atomize_elim 

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

50087  186 
with topological_basis_iff assms 
53282  187 
show "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" 
188 
using assms by (simp add: Bex_def) 

50087  189 
qed 
190 

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

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

192 
assumes "topological_basis B" 
53282  193 
and "X \<in> B" 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

194 
shows "open X" 
53282  195 
using assms by (simp add: topological_basis_def) 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

196 

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

197 
lemma topological_basis_imp_subbasis: 
53255  198 
assumes B: "topological_basis B" 
199 
shows "open = generate_topology B" 

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

200 
proof (intro ext iffI) 
53255  201 
fix S :: "'a set" 
202 
assume "open S" 

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

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

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

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

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

207 
next 
53255  208 
fix S :: "'a set" 
209 
assume "generate_topology B S" 

210 
then show "open S" 

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

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

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

213 

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

214 
lemma basis_dense: 
53640  215 
fixes B :: "'a set set" 
216 
and f :: "'a set \<Rightarrow> 'a" 

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

217 
assumes "topological_basis B" 
53255  218 
and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'" 
55522  219 
shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

220 
proof (intro allI impI) 
53640  221 
fix X :: "'a set" 
222 
assume "open X" and "X \<noteq> {}" 

60420  223 
from topological_basisE[OF \<open>topological_basis B\<close> \<open>open X\<close> choosefrom_basis[OF \<open>X \<noteq> {}\<close>]] 
55522  224 
obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" . 
53255  225 
then show "\<exists>B'\<in>B. f B' \<in> X" 
226 
by (auto intro!: choosefrom_basis) 

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

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

228 

50087  229 
end 
230 

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

231 
lemma topological_basis_prod: 
53255  232 
assumes A: "topological_basis A" 
233 
and B: "topological_basis B" 

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

234 
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

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

236 
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric]) 
53255  237 
fix S :: "('a \<times> 'b) set" 
238 
assume "open S" 

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

239 
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

240 
proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"]) 
53255  241 
fix x y 
242 
assume "(x, y) \<in> S" 

60420  243 
from open_prod_elim[OF \<open>open S\<close> this] 
50882
a382bf90867e
move prod instantiation of second_countable_topology to its definition
hoelzl
parents:
50881
diff
changeset

244 
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

245 
by (metis mem_Sigma_iff) 
55522  246 
moreover 
247 
from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a" 

248 
by (rule topological_basisE) 

249 
moreover 

250 
from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b" 

251 
by (rule topological_basisE) 

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

252 
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

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

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

255 
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

256 

53255  257 

60420  258 
subsection \<open>Countable Basis\<close> 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

259 

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

260 
locale countable_basis = 
53640  261 
fixes B :: "'a::topological_space set set" 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

262 
assumes is_basis: "topological_basis B" 
53282  263 
and countable_basis: "countable B" 
33175  264 
begin 
265 

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

266 
lemma open_countable_basis_ex: 
50087  267 
assumes "open X" 
61952  268 
shows "\<exists>B' \<subseteq> B. X = \<Union>B'" 
53255  269 
using assms countable_basis is_basis 
270 
unfolding topological_basis_def by blast 

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

271 

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

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

273 
assumes "open X" 
61952  274 
obtains B' where "B' \<subseteq> B" "X = \<Union>B'" 
53255  275 
using assms open_countable_basis_ex 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

276 
by atomize_elim simp 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50105
diff
changeset

277 

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

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

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

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

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

284 
by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI) 
50087  285 
qed 
286 

287 
lemma countable_dense_setE: 

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

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

289 
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

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

291 

50087  292 
end 
293 

50883  294 
lemma (in first_countable_topology) first_countable_basisE: 
295 
obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" 

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

297 
using first_countable_basis[of x] 

51473  298 
apply atomize_elim 
299 
apply (elim exE) 

66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

300 
apply (rule_tac x="range A" in exI, auto) 
51473  301 
done 
50883  302 

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

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

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

307 
proof atomize_elim 

55522  308 
obtain A' where A': 
309 
"countable A'" 

310 
"\<And>a. a \<in> A' \<Longrightarrow> x \<in> a" 

311 
"\<And>a. a \<in> A' \<Longrightarrow> open a" 

312 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S" 

313 
by (rule first_countable_basisE) blast 

63040  314 
define A where [abs_def]: 
315 
"A = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)" 

53255  316 
then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and> 
51105  317 
(\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" 
318 
proof (safe intro!: exI[where x=A]) 

53255  319 
show "countable A" 
320 
unfolding A_def by (intro countable_image countable_Collect_finite) 

321 
fix a 

322 
assume "a \<in> A" 

323 
then show "x \<in> a" "open a" 

324 
using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) 

51105  325 
next 
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51773
diff
changeset

326 
let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)" 
53255  327 
fix a b 
328 
assume "a \<in> A" "b \<in> A" 

329 
then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" 

330 
by (auto simp: A_def) 

331 
then show "a \<inter> b \<in> A" 

332 
by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) 

51105  333 
next 
53255  334 
fix S 
335 
assume "open S" "x \<in> S" 

336 
then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast 

337 
then show "\<exists>a\<in>A. a \<subseteq> S" using a A' 

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

340 
qed 

341 

51473  342 
lemma (in topological_space) first_countableI: 
53255  343 
assumes "countable A" 
344 
and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" 

345 
and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" 

51473  346 
shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 
347 
proof (safe intro!: exI[of _ "from_nat_into A"]) 

53255  348 
fix i 
51473  349 
have "A \<noteq> {}" using 2[of UNIV] by auto 
53255  350 
show "x \<in> from_nat_into A i" "open (from_nat_into A i)" 
60420  351 
using range_from_nat_into_subset[OF \<open>A \<noteq> {}\<close>] 1 by auto 
53255  352 
next 
353 
fix S 

354 
assume "open S" "x\<in>S" from 2[OF this] 

355 
show "\<exists>i. from_nat_into A i \<subseteq> S" 

60420  356 
using subset_range_from_nat_into[OF \<open>countable A\<close>] by auto 
51473  357 
qed 
51350  358 

50883  359 
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology 
360 
proof 

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

55522  362 
obtain A where A: 
363 
"countable A" 

364 
"\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a" 

365 
"\<And>a. a \<in> A \<Longrightarrow> open a" 

366 
"\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" 

367 
by (rule first_countable_basisE[of "fst x"]) blast 

368 
obtain B where B: 

369 
"countable B" 

370 
"\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a" 

371 
"\<And>a. a \<in> B \<Longrightarrow> open a" 

372 
"\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S" 

373 
by (rule first_countable_basisE[of "snd x"]) blast 

53282  374 
show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set. 
375 
(\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 

51473  376 
proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe) 
53255  377 
fix a b 
378 
assume x: "a \<in> A" "b \<in> B" 

53640  379 
with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" and "open (a \<times> b)" 
380 
unfolding mem_Times_iff 

381 
by (auto intro: open_Times) 

50883  382 
next 
53255  383 
fix S 
384 
assume "open S" "x \<in> S" 

55522  385 
then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S" 
386 
by (rule open_prod_elim) 

387 
moreover 

388 
from a'b' A(4)[of a'] B(4)[of b'] 

389 
obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" 

390 
by auto 

391 
ultimately 

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

50883  393 
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) 
394 
qed (simp add: A B) 

395 
qed 

396 

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

397 
class second_countable_topology = topological_space + 
53282  398 
assumes ex_countable_subbasis: 
399 
"\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B" 

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

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

401 

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

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

403 
proof  
53255  404 
from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" 
405 
by blast 

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

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

407 

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

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

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

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

411 
by (intro countable_image countable_Collect_finite_subset B) 
53255  412 
{ 
413 
fix S 

414 
assume "open S" 

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

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

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

417 
proof induct 
53255  418 
case UNIV 
419 
show ?case by (intro exI[of _ "{{}}"]) simp 

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

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

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

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

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

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

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

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

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

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

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

430 
then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto 
55522  431 
then obtain k where 
432 
"\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka" 

433 
unfolding bchoice_iff .. 

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

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

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

436 
next 
53255  437 
case (Basis S) 
438 
then show ?case 

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

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

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

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

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

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

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

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

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

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

449 

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

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

451 

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

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

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

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

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

456 

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

457 
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

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

459 
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

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

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

462 
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

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

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

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

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

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

468 

50883  469 
instance second_countable_topology \<subseteq> first_countable_topology 
470 
proof 

471 
fix x :: 'a 

63040  472 
define B :: "'a set set" where "B = (SOME B. countable B \<and> topological_basis B)" 
50883  473 
then have B: "countable B" "topological_basis B" 
474 
using countable_basis is_basis 

475 
by (auto simp: countable_basis is_basis) 

53282  476 
then show "\<exists>A::nat \<Rightarrow> 'a set. 
477 
(\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 

51473  478 
by (intro first_countableI[of "{b\<in>B. x \<in> b}"]) 
479 
(fastforce simp: topological_space_class.topological_basis_def)+ 

50883  480 
qed 
481 

64320
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
64287
diff
changeset

482 
instance nat :: second_countable_topology 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
64287
diff
changeset

483 
proof 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
64287
diff
changeset

484 
show "\<exists>B::nat set set. countable B \<and> open = generate_topology B" 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
64287
diff
changeset

485 
by (intro exI[of _ "range lessThan \<union> range greaterThan"]) (auto simp: open_nat_def) 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
64287
diff
changeset

486 
qed 
53255  487 

64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

488 
lemma countable_separating_set_linorder1: 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

489 
shows "\<exists>B::('a::{linorder_topology, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x < b \<and> b \<le> y))" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

490 
proof  
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

491 
obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

492 
define B1 where "B1 = {(LEAST x. x \<in> U) U. U \<in> A}" 
64911  493 
then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image) 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

494 
define B2 where "B2 = {(SOME x. x \<in> U) U. U \<in> A}" 
64911  495 
then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image) 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

496 
have "\<exists>b \<in> B1 \<union> B2. x < b \<and> b \<le> y" if "x < y" for x y 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

497 
proof (cases) 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

498 
assume "\<exists>z. x < z \<and> z < y" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

499 
then obtain z where z: "x < z \<and> z < y" by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

500 
define U where "U = {x<..<y}" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

501 
then have "open U" by simp 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

502 
moreover have "z \<in> U" using z U_def by simp 
64911  503 
ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

504 
define w where "w = (SOME x. x \<in> V)" 
64911  505 
then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2) 
506 
then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce 

507 
moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto 

64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

508 
ultimately show ?thesis by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

509 
next 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

510 
assume "\<not>(\<exists>z. x < z \<and> z < y)" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

511 
then have *: "\<And>z. z > x \<Longrightarrow> z \<ge> y" by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

512 
define U where "U = {x<..}" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

513 
then have "open U" by simp 
64911  514 
moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp 
515 
ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto 

516 
have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto 

517 
then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp 

518 
then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE) 

519 
then have "y \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto 

520 
moreover have "x < y \<and> y \<le> y" using \<open>x < y\<close> by simp 

64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

521 
ultimately show ?thesis by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

522 
qed 
64911  523 
moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

524 
ultimately show ?thesis by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

525 
qed 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

526 

f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

527 
lemma countable_separating_set_linorder2: 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

528 
shows "\<exists>B::('a::{linorder_topology, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x \<le> b \<and> b < y))" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

529 
proof  
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

530 
obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

531 
define B1 where "B1 = {(GREATEST x. x \<in> U)  U. U \<in> A}" 
64911  532 
then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image) 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

533 
define B2 where "B2 = {(SOME x. x \<in> U) U. U \<in> A}" 
64911  534 
then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image) 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

535 
have "\<exists>b \<in> B1 \<union> B2. x \<le> b \<and> b < y" if "x < y" for x y 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

536 
proof (cases) 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

537 
assume "\<exists>z. x < z \<and> z < y" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

538 
then obtain z where z: "x < z \<and> z < y" by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

539 
define U where "U = {x<..<y}" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

540 
then have "open U" by simp 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

541 
moreover have "z \<in> U" using z U_def by simp 
64911  542 
ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

543 
define w where "w = (SOME x. x \<in> V)" 
64911  544 
then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2) 
545 
then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce 

546 
moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto 

64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

547 
ultimately show ?thesis by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

548 
next 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

549 
assume "\<not>(\<exists>z. x < z \<and> z < y)" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

550 
then have *: "\<And>z. z < y \<Longrightarrow> z \<le> x" using leI by blast 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

551 
define U where "U = {..<y}" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

552 
then have "open U" by simp 
64911  553 
moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp 
554 
ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto 

555 
have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto 

556 
then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp 

557 
then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE) 

558 
then have "x \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto 

559 
moreover have "x \<le> x \<and> x < y" using \<open>x < y\<close> by simp 

64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

560 
ultimately show ?thesis by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

561 
qed 
64911  562 
moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

563 
ultimately show ?thesis by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

564 
qed 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

565 

f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

566 
lemma countable_separating_set_dense_linorder: 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

567 
shows "\<exists>B::('a::{linorder_topology, dense_linorder, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x < b \<and> b < y))" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

568 
proof  
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

569 
obtain B::"'a set" where B: "countable B" "\<And>x y. x < y \<Longrightarrow> (\<exists>b \<in> B. x < b \<and> b \<le> y)" 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

570 
using countable_separating_set_linorder1 by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

571 
have "\<exists>b \<in> B. x < b \<and> b < y" if "x < y" for x y 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

572 
proof  
64911  573 
obtain z where "x < z" "z < y" using \<open>x < y\<close> dense by blast 
64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

574 
then obtain b where "b \<in> B" "x < b \<and> b \<le> z" using B(2) by auto 
64911  575 
then have "x < b \<and> b < y" using \<open>z < y\<close> by auto 
576 
then show ?thesis using \<open>b \<in> B\<close> by auto 

64284
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

577 
qed 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

578 
then show ?thesis using B(1) by auto 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

579 
qed 
f3b905b2eee2
HOLAnalysis: more theorems from SÃ©bastien GouÃ«zel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

580 

60420  581 
subsection \<open>Polish spaces\<close> 
582 

583 
text \<open>Textbooks define Polish spaces as completely metrizable. 

584 
We assume the topology to be complete for a given metric.\<close> 

50087  585 

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

586 
class polish_space = complete_space + second_countable_topology 
50087  587 

60420  588 
subsection \<open>General notion of a topology as a value\<close> 
33175  589 

53255  590 
definition "istopology L \<longleftrightarrow> 
60585  591 
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))" 
53255  592 

49834  593 
typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" 
33175  594 
morphisms "openin" "topology" 
595 
unfolding istopology_def by blast 

596 

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

597 
lemma istopology_openin[intro]: "istopology(openin U)" 
33175  598 
using openin[of U] by blast 
599 

600 
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

601 
using topology_inverse[unfolded mem_Collect_eq] . 
33175  602 

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

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

604 
using topology_inverse[of U] istopology_openin[of "topology U"] by auto 
33175  605 

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

53255  607 
proof 
608 
assume "T1 = T2" 

609 
then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp 

610 
next 

611 
assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" 

612 
then have "openin T1 = openin T2" by (simp add: fun_eq_iff) 

613 
then have "topology (openin T1) = topology (openin T2)" by simp 

614 
then show "T1 = T2" unfolding openin_inverse . 

33175  615 
qed 
616 

60420  617 
text\<open>Infer the "universe" from union of all sets in the topology.\<close> 
33175  618 

53640  619 
definition "topspace T = \<Union>{S. openin T S}" 
33175  620 

60420  621 
subsubsection \<open>Main properties of open sets\<close> 
33175  622 

623 
lemma openin_clauses: 

624 
fixes U :: "'a topology" 

53282  625 
shows 
626 
"openin U {}" 

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

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

629 
using openin[of U] unfolding istopology_def mem_Collect_eq by fast+ 

33175  630 

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

632 
unfolding topspace_def by blast 

53255  633 

634 
lemma openin_empty[simp]: "openin U {}" 

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

635 
by (rule openin_clauses) 
33175  636 

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

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

638 
by (rule openin_clauses) 
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

639 

313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

640 
lemma openin_Union[intro]: "(\<And>S. S \<in> K \<Longrightarrow> openin U S) \<Longrightarrow> openin U (\<Union>K)" 
63075
60a42a4166af
lemmas about dimension, hyperplanes, span, etc.
paulson <lp15@cam.ac.uk>
parents:
63040
diff
changeset

641 
using openin_clauses by blast 
33175  642 

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

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

645 

53255  646 
lemma openin_topspace[intro, simp]: "openin U (topspace U)" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

647 
by (force simp: openin_Union topspace_def) 
33175  648 

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

36584  651 
proof 
49711  652 
assume ?lhs 
653 
then show ?rhs by auto 

36584  654 
next 
655 
assume H: ?rhs 

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

66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

657 
have "openin U ?t" by (force simp: openin_Union) 
36584  658 
also have "?t = S" using H by auto 
659 
finally show "openin U S" . 

33175  660 
qed 
661 

64845  662 
lemma openin_INT [intro]: 
663 
assumes "finite I" 

664 
"\<And>i. i \<in> I \<Longrightarrow> openin T (U i)" 

665 
shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)" 

66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

666 
using assms by (induct, auto simp: inf_sup_aci(2) openin_Int) 
64845  667 

668 
lemma openin_INT2 [intro]: 

669 
assumes "finite I" "I \<noteq> {}" 

670 
"\<And>i. i \<in> I \<Longrightarrow> openin T (U i)" 

671 
shows "openin T (\<Inter>i \<in> I. U i)" 

672 
proof  

673 
have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T" 

64911  674 
using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto 
64845  675 
then show ?thesis 
676 
using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute) 

677 
qed 

678 

66793
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66643
diff
changeset

679 
lemma openin_Inter [intro]: 
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66643
diff
changeset

680 
assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)" 
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66643
diff
changeset

681 
by (metis (full_types) assms openin_INT2 image_ident) 
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66643
diff
changeset

682 

49711  683 

60420  684 
subsubsection \<open>Closed sets\<close> 
33175  685 

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

687 

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

690 

691 
lemma closedin_empty[simp]: "closedin U {}" 

692 
by (simp add: closedin_def) 

693 

694 
lemma closedin_topspace[intro, simp]: "closedin U (topspace U)" 

695 
by (simp add: closedin_def) 

696 

33175  697 
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

698 
by (auto simp: Diff_Un closedin_def) 
33175  699 

60585  700 
lemma Diff_Inter[intro]: "A  \<Inter>S = \<Union>{A  ss. s\<in>S}" 
53255  701 
by auto 
702 

63955  703 
lemma closedin_Union: 
704 
assumes "finite S" "\<And>T. T \<in> S \<Longrightarrow> closedin U T" 

705 
shows "closedin U (\<Union>S)" 

706 
using assms by induction auto 

707 

53255  708 
lemma closedin_Inter[intro]: 
709 
assumes Ke: "K \<noteq> {}" 

62131
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

710 
and Kc: "\<And>S. S \<in>K \<Longrightarrow> closedin U S" 
60585  711 
shows "closedin U (\<Inter>K)" 
53255  712 
using Ke Kc unfolding closedin_def Diff_Inter by auto 
33175  713 

62131
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

714 
lemma closedin_INT[intro]: 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

715 
assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)" 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

716 
shows "closedin U (\<Inter>x\<in>A. B x)" 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

717 
apply (rule closedin_Inter) 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

718 
using assms 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

719 
apply auto 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

720 
done 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62127
diff
changeset

721 

33175  722 
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" 
723 
using closedin_Inter[of "{S,T}" U] by auto 

724 

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

66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

726 
apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2) 
33175  727 
apply (metis openin_subset subset_eq) 
728 
done 

729 

53255  730 
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U  S))" 
33175  731 
by (simp add: openin_closedin_eq) 
732 

53255  733 
lemma openin_diff[intro]: 
734 
assumes oS: "openin U S" 

735 
and cT: "closedin U T" 

736 
shows "openin U (S  T)" 

737 
proof  

33175  738 
have "S  T = S \<inter> (topspace U  T)" using openin_subset[of U S] oS cT 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

739 
by (auto simp: topspace_def openin_subset) 
53282  740 
then show ?thesis using oS cT 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

741 
by (auto simp: closedin_def) 
33175  742 
qed 
743 

53255  744 
lemma closedin_diff[intro]: 
745 
assumes oS: "closedin U S" 

746 
and cT: "openin U T" 

747 
shows "closedin U (S  T)" 

748 
proof  

749 
have "S  T = S \<inter> (topspace U  T)" 

66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

750 
using closedin_subset[of U S] oS cT by (auto simp: topspace_def) 
53255  751 
then show ?thesis 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

752 
using oS cT by (auto simp: openin_closedin_eq) 
53255  753 
qed 
754 

33175  755 

60420  756 
subsubsection \<open>Subspace topology\<close> 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

757 

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

758 
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

759 

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

760 
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

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

763 
have "?L {}" by blast 
53255  764 
{ 
765 
fix A B 

766 
assume A: "?L A" and B: "?L B" 

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

768 
by blast 

769 
have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" 

770 
using Sa Sb by blast+ 

771 
then have "?L (A \<inter> B)" by blast 

772 
} 

33175  773 
moreover 
53255  774 
{ 
53282  775 
fix K 
776 
assume K: "K \<subseteq> Collect ?L" 

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

777 
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)" 
55775  778 
by blast 
33175  779 
from K[unfolded th0 subset_image_iff] 
53255  780 
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" 
781 
by blast 

782 
have "\<Union>K = (\<Union>Sk) \<inter> V" 

783 
using Sk by auto 

60585  784 
moreover have "openin U (\<Union>Sk)" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

785 
using Sk by (auto simp: subset_eq) 
53255  786 
ultimately have "?L (\<Union>K)" by blast 
787 
} 

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

788 
ultimately show ?thesis 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62131
diff
changeset

789 
unfolding subset_eq mem_Collect_eq istopology_def by auto 
33175  790 
qed 
791 

53255  792 
lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)" 
33175  793 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

794 
by auto 
33175  795 

53255  796 
lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

797 
by (auto simp: topspace_def openin_subtopology) 
33175  798 

53255  799 
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" 
33175  800 
unfolding closedin_def topspace_subtopology 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

801 
by (auto simp: openin_subtopology) 
33175  802 

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

804 
unfolding openin_subtopology 

55775  805 
by auto (metis IntD1 in_mono openin_subset) 
49711  806 

807 
lemma subtopology_superset: 

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

33175  809 
shows "subtopology U V = U" 
53255  810 
proof  
811 
{ 

812 
fix S 

813 
{ 

814 
fix T 

815 
assume T: "openin U T" "S = T \<inter> V" 

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

817 
by blast 

818 
have "openin U S" 

819 
unfolding eq using T by blast 

820 
} 

33175  821 
moreover 
53255  822 
{ 
823 
assume S: "openin U S" 

824 
then have "\<exists>T. openin U T \<and> S = T \<inter> V" 

825 
using openin_subset[OF S] UV by auto 

826 
} 

827 
ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" 

828 
by blast 

829 
} 

830 
then show ?thesis 

831 
unfolding topology_eq openin_subtopology by blast 

33175  832 
qed 
833 

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

835 
by (simp add: subtopology_superset) 

836 

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

838 
by (simp add: subtopology_superset) 

839 

62948
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

840 
lemma openin_subtopology_empty: 
64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64539
diff
changeset

841 
"openin (subtopology U {}) S \<longleftrightarrow> S = {}" 
62948
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

842 
by (metis Int_empty_right openin_empty openin_subtopology) 
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

843 

7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

844 
lemma closedin_subtopology_empty: 
64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64539
diff
changeset

845 
"closedin (subtopology U {}) S \<longleftrightarrow> S = {}" 
62948
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

846 
by (metis Int_empty_right closedin_empty closedin_subtopology) 
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

847 

64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64539
diff
changeset

848 
lemma closedin_subtopology_refl [simp]: 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64539
diff
changeset

849 
"closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U" 
62948
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

850 
by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology) 
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

851 

7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

852 
lemma openin_imp_subset: 
64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64539
diff
changeset

853 
"openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S" 
62948
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

854 
by (metis Int_iff openin_subtopology subsetI) 
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

855 

7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

856 
lemma closedin_imp_subset: 
64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64539
diff
changeset

857 
"closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S" 
62948
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

858 
by (simp add: closedin_def topspace_subtopology) 
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

859 

7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

860 
lemma openin_subtopology_Un: 
64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64539
diff
changeset

861 
"openin (subtopology U T) S \<and> openin (subtopology U u) S 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64539
diff
changeset

862 
\<Longrightarrow> openin (subtopology U (T \<union> u)) S" 
62948
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

863 
by (simp add: openin_subtopology) blast 
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

864 

53255  865 

60420  866 
subsubsection \<open>The standard Euclidean topology\<close> 
33175  867 

53255  868 
definition euclidean :: "'a::topological_space topology" 
869 
where "euclidean = topology open" 

33175  870 

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

872 
unfolding euclidean_def 

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

874 
apply (rule topology_inverse[symmetric]) 

66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

875 
apply (auto simp: istopology_def) 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

876 
done 
33175  877 

64122  878 
declare open_openin [symmetric, simp] 
879 

63492
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
63469
diff
changeset

880 
lemma topspace_euclidean [simp]: "topspace euclidean = UNIV" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

881 
by (force simp: topspace_def) 
33175  882 

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

64122  884 
by (simp add: topspace_subtopology) 
33175  885 

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

64122  887 
by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV) 
33175  888 

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

64122  890 
using openI by auto 
33175  891 

62948
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

892 
lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S" 
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

893 
by (metis openin_topspace topspace_euclidean_subtopology) 
7700f467892b
lots of new theorems for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
62843
diff
changeset

894 

60420  895 
text \<open>Basic "localization" results are handy for connectedness.\<close> 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

896 

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

897 
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

898 
by (auto simp: openin_subtopology) 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

899 

63305
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

900 
lemma openin_Int_open: 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

901 
"\<lbrakk>openin (subtopology euclidean U) S; open T\<rbrakk> 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

902 
\<Longrightarrow> openin (subtopology euclidean U) (S \<inter> T)" 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

903 
by (metis open_Int Int_assoc openin_open) 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

904 

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

905 
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

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

907 

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

908 
lemma open_openin_trans[trans]: 
53255  909 
"open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T" 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

911 

53255  912 
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

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

914 

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

915 
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

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

917 

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

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

920 

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

921 
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

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

923 

64791
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64788
diff
changeset

924 
lemma closedin_closed_subset: 
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64788
diff
changeset

925 
"\<lbrakk>closedin (subtopology euclidean U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk> 
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64788
diff
changeset

926 
\<Longrightarrow> closedin (subtopology euclidean T) S" 
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64788
diff
changeset

927 
by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE) 
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64788
diff
changeset

928 

63928
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63881
diff
changeset

929 
lemma finite_imp_closedin: 
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63881
diff
changeset

930 
fixes S :: "'a::t1_space set" 
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63881
diff
changeset

931 
shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology euclidean T) S" 
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63881
diff
changeset

932 
by (simp add: finite_imp_closed closed_subset) 
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63881
diff
changeset

933 

63305
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

934 
lemma closedin_singleton [simp]: 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

935 
fixes a :: "'a::t1_space" 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

936 
shows "closedin (subtopology euclidean U) {a} \<longleftrightarrow> a \<in> U" 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

937 
using closedin_subset by (force intro: closed_subset) 
3b6975875633
Urysohn's lemma, Dugundji extension theorem and many other proofs
paulson <lp15@cam.ac.uk>
parents:
63301
diff
changeset

938 

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

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

940 
fixes S U :: "'a::metric_space set" 
53255  941 
shows "openin (subtopology euclidean U) S \<longleftrightarrow> 
942 
S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" 

943 
(is "?lhs \<longleftrightarrow> ?rhs") 

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

944 
proof 
53255  945 
assume ?lhs 
53282  946 
then show ?rhs 
947 
unfolding openin_open open_dist by blast 

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

948 
next 
63040  949 
define T where "T = {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}" 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

950 
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

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

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

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

954 
apply (clarsimp simp add: less_diff_eq) 
55775  955 
by (metis dist_commute dist_triangle_lt) 
53282  956 
assume ?rhs then have 2: "S = U \<inter> T" 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60040
diff
changeset

957 
unfolding T_def 
55775  958 
by auto (metis dist_self) 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

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

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

961 
qed 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

962 

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

963 
lemma connected_openin: 
61306
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

964 
"connected s \<longleftrightarrow> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

965 
~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

966 
openin (subtopology euclidean s) e2 \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

967 
s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

968 
apply (simp add: connected_def openin_open, safe) 
63988  969 
apply (simp_all, blast+) (* SLOW *) 
61306
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

970 
done 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

971 

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

972 
lemma connected_openin_eq: 
61306
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

973 
"connected s \<longleftrightarrow> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

974 
~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

975 
openin (subtopology euclidean s) e2 \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

976 
e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

977 
e1 \<noteq> {} \<and> e2 \<noteq> {})" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

978 
apply (simp add: connected_openin, safe, blast) 
61306
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

979 
by (metis Int_lower1 Un_subset_iff openin_open subset_antisym) 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

980 

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

981 
lemma connected_closedin: 
61306
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

982 
"connected s \<longleftrightarrow> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

983 
~(\<exists>e1 e2. 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

984 
closedin (subtopology euclidean s) e1 \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

985 
closedin (subtopology euclidean s) e2 \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

986 
s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

987 
e1 \<noteq> {} \<and> e2 \<noteq> {})" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

988 
proof  
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

989 
{ fix A B x x' 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

990 
assume s_sub: "s \<subseteq> A \<union> B" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

991 
and disj: "A \<inter> B \<inter> s = {}" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

992 
and x: "x \<in> s" "x \<in> B" and x': "x' \<in> s" "x' \<in> A" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

993 
and cl: "closed A" "closed B" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

994 
assume "\<forall>e1. (\<forall>T. closed T \<longrightarrow> e1 \<noteq> s \<inter> T) \<or> (\<forall>e2. e1 \<inter> e2 = {} \<longrightarrow> s \<subseteq> e1 \<union> e2 \<longrightarrow> (\<forall>T. closed T \<longrightarrow> e2 \<noteq> s \<inter> T) \<or> e1 = {} \<or> e2 = {})" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

995 
then have "\<And>C D. s \<inter> C = {} \<or> s \<inter> D = {} \<or> s \<inter> (C \<inter> (s \<inter> D)) \<noteq> {} \<or> \<not> s \<subseteq> s \<inter> (C \<union> D) \<or> \<not> closed C \<or> \<not> closed D" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

996 
by (metis (no_types) Int_Un_distrib Int_assoc) 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

997 
moreover have "s \<inter> (A \<inter> B) = {}" "s \<inter> (A \<union> B) = s" "s \<inter> B \<noteq> {}" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

998 
using disj s_sub x by blast+ 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

999 
ultimately have "s \<inter> A = {}" 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1000 
using cl by (metis inf.left_commute inf_bot_right order_refl) 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1001 
then have False 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1002 
using x' by blast 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1003 
} note * = this 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1004 
show ?thesis 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1005 
apply (simp add: connected_closed closedin_closed) 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1006 
apply (safe; simp) 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1007 
apply blast 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1008 
apply (blast intro: *) 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1009 
done 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1010 
qed 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1011 

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

1012 
lemma connected_closedin_eq: 
61306
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1013 
"connected s \<longleftrightarrow> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1014 
~(\<exists>e1 e2. 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1015 
closedin (subtopology euclidean s) e1 \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1016 
closedin (subtopology euclidean s) e2 \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1017 
e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and> 
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1018 
e1 \<noteq> {} \<and> e2 \<noteq> {})" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

1019 
apply (simp add: connected_closedin, safe, blast) 
61306
9dd394c866fc
New theorems about connected sets. And pairwise moved to Set.thy.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1020 
by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

1021 

60420  1022 
text \<open>These "transitivity" results are handy too\<close> 
44210
eba74571833b
Topology_Euclidean_Space.thy: organize section headings
huffman
parents:
44207
diff
changeset

1023 

53255  1024 
lemma openin_trans[trans]: 
1025 
"openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow> 

1026 
openin (subtopology euclidean U) S" 

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

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

1028 

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

1029 
lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

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

1031 

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

1032 
lemma closedin_trans[trans]: 
53255  1033 
"closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow> 
1034 
closedin (subtopology euclidean U) S" 

66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

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

1036 

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

1037 
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S" 
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset

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

1039 

62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

1040 
lemma openin_subtopology_Int_subset: 
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset

1041 
"\<lbrakk>openin (subtopology euclidean u) (u \<inter> S); v \<subseteq> u\<rbrakk> \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> S)" 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1042 
by (auto simp: openin_subtopology) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1043 

ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1044 
lemma openin_open_eq: "open s \<Longrightarrow> (openin (subtopology euclidean s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1045 
using open_subset openin_open_trans openin_subset by fastforce 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1046 

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

1047 

60420  1048 
subsection \<open>Open and closed balls\<close> 
33175  1049 

53255  1050 
definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" 
1051 
where "ball x e = {y. dist x y < e}" 

1052 

1053 
definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" 

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

33175  1055 

61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

1056 
definition sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

1057 
where "sphere x e = {y. dist x y = e}" 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

1058 

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

1059 
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

1060 
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

1061 

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

1062 
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

1063 
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

1064 

61848  1065 
lemma mem_sphere [simp]: "y \<in> sphere x e \<longleftrightarrow> dist x y = e" 
1066 
by (simp add: sphere_def) 

1067 

61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1068 
lemma ball_trivial [simp]: "ball x 0 = {}" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1069 
by (simp add: ball_def) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1070 

ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1071 
lemma cball_trivial [simp]: "cball x 0 = {x}" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1072 
by (simp add: cball_def) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1073 

63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63332
diff
changeset

1074 
lemma sphere_trivial [simp]: "sphere x 0 = {x}" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63332
diff
changeset

1075 
by (simp add: sphere_def) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63332
diff
changeset

1076 

64539  1077 
lemma mem_ball_0 [simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" 
1078 
for x :: "'a::real_normed_vector" 

33175  1079 
by (simp add: dist_norm) 
1080 

64539  1081 
lemma mem_cball_0 [simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" 
1082 
for x :: "'a::real_normed_vector" 

33175  1083 
by (simp add: dist_norm) 
1084 

64539  1085 
lemma disjoint_ballI: "dist x y \<ge> r+s \<Longrightarrow> ball x r \<inter> ball y s = {}" 
64287  1086 
using dist_triangle_less_add not_le by fastforce 
1087 

64539  1088 
lemma disjoint_cballI: "dist x y > r + s \<Longrightarrow> cball x r \<inter> cball y s = {}" 
64287  1089 
by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball) 
1090 

64539  1091 
lemma mem_sphere_0 [simp]: "x \<in> sphere 0 e \<longleftrightarrow> norm x = e" 
1092 
for x :: "'a::real_normed_vector" 

63114
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset

1093 
by (simp add: dist_norm) 
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset

1094 

64539  1095 
lemma sphere_empty [simp]: "r < 0 \<Longrightarrow> sphere a r = {}" 
1096 
for a :: "'a::metric_space" 

1097 
by auto 

63881
b746b19197bd
lots of new results about topology, affine dimension etc
paulson <lp15@cam.ac.uk>
parents:
63627
diff
changeset

1098 

61518 