lp15@69874: section\T1 spaces with equivalences to many naturally "nice" properties. \
lp15@69874:
lp15@69874: theory T1_Spaces
lp15@69939: imports Product_Topology
lp15@69874: begin
lp15@69874:
lp15@69874: definition t1_space where
lp15@69874: "t1_space X \ \x \ topspace X. \y \ topspace X. x\y \ (\U. openin X U \ x \ U \ y \ U)"
lp15@69874:
lp15@69874: lemma t1_space_expansive:
lp15@69874: "\topspace Y = topspace X; \U. openin X U \ openin Y U\ \ t1_space X \ t1_space Y"
lp15@69874: by (metis t1_space_def)
lp15@69874:
lp15@69874: lemma t1_space_alt:
lp15@69874: "t1_space X \ (\x \ topspace X. \y \ topspace X. x\y \ (\U. closedin X U \ x \ U \ y \ U))"
lp15@69874: by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def)
lp15@69874:
lp15@69874: lemma t1_space_empty: "topspace X = {} \ t1_space X"
lp15@69874: by (simp add: t1_space_def)
lp15@69874:
lp15@69874: lemma t1_space_derived_set_of_singleton:
lp15@69874: "t1_space X \ (\x \ topspace X. X derived_set_of {x} = {})"
lp15@69874: apply (simp add: t1_space_def derived_set_of_def, safe)
lp15@69874: apply (metis openin_topspace)
lp15@69874: by force
lp15@69874:
lp15@69874: lemma t1_space_derived_set_of_finite:
lp15@69874: "t1_space X \ (\S. finite S \ X derived_set_of S = {})"
lp15@69874: proof (intro iffI allI impI)
lp15@69874: fix S :: "'a set"
lp15@69874: assume "finite S"
lp15@69874: then have fin: "finite ((\x. {x}) ` (topspace X \ S))"
lp15@69874: by blast
lp15@69874: assume "t1_space X"
lp15@69874: then have "X derived_set_of (\x \ topspace X \ S. {x}) = {}"
lp15@69874: unfolding derived_set_of_Union [OF fin]
lp15@69874: by (auto simp: t1_space_derived_set_of_singleton)
lp15@69874: then have "X derived_set_of (topspace X \ S) = {}"
lp15@69874: by simp
lp15@69874: then show "X derived_set_of S = {}"
lp15@69874: by simp
lp15@69874: qed (auto simp: t1_space_derived_set_of_singleton)
lp15@69874:
lp15@69874: lemma t1_space_closedin_singleton:
lp15@69874: "t1_space X \ (\x \ topspace X. closedin X {x})"
lp15@69874: apply (rule iffI)
lp15@69874: apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton)
lp15@69874: using t1_space_alt by auto
lp15@69874:
lp15@69874: lemma closedin_t1_singleton:
lp15@69874: "\t1_space X; a \ topspace X\ \ closedin X {a}"
lp15@69874: by (simp add: t1_space_closedin_singleton)
lp15@69874:
lp15@69874: lemma t1_space_closedin_finite:
lp15@69874: "t1_space X \ (\S. finite S \ S \ topspace X \ closedin X S)"
lp15@69874: apply (rule iffI)
lp15@69874: apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_finite)
lp15@69874: by (simp add: t1_space_closedin_singleton)
lp15@69874:
lp15@69874: lemma closure_of_singleton:
lp15@69874: "t1_space X \ X closure_of {a} = (if a \ topspace X then {a} else {})"
lp15@69874: by (simp add: closure_of_eq t1_space_closedin_singleton closure_of_eq_empty_gen)
lp15@69874:
lp15@69874: lemma separated_in_singleton:
lp15@69874: assumes "t1_space X"
lp15@69874: shows "separatedin X {a} S \ a \ topspace X \ S \ topspace X \ (a \ X closure_of S)"
lp15@69874: "separatedin X S {a} \ a \ topspace X \ S \ topspace X \ (a \ X closure_of S)"
lp15@69874: unfolding separatedin_def
lp15@69874: using assms closure_of closure_of_singleton by fastforce+
lp15@69874:
lp15@69874: lemma t1_space_openin_delete:
lp15@69874: "t1_space X \ (\U x. openin X U \ x \ U \ openin X (U - {x}))"
lp15@69874: apply (rule iffI)
lp15@69874: apply (meson closedin_t1_singleton in_mono openin_diff openin_subset)
lp15@69874: by (simp add: closedin_def t1_space_closedin_singleton)
lp15@69874:
lp15@69874: lemma t1_space_openin_delete_alt:
lp15@69874: "t1_space X \ (\U x. openin X U \ openin X (U - {x}))"
lp15@69874: by (metis Diff_empty Diff_insert0 t1_space_openin_delete)
lp15@69874:
lp15@69874:
lp15@69874: lemma t1_space_singleton_Inter_open:
lp15@69874: "t1_space X \ (\x \ topspace X. \{U. openin X U \ x \ U} = {x})" (is "?P=?Q")
lp15@69874: and t1_space_Inter_open_supersets:
lp15@69874: "t1_space X \ (\S. S \ topspace X \ \{U. openin X U \ S \ U} = S)" (is "?P=?R")
lp15@69874: proof -
lp15@69874: have "?R \ ?Q"
lp15@69874: apply clarify
lp15@69874: apply (drule_tac x="{x}" in spec, simp)
lp15@69874: done
lp15@69874: moreover have "?Q \ ?P"
lp15@69874: apply (clarsimp simp add: t1_space_def)
lp15@69874: apply (drule_tac x=x in bspec)
lp15@69874: apply (simp_all add: set_eq_iff)
lp15@69874: by (metis (no_types, lifting))
lp15@69874: moreover have "?P \ ?R"
lp15@69874: proof (clarsimp simp add: t1_space_closedin_singleton, rule subset_antisym)
lp15@69874: fix S
lp15@69874: assume S: "\x\topspace X. closedin X {x}" "S \ topspace X"
lp15@69874: then show "\ {U. openin X U \ S \ U} \ S"
lp15@69874: apply clarsimp
lp15@69874: by (metis Diff_insert_absorb Set.set_insert closedin_def openin_topspace subset_insert)
lp15@69874: qed force
lp15@69874: ultimately show "?P=?Q" "?P=?R"
lp15@69874: by auto
lp15@69874: qed
lp15@69874:
lp15@69874: lemma t1_space_derived_set_of_infinite_openin:
lp15@69874: "t1_space X \
lp15@69874: (\S. X derived_set_of S =
lp15@69874: {x \ topspace X. \U. x \ U \ openin X U \ infinite(S \ U)})"
lp15@69874: (is "_ = ?rhs")
lp15@69874: proof
lp15@69874: assume "t1_space X"
lp15@69874: show ?rhs
lp15@69874: proof safe
lp15@69874: fix S x U
lp15@69874: assume "x \ X derived_set_of S" "x \ U" "openin X U" "finite (S \ U)"
lp15@69874: with \t1_space X\ show "False"
lp15@69874: apply (simp add: t1_space_derived_set_of_finite)
lp15@69874: by (metis IntI empty_iff empty_subsetI inf_commute openin_Int_derived_set_of_subset subset_antisym)
lp15@69874: next
lp15@69874: fix S x
lp15@69874: have eq: "(\y. (y \ x) \ y \ S \ y \ T) \ ~((S \ T) \ {x})" for x S T
lp15@69874: by blast
lp15@69874: assume "x \ topspace X" "\U. x \ U \ openin X U \ infinite (S \ U)"
lp15@69874: then show "x \ X derived_set_of S"
lp15@69874: apply (clarsimp simp add: derived_set_of_def eq)
lp15@69874: by (meson finite.emptyI finite.insertI finite_subset)
lp15@69874: qed (auto simp: in_derived_set_of)
lp15@69874: qed (auto simp: t1_space_derived_set_of_singleton)
lp15@69874:
lp15@69874: lemma finite_t1_space_imp_discrete_topology:
lp15@69874: "\topspace X = U; finite U; t1_space X\ \ X = discrete_topology U"
lp15@69874: by (metis discrete_topology_unique_derived_set t1_space_derived_set_of_finite)
lp15@69874:
lp15@69874: lemma t1_space_subtopology: "t1_space X \ t1_space(subtopology X U)"
lp15@69874: by (simp add: derived_set_of_subtopology t1_space_derived_set_of_finite)
lp15@69874:
lp15@69874: lemma closedin_derived_set_of_gen:
lp15@69874: "t1_space X \ closedin X (X derived_set_of S)"
lp15@69874: apply (clarsimp simp add: in_derived_set_of closedin_contains_derived_set derived_set_of_subset_topspace)
lp15@69874: by (metis DiffD2 insert_Diff insert_iff t1_space_openin_delete)
lp15@69874:
lp15@69874: lemma derived_set_of_derived_set_subset_gen:
lp15@69874: "t1_space X \ X derived_set_of (X derived_set_of S) \ X derived_set_of S"
lp15@69874: by (meson closedin_contains_derived_set closedin_derived_set_of_gen)
lp15@69874:
lp15@69874: lemma subtopology_eq_discrete_topology_gen_finite:
lp15@69874: "\t1_space X; finite S\ \ subtopology X S = discrete_topology(topspace X \ S)"
lp15@69874: by (simp add: subtopology_eq_discrete_topology_gen t1_space_derived_set_of_finite)
lp15@69874:
lp15@69874: lemma subtopology_eq_discrete_topology_finite:
lp15@69874: "\t1_space X; S \ topspace X; finite S\
lp15@69874: \ subtopology X S = discrete_topology S"
lp15@69874: by (simp add: subtopology_eq_discrete_topology_eq t1_space_derived_set_of_finite)
lp15@69874:
lp15@69874: lemma t1_space_closed_map_image:
lp15@69874: "\closed_map X Y f; f ` (topspace X) = topspace Y; t1_space X\ \ t1_space Y"
lp15@69874: by (metis closed_map_def finite_subset_image t1_space_closedin_finite)
lp15@69874:
lp15@69874: lemma homeomorphic_t1_space: "X homeomorphic_space Y \ (t1_space X \ t1_space Y)"
lp15@69874: apply (clarsimp simp add: homeomorphic_space_def)
lp15@69874: by (meson homeomorphic_eq_everything_map homeomorphic_maps_map t1_space_closed_map_image)
lp15@69874:
lp15@69874: proposition t1_space_product_topology:
lp15@69874: "t1_space (product_topology X I)
lp15@69874: \ topspace(product_topology X I) = {} \ (\i \ I. t1_space (X i))"
lp15@69874: proof (cases "topspace(product_topology X I) = {}")
lp15@69874: case True
lp15@69874: then show ?thesis
lp15@69874: using True t1_space_empty by blast
lp15@69874: next
lp15@69874: case False
lp15@69874: then obtain f where f: "f \ (\\<^sub>E i\I. topspace(X i))"
lp15@69874: by fastforce
lp15@69874: have "t1_space (product_topology X I) \ (\i\I. t1_space (X i))"
lp15@69874: proof (intro iffI ballI)
lp15@69874: show "t1_space (X i)" if "t1_space (product_topology X I)" and "i \ I" for i
lp15@69874: proof -
lp15@69874: have clo: "\h. h \ (\\<^sub>E i\I. topspace (X i)) \ closedin (product_topology X I) {h}"
lp15@69874: using that by (simp add: t1_space_closedin_singleton)
lp15@69874: show ?thesis
lp15@69874: unfolding t1_space_closedin_singleton
lp15@69874: proof clarify
lp15@69874: show "closedin (X i) {xi}" if "xi \ topspace (X i)" for xi
lp15@69874: using clo [of "\j \ I. if i=j then xi else f j"] f that \i \ I\
lp15@69874: by (fastforce simp add: closedin_product_topology_singleton)
lp15@69874: qed
lp15@69874: qed
lp15@69874: next
lp15@69874: next
lp15@69874: show "t1_space (product_topology X I)" if "\i\I. t1_space (X i)"
lp15@69874: using that
lp15@69874: by (simp add: t1_space_closedin_singleton Ball_def PiE_iff closedin_product_topology_singleton)
lp15@69874: qed
lp15@69874: then show ?thesis
lp15@69874: using False by blast
lp15@69874: qed
lp15@69874:
lp15@69939: lemma t1_space_prod_topology:
lp15@69939: "t1_space(prod_topology X Y) \ topspace(prod_topology X Y) = {} \ t1_space X \ t1_space Y"
lp15@69939: proof (cases "topspace (prod_topology X Y) = {}")
lp15@69939: case True then show ?thesis
lp15@69939: by (auto simp: t1_space_empty)
lp15@69939: next
lp15@69939: case False
lp15@69939: have eq: "{(x,y)} = {x} \ {y}" for x y
lp15@69939: by simp
lp15@69939: have "t1_space (prod_topology X Y) \ (t1_space X \ t1_space Y)"
lp15@69939: using False
lp15@69939: by (force simp: t1_space_closedin_singleton closedin_Times eq simp del: insert_Times_insert)
lp15@69939: with False show ?thesis
lp15@69939: by simp
lp15@69939: qed
lp15@69939:
lp15@69874: end