Theory HOL-Analysis.Abstract_Topology_2
section ‹Abstract Topology 2›
theory Abstract_Topology_2
imports
Elementary_Topology Abstract_Topology Continuum_Not_Denumerable
"HOL-Library.Indicator_Function"
"HOL-Library.Equipollence"
begin
text ‹Combination of Elementary and Abstract Topology›
lemma approachable_lt_le2:
"(∃(d::real) > 0. ∀x. Q x ⟶ f x < d ⟶ P x) ⟷ (∃d>0. ∀x. f x ≤ d ⟶ Q x ⟶ P x)"
by (meson dense less_eq_real_def order_le_less_trans)
lemma triangle_lemma:
fixes x y z :: real
assumes x: "0 ≤ x"
and y: "0 ≤ y"
and z: "0 ≤ z"
and xy: "x⇧2 ≤ y⇧2 + z⇧2"
shows "x ≤ y + z"
proof -
have "y⇧2 + z⇧2 ≤ y⇧2 + 2 * y * z + z⇧2"
using z y by simp
with xy have th: "x⇧2 ≤ (y + z)⇧2"
by (simp add: power2_eq_square field_simps)
from y z have yz: "y + z ≥ 0"
by arith
from power2_le_imp_le[OF th yz] show ?thesis .
qed
lemma isCont_indicator:
fixes x :: "'a::t2_space"
shows "isCont (indicator A :: 'a ⇒ real) x = (x ∉ frontier A)"
proof auto
fix x
assume cts_at: "isCont (indicator A :: 'a ⇒ real) x" and fr: "x ∈ frontier A"
with continuous_at_open have 1: "∀V::real set. open V ∧ indicator A x ∈ V ⟶
(∃U::'a set. open U ∧ x ∈ U ∧ (∀y∈U. indicator A y ∈ V))" by auto
show False
proof (cases "x ∈ A")
assume x: "x ∈ A"
hence "indicator A x ∈ ({0<..<2} :: real set)" by simp
with 1 obtain U where U: "open U" "x ∈ U" "∀y∈U. indicator A y ∈ ({0<..<2} :: real set)"
using open_greaterThanLessThan by metis
hence "∀y∈U. indicator A y > (0::real)"
unfolding greaterThanLessThan_def by auto
hence "U ⊆ A" using indicator_eq_0_iff by force
hence "x ∈ interior A" using U interiorI by auto
thus ?thesis using fr unfolding frontier_def by simp
next
assume x: "x ∉ A"
hence "indicator A x ∈ ({-1<..<1} :: real set)" by simp
with 1 obtain U where U: "open U" "x ∈ U" "∀y∈U. indicator A y ∈ ({-1<..<1} :: real set)"
using 1 open_greaterThanLessThan by metis
hence "∀y∈U. indicator A y < (1::real)"
unfolding greaterThanLessThan_def by auto
hence "U ⊆ -A" by auto
hence "x ∈ interior (-A)" using U interiorI by auto
thus ?thesis using fr interior_complement unfolding frontier_def by auto
qed
next
assume nfr: "x ∉ frontier A"
hence "x ∈ interior A ∨ x ∈ interior (-A)"
by (auto simp: frontier_def closure_interior)
thus "isCont ((indicator A)::'a ⇒ real) x"
proof
assume int: "x ∈ interior A"
then obtain U where U: "open U" "x ∈ U" "U ⊆ A" unfolding interior_def by auto
hence "∀y∈U. indicator A y = (1::real)" unfolding indicator_def by auto
hence "continuous_on U (indicator A)" by (simp add: indicator_eq_1_iff)
thus ?thesis using U continuous_on_eq_continuous_at by auto
next
assume ext: "x ∈ interior (-A)"
then obtain U where U: "open U" "x ∈ U" "U ⊆ -A" unfolding interior_def by auto
then have "continuous_on U (indicator A)"
using continuous_on_topological by (auto simp: subset_iff)
thus ?thesis using U continuous_on_eq_continuous_at by auto
qed
qed
lemma islimpt_closure:
"⟦S ⊆ T; ⋀x. ⟦x islimpt S; x ∈ T⟧ ⟹ x ∈ S⟧ ⟹ S = T ∩ closure S"
using closure_def by fastforce
lemma closedin_limpt:
"closedin (top_of_set T) S ⟷ S ⊆ T ∧ (∀x. x islimpt S ∧ x ∈ T ⟶ x ∈ S)"
proof -
have "⋀U x. ⟦closed U; S = T ∩ U; x islimpt S; x ∈ T⟧ ⟹ x ∈ S"
by (meson IntI closed_limpt inf_le2 islimpt_subset)
then show ?thesis
by (metis closed_closure closedin_closed closedin_imp_subset islimpt_closure)
qed
lemma closedin_closed_eq: "closed S ⟹ closedin (top_of_set S) T ⟷ closed T ∧ T ⊆ S"
by (meson closedin_limpt closed_subset closedin_closed_trans)
lemma connected_closed_set:
"closed S
⟹ connected S ⟷ (∄A B. closed A ∧ closed B ∧ A ≠ {} ∧ B ≠ {} ∧ A ∪ B = S ∧ A ∩ B = {})"
unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
text ‹If a connnected set is written as the union of two nonempty closed sets,
then these sets have to intersect.›
lemma connected_as_closed_union:
assumes "connected C" "C = A ∪ B" "closed A" "closed B" "A ≠ {}" "B ≠ {}"
shows "A ∩ B ≠ {}"
by (metis assms closed_Un connected_closed_set)
lemma closedin_subset_trans:
"closedin (top_of_set U) S ⟹ S ⊆ T ⟹ T ⊆ U ⟹
closedin (top_of_set T) S"
by (meson closedin_limpt subset_iff)
lemma openin_subset_trans:
"openin (top_of_set U) S ⟹ S ⊆ T ⟹ T ⊆ U ⟹
openin (top_of_set T) S"
by (auto simp: openin_open)
lemma closedin_compact:
"⟦compact S; closedin (top_of_set S) T⟧ ⟹ compact T"
by (metis closedin_closed compact_Int_closed)
lemma closedin_compact_eq:
fixes S :: "'a::t2_space set"
shows "compact S ⟹ (closedin (top_of_set S) T ⟷ compact T ∧ T ⊆ S)"
by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
subsection ‹Closure›
lemma euclidean_closure_of [simp]: "euclidean closure_of S = closure S"
by (auto simp: closure_of_def closure_def islimpt_def)
lemma closure_openin_Int_closure:
assumes ope: "openin (top_of_set U) S" and "T ⊆ U"
shows "closure(S ∩ closure T) = closure(S ∩ T)"
proof
obtain V where "open V" and S: "S = U ∩ V"
using ope using openin_open by metis
show "closure (S ∩ closure T) ⊆ closure (S ∩ T)"
proof (clarsimp simp: S)
fix x
assume "x ∈ closure (U ∩ V ∩ closure T)"
then have "V ∩ closure T ⊆ A ⟹ x ∈ closure A" for A
by (metis closure_mono subsetD inf.coboundedI2 inf_assoc)
then have "x ∈ closure (T ∩ V)"
by (metis ‹open V› closure_closure inf_commute open_Int_closure_subset)
then show "x ∈ closure (U ∩ V ∩ T)"
by (metis ‹T ⊆ U› inf.absorb_iff2 inf_assoc inf_commute)
qed
next
show "closure (S ∩ T) ⊆ closure (S ∩ closure T)"
by (meson Int_mono closure_mono closure_subset order_refl)
qed
corollary infinite_openin:
fixes S :: "'a :: t1_space set"
shows "⟦openin (top_of_set U) S; x ∈ S; x islimpt U⟧ ⟹ infinite S"
by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute)
lemma closure_Int_ballI:
assumes "⋀U. ⟦openin (top_of_set S) U; U ≠ {}⟧ ⟹ T ∩ U ≠ {}"
shows "S ⊆ closure T"
proof (clarsimp simp: closure_iff_nhds_not_empty)
fix x and A and V
assume "x ∈ S" "V ⊆ A" "open V" "x ∈ V" "T ∩ A = {}"
then have "openin (top_of_set S) (A ∩ V ∩ S)"
by (simp add: inf_absorb2 openin_subtopology_Int)
moreover have "A ∩ V ∩ S ≠ {}" using ‹x ∈ V› ‹V ⊆ A› ‹x ∈ S›
by auto
ultimately show False
using ‹T ∩ A = {}› assms by fastforce
qed
subsection ‹Frontier›
lemma euclidean_interior_of [simp]: "euclidean interior_of S = interior S"
by (auto simp: interior_of_def interior_def)
lemma euclidean_frontier_of [simp]: "euclidean frontier_of S = frontier S"
by (auto simp: frontier_of_def frontier_def)
lemma connected_Int_frontier:
"⟦connected S; S ∩ T ≠ {}; S - T ≠ {}⟧ ⟹ S ∩ frontier T ≠ {}"
apply (simp add: frontier_interiors connected_openin, safe)
apply (drule_tac x="S ∩ interior T" in spec, safe)
apply (drule_tac [2] x="S ∩ interior (-T)" in spec)
apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
done
subsection ‹Compactness›
lemma openin_delete:
fixes a :: "'a :: t1_space"
shows "openin (top_of_set u) S ⟹ openin (top_of_set u) (S - {a})"
by (metis Int_Diff open_delete openin_open)
lemma compact_eq_openin_cover:
"compact S ⟷
(∀C. (∀c∈C. openin (top_of_set S) c) ∧ S ⊆ ⋃C ⟶
(∃D⊆C. finite D ∧ S ⊆ ⋃D))"
proof safe
fix C
assume "compact S" and "∀c∈C. openin (top_of_set S) c" and "S ⊆ ⋃C"
then have "∀c∈{T. open T ∧ S ∩ T ∈ C}. open c" and "S ⊆ ⋃{T. open T ∧ S ∩ T ∈ C}"
unfolding openin_open by force+
with ‹compact S› obtain D where "D ⊆ {T. open T ∧ S ∩ T ∈ C}" and "finite D" and "S ⊆ ⋃D"
by (meson compactE)
then have "image (λT. S ∩ T) D ⊆ C ∧ finite (image (λT. S ∩ T) D) ∧ S ⊆ ⋃(image (λT. S ∩ T) D)"
by auto
then show "∃D⊆C. finite D ∧ S ⊆ ⋃D" ..
next
assume 1: "∀C. (∀c∈C. openin (top_of_set S) c) ∧ S ⊆ ⋃C ⟶
(∃D⊆C. finite D ∧ S ⊆ ⋃D)"
show "compact S"
proof (rule compactI)
fix C
let ?C = "image (λT. S ∩ T) C"
assume "∀t∈C. open t" and "S ⊆ ⋃C"
then have "(∀c∈?C. openin (top_of_set S) c) ∧ S ⊆ ⋃?C"
unfolding openin_open by auto
with 1 obtain D where "D ⊆ ?C" and "finite D" and "S ⊆ ⋃D"
by metis
let ?D = "inv_into C (λT. S ∩ T) ` D"
have "?D ⊆ C ∧ finite ?D ∧ S ⊆ ⋃?D"
proof (intro conjI)
from ‹D ⊆ ?C› show "?D ⊆ C"
by (fast intro: inv_into_into)
from ‹finite D› show "finite ?D"
by (rule finite_imageI)
from ‹S ⊆ ⋃D› show "S ⊆ ⋃?D"
by (metis ‹D ⊆ (∩) S ` C› image_inv_into_cancel inf_Sup le_infE)
qed
then show "∃D⊆C. finite D ∧ S ⊆ ⋃D" ..
qed
qed
subsection ‹Continuity›
lemma interior_image_subset:
assumes "inj f" "⋀x. continuous (at x) f"
shows "interior (f ` S) ⊆ f ` (interior S)"
proof
fix x assume "x ∈ interior (f ` S)"
then obtain T where as: "open T" "x ∈ T" "T ⊆ f ` S" ..
then have "x ∈ f ` S" by auto
then obtain y where y: "y ∈ S" "x = f y" by auto
have "open (f -` T)"
using assms ‹open T› by (simp add: continuous_at_imp_continuous_on open_vimage)
moreover have "y ∈ vimage f T"
using ‹x = f y› ‹x ∈ T› by simp
moreover have "vimage f T ⊆ S"
using ‹T ⊆ image f S› ‹inj f› unfolding inj_on_def subset_eq by auto
ultimately have "y ∈ interior S" ..
with ‹x = f y› show "x ∈ f ` interior S" ..
qed
subsection ‹Equality of continuous functions on closure and related results›
lemma continuous_closedin_preimage_constant:
fixes f :: "_ ⇒ 'b::t1_space"
shows "continuous_on S f ⟹ closedin (top_of_set S) {x ∈ S. f x = a}"
using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
lemma continuous_closed_preimage_constant:
fixes f :: "_ ⇒ 'b::t1_space"
shows "continuous_on S f ⟹ closed S ⟹ closed {x ∈ S. f x = a}"
using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
lemma continuous_constant_on_closure:
fixes f :: "_ ⇒ 'b::t1_space"
assumes "continuous_on (closure S) f"
and "⋀x. x ∈ S ⟹ f x = a"
and "x ∈ closure S"
shows "f x = a"
using continuous_closed_preimage_constant[of "closure S" f a]
assms closure_minimal[of S "{x ∈ closure S. f x = a}"] closure_subset
unfolding subset_eq
by auto
lemma image_closure_subset:
assumes contf: "continuous_on (closure S) f"
and "closed T"
and "(f ` S) ⊆ T"
shows "f ` (closure S) ⊆ T"
proof -
have "S ⊆ {x ∈ closure S. f x ∈ T}"
using assms(3) closure_subset by auto
moreover have "closed (closure S ∩ f -` T)"
using continuous_closed_preimage[OF contf] ‹closed T› by auto
ultimately have "closure S = (closure S ∩ f -` T)"
using closure_minimal[of S "(closure S ∩ f -` T)"] by auto
then show ?thesis by auto
qed
lemma continuous_image_closure_subset:
assumes "continuous_on A f" "closure B ⊆ A"
shows "f ` closure B ⊆ closure (f ` B)"
using assms by (meson closed_closure closure_subset continuous_on_subset image_closure_subset)
subsection ‹A function constant on a set›
definition constant_on (infixl "(constant'_on)" 50)
where "f constant_on A ≡ ∃y. ∀x∈A. f x = y"
lemma constant_on_subset: "⟦f constant_on A; B ⊆ A⟧ ⟹ f constant_on B"
unfolding constant_on_def by blast
lemma injective_not_constant:
fixes S :: "'a::{perfect_space} set"
shows "⟦open S; inj_on f S; f constant_on S⟧ ⟹ S = {}"
unfolding constant_on_def
by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
lemma constant_on_compose:
assumes "f constant_on A"
shows "g ∘ f constant_on A"
using assms by (auto simp: constant_on_def)
lemma not_constant_onI:
"f x ≠ f y ⟹ x ∈ A ⟹ y ∈ A ⟹ ¬f constant_on A"
unfolding constant_on_def by metis
lemma constant_onE:
assumes "f constant_on S" and "⋀x. x∈S ⟹ f x = g x"
shows "g constant_on S"
using assms unfolding constant_on_def by simp
lemma constant_on_closureI:
fixes f :: "_ ⇒ 'b::t1_space"
assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
shows "f constant_on (closure S)"
using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
by metis
subsection ‹Continuity relative to a union.›
lemma continuous_on_Un_local:
"⟦closedin (top_of_set (S ∪ T)) S; closedin (top_of_set (S ∪ T)) T;
continuous_on S f; continuous_on T f⟧
⟹ continuous_on (S ∪ T) f"
unfolding continuous_on closedin_limpt
by (metis Lim_trivial_limit Lim_within_Un Un_iff trivial_limit_within)
lemma continuous_on_cases_local:
"⟦closedin (top_of_set (S ∪ T)) S; closedin (top_of_set (S ∪ T)) T;
continuous_on S f; continuous_on T g;
⋀x. ⟦x ∈ S ∧ ¬P x ∨ x ∈ T ∧ P x⟧ ⟹ f x = g x⟧
⟹ continuous_on (S ∪ T) (λx. if P x then f x else g x)"
by (rule continuous_on_Un_local) (auto intro: continuous_on_eq)
lemma continuous_on_cases_le:
fixes h :: "'a :: topological_space ⇒ real"
assumes "continuous_on {x ∈ S. h x ≤ a} f"
and "continuous_on {x ∈ S. a ≤ h x} g"
and h: "continuous_on S h"
and "⋀x. ⟦x ∈ S; h x = a⟧ ⟹ f x = g x"
shows "continuous_on S (λx. if h x ≤ a then f(x) else g(x))"
proof -
have S: "S = (S ∩ h -` atMost a) ∪ (S ∩ h -` atLeast a)"
by force
have 1: "closedin (top_of_set S) (S ∩ h -` atMost a)"
by (rule continuous_closedin_preimage [OF h closed_atMost])
have 2: "closedin (top_of_set S) (S ∩ h -` atLeast a)"
by (rule continuous_closedin_preimage [OF h closed_atLeast])
have [simp]: "S ∩ h -` {..a} = {x ∈ S. h x ≤ a}" "S ∩ h -` {a..} = {x ∈ S. a ≤ h x}"
by auto
have "continuous_on (S ∩ h -` {..a} ∪ S ∩ h -` {a..}) (λx. if h x ≤ a then f x else g x)"
by (intro continuous_on_cases_local) (use 1 2 S assms in auto)
then show ?thesis
using S by force
qed
lemma continuous_on_cases_1:
fixes S :: "real set"
assumes "continuous_on {t ∈ S. t ≤ a} f"
and "continuous_on {t ∈ S. a ≤ t} g"
and "a ∈ S ⟹ f a = g a"
shows "continuous_on S (λt. if t ≤ a then f(t) else g(t))"
using assms
by (auto intro: continuous_on_cases_le [where h = id, simplified])
subsection‹Inverse function property for open/closed maps›
lemma continuous_on_inverse_open_map:
assumes contf: "continuous_on S f"
and imf: "f ` S = T"
and injf: "⋀x. x ∈ S ⟹ g (f x) = x"
and oo: "⋀U. openin (top_of_set S) U ⟹ openin (top_of_set T) (f ` U)"
shows "continuous_on T g"
proof -
from imf injf have gTS: "g ` T = S"
by force
from imf injf have fU: "U ⊆ S ⟹ (f ` U) = T ∩ g -` U" for U
by force
show ?thesis
by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo)
qed
lemma continuous_on_inverse_closed_map:
assumes contf: "continuous_on S f"
and imf: "f ` S = T"
and injf: "⋀x. x ∈ S ⟹ g(f x) = x"
and oo: "⋀U. closedin (top_of_set S) U ⟹ closedin (top_of_set T) (f ` U)"
shows "continuous_on T g"
proof -
from imf injf have gTS: "g ` T = S"
by force
from imf injf have fU: "U ⊆ S ⟹ (f ` U) = T ∩ g -` U" for U
by force
show ?thesis
by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo)
qed
lemma homeomorphism_injective_open_map:
assumes contf: "continuous_on S f"
and imf: "f ` S = T"
and injf: "inj_on f S"
and oo: "⋀U. openin (top_of_set S) U ⟹ openin (top_of_set T) (f ` U)"
obtains g where "homeomorphism S T f g"
proof
have "continuous_on T (inv_into S f)"
by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo)
with imf injf contf show "homeomorphism S T f (inv_into S f)"
by (auto simp: homeomorphism_def)
qed
lemma homeomorphism_injective_closed_map:
assumes contf: "continuous_on S f"
and imf: "f ` S = T"
and injf: "inj_on f S"
and oo: "⋀U. closedin (top_of_set S) U ⟹ closedin (top_of_set T) (f ` U)"
obtains g where "homeomorphism S T f g"
proof
have "continuous_on T (inv_into S f)"
by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo)
with imf injf contf show "homeomorphism S T f (inv_into S f)"
by (auto simp: homeomorphism_def)
qed
lemma homeomorphism_imp_open_map:
assumes hom: "homeomorphism S T f g"
and oo: "openin (top_of_set S) U"
shows "openin (top_of_set T) (f ` U)"
proof -
from hom oo have [simp]: "f ` U = T ∩ g -` U"
using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
from hom have "continuous_on T g"
unfolding homeomorphism_def by blast
moreover have "g ` T = S"
by (metis hom homeomorphism_def)
ultimately show ?thesis
by (simp add: continuous_on_open oo)
qed
lemma homeomorphism_imp_closed_map:
assumes hom: "homeomorphism S T f g"
and oo: "closedin (top_of_set S) U"
shows "closedin (top_of_set T) (f ` U)"
proof -
from hom oo have [simp]: "f ` U = T ∩ g -` U"
using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
from hom have "continuous_on T g"
unfolding homeomorphism_def by blast
moreover have "g ` T = S"
by (metis hom homeomorphism_def)
ultimately show ?thesis
by (simp add: continuous_on_closed oo)
qed
subsection ‹Seperability›
lemma subset_second_countable:
obtains ℬ :: "'a:: second_countable_topology set set"
where "countable ℬ"
"{} ∉ ℬ"
"⋀C. C ∈ ℬ ⟹ openin(top_of_set S) C"
"⋀T. openin(top_of_set S) T ⟹ ∃𝒰. 𝒰 ⊆ ℬ ∧ T = ⋃𝒰"
proof -
obtain ℬ :: "'a set set"
where "countable ℬ"
and opeB: "⋀C. C ∈ ℬ ⟹ openin(top_of_set S) C"
and ℬ: "⋀T. openin(top_of_set S) T ⟹ ∃𝒰. 𝒰 ⊆ ℬ ∧ T = ⋃𝒰"
proof -
obtain 𝒞 :: "'a set set"
where "countable 𝒞" and ope: "⋀C. C ∈ 𝒞 ⟹ open C"
and 𝒞: "⋀S. open S ⟹ ∃U. U ⊆ 𝒞 ∧ S = ⋃U"
by (metis univ_second_countable that)
show ?thesis
proof
show "countable ((λC. S ∩ C) ` 𝒞)"
by (simp add: ‹countable 𝒞›)
show "⋀C. C ∈ (∩) S ` 𝒞 ⟹ openin (top_of_set S) C"
using ope by auto
show "⋀T. openin (top_of_set S) T ⟹ ∃𝒰⊆(∩) S ` 𝒞. T = ⋃𝒰"
by (metis 𝒞 image_mono inf_Sup openin_open)
qed
qed
show ?thesis
proof
show "countable (ℬ - {{}})"
using ‹countable ℬ› by blast
show "⋀C. ⟦C ∈ ℬ - {{}}⟧ ⟹ openin (top_of_set S) C"
by (simp add: ‹⋀C. C ∈ ℬ ⟹ openin (top_of_set S) C›)
show "∃𝒰⊆ℬ - {{}}. T = ⋃𝒰" if "openin (top_of_set S) T" for T
using ℬ [OF that]
apply clarify
by (rule_tac x="𝒰 - {{}}" in exI, auto)
qed auto
qed
lemma Lindelof_openin:
fixes ℱ :: "'a::second_countable_topology set set"
assumes "⋀S. S ∈ ℱ ⟹ openin (top_of_set U) S"
obtains ℱ' where "ℱ' ⊆ ℱ" "countable ℱ'" "⋃ℱ' = ⋃ℱ"
proof -
have "⋀S. S ∈ ℱ ⟹ ∃T. open T ∧ S = U ∩ T"
using assms by (simp add: openin_open)
then obtain tf where tf: "⋀S. S ∈ ℱ ⟹ open (tf S) ∧ (S = U ∩ tf S)"
by metis
have [simp]: "⋀ℱ'. ℱ' ⊆ ℱ ⟹ ⋃ℱ' = U ∩ ⋃(tf ` ℱ')"
using tf by fastforce
obtain 𝒢 where "countable 𝒢 ∧ 𝒢 ⊆ tf ` ℱ" "⋃𝒢 = ⋃(tf ` ℱ)"
using tf by (force intro: Lindelof [of "tf ` ℱ"])
then obtain ℱ' where ℱ': "ℱ' ⊆ ℱ" "countable ℱ'" "⋃ℱ' = ⋃ℱ"
by (clarsimp simp add: countable_subset_image)
then show ?thesis ..
qed
subsection‹Closed Maps›
lemma continuous_imp_closed_map:
fixes f :: "'a::t2_space ⇒ 'b::t2_space"
assumes "closedin (top_of_set S) U"
"continuous_on S f" "f ` S = T" "compact S"
shows "closedin (top_of_set T) (f ` U)"
by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
lemma closed_map_restrict:
assumes cloU: "closedin (top_of_set (S ∩ f -` T')) U"
and cc: "⋀U. closedin (top_of_set S) U ⟹ closedin (top_of_set T) (f ` U)"
and "T' ⊆ T"
shows "closedin (top_of_set T') (f ` U)"
proof -
obtain V where "closed V" "U = S ∩ f -` T' ∩ V"
using cloU by (auto simp: closedin_closed)
with cc [of "S ∩ V"] ‹T' ⊆ T› show ?thesis
by (fastforce simp add: closedin_closed)
qed
subsection‹Open Maps›
lemma open_map_restrict:
assumes opeU: "openin (top_of_set (S ∩ f -` T')) U"
and oo: "⋀U. openin (top_of_set S) U ⟹ openin (top_of_set T) (f ` U)"
and "T' ⊆ T"
shows "openin (top_of_set T') (f ` U)"
proof -
obtain V where "open V" "U = S ∩ f -` T' ∩ V"
using opeU by (auto simp: openin_open)
with oo [of "S ∩ V"] ‹T' ⊆ T› show ?thesis
by (fastforce simp add: openin_open)
qed
subsection‹Quotient maps›
lemma quotient_map_imp_continuous_open:
assumes T: "f ∈ S → T"
and ope: "⋀U. U ⊆ T
⟹ (openin (top_of_set S) (S ∩ f -` U) ⟷
openin (top_of_set T) U)"
shows "continuous_on S f"
proof -
have [simp]: "S ∩ f -` f ` S = S" by auto
show ?thesis
by (meson T continuous_on_open_gen ope openin_imp_subset)
qed
lemma quotient_map_imp_continuous_closed:
assumes T: "f ∈ S → T"
and ope: "⋀U. U ⊆ T
⟹ (closedin (top_of_set S) (S ∩ f -` U) ⟷
closedin (top_of_set T) U)"
shows "continuous_on S f"
proof -
have [simp]: "S ∩ f -` f ` S = S" by auto
show ?thesis
by (meson T closedin_imp_subset continuous_on_closed_gen ope)
qed
lemma open_map_imp_quotient_map:
assumes contf: "continuous_on S f"
and T: "T ⊆ f ` S"
and ope: "⋀T. openin (top_of_set S) T
⟹ openin (top_of_set (f ` S)) (f ` T)"
shows "openin (top_of_set S) (S ∩ f -` T) =
openin (top_of_set (f ` S)) T"
proof -
have "T = f ` (S ∩ f -` T)"
using T by blast
then show ?thesis
using "ope" contf continuous_on_open by metis
qed
lemma closed_map_imp_quotient_map:
assumes contf: "continuous_on S f"
and T: "T ⊆ f ` S"
and ope: "⋀T. closedin (top_of_set S) T
⟹ closedin (top_of_set (f ` S)) (f ` T)"
shows "openin (top_of_set S) (S ∩ f -` T) ⟷
openin (top_of_set (f ` S)) T"
(is "?lhs = ?rhs")
proof
assume ?lhs
then have *: "closedin (top_of_set S) (S - (S ∩ f -` T))"
using closedin_diff by fastforce
have [simp]: "(f ` S - f ` (S - (S ∩ f -` T))) = T"
using T by blast
show ?rhs
using ope [OF *, unfolded closedin_def] by auto
next
assume ?rhs
with contf show ?lhs
by (auto simp: continuous_on_open)
qed
lemma continuous_right_inverse_imp_quotient_map:
assumes contf: "continuous_on S f" and imf: "f ∈ S → T"
and contg: "continuous_on T g" and img: "g ∈ T → S"
and fg [simp]: "⋀y. y ∈ T ⟹ f(g y) = y"
and U: "U ⊆ T"
shows "openin (top_of_set S) (S ∩ f -` U) ⟷
openin (top_of_set T) U"
(is "?lhs = ?rhs")
proof -
have f: "⋀Z. openin (top_of_set (f ` S)) Z ⟹
openin (top_of_set S) (S ∩ f -` Z)"
and g: "⋀Z. openin (top_of_set (g ` T)) Z ⟹
openin (top_of_set T) (T ∩ g -` Z)"
using contf contg by (auto simp: continuous_on_open)
show ?thesis
proof
have "T ∩ g -` (g ` T ∩ (S ∩ f -` U)) = {x ∈ T. f (g x) ∈ U}"
using imf img by blast
also have "... = U"
using U by auto
finally have eq: "T ∩ g -` (g ` T ∩ (S ∩ f -` U)) = U" .
assume ?lhs
then have *: "openin (top_of_set (g ` T)) (g ` T ∩ (S ∩ f -` U))"
by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self image_subset_iff_funcset)
show ?rhs
using g [OF *] eq by auto
next
assume rhs: ?rhs
show ?lhs
using assms continuous_openin_preimage rhs by blast
qed
qed
lemma continuous_left_inverse_imp_quotient_map:
assumes "continuous_on S f"
and "continuous_on (f ` S) g"
and "⋀x. x ∈ S ⟹ g(f x) = x"
and "U ⊆ f ` S"
shows "openin (top_of_set S) (S ∩ f -` U) ⟷
openin (top_of_set (f ` S)) U"
using assms
by (intro continuous_right_inverse_imp_quotient_map) auto
lemma continuous_imp_quotient_map:
fixes f :: "'a::t2_space ⇒ 'b::t2_space"
assumes "continuous_on S f" "f ` S = T" "compact S" "U ⊆ T"
shows "openin (top_of_set S) (S ∩ f -` U) ⟷
openin (top_of_set T) U"
by (simp add: assms closed_map_imp_quotient_map continuous_imp_closed_map)
subsection‹Pasting lemmas for functions, for of casewise definitions›
subsubsection‹on open sets›
lemma pasting_lemma:
assumes ope: "⋀i. i ∈ I ⟹ openin X (T i)"
and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)"
and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x"
and g: "⋀x. x ∈ topspace X ⟹ ∃j. j ∈ I ∧ x ∈ T j ∧ g x = f j x"
shows "continuous_map X Y g"
unfolding continuous_map_openin_preimage_eq
proof (intro conjI allI impI)
show "g ∈ topspace X → topspace Y"
using g cont continuous_map_image_subset_topspace by fastforce
next
fix U
assume Y: "openin Y U"
have T: "T i ⊆ topspace X" if "i ∈ I" for i
using ope by (simp add: openin_subset that)
have *: "topspace X ∩ g -` U = (⋃i ∈ I. T i ∩ f i -` U)"
using f g T by fastforce
have "⋀i. i ∈ I ⟹ openin X (T i ∩ f i -` U)"
using cont unfolding continuous_map_openin_preimage_eq
by (metis Y T inf.commute inf_absorb1 ope topspace_subtopology openin_trans_full)
then show "openin X (topspace X ∩ g -` U)"
by (auto simp: *)
qed
lemma pasting_lemma_exists:
assumes X: "topspace X ⊆ (⋃i ∈ I. T i)"
and ope: "⋀i. i ∈ I ⟹ openin X (T i)"
and cont: "⋀i. i ∈ I ⟹ continuous_map (subtopology X (T i)) Y (f i)"
and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x"
obtains g where "continuous_map X Y g" "⋀x i. ⟦i ∈ I; x ∈ topspace X ∩ T i⟧ ⟹ g x = f i x"
proof
let ?h = "λx. f (SOME i. i ∈ I ∧ x ∈ T i) x"
show "continuous_map X Y ?h"
apply (rule pasting_lemma [OF ope cont])
apply (blast intro: f)+
by (metis (no_types, lifting) UN_E X subsetD someI_ex)
show "f (SOME i. i ∈ I ∧ x ∈ T i) x = f i x" if "i ∈ I" "x ∈ topspace X ∩ T i" for i x
by (metis (no_types, lifting) IntD2 IntI f someI_ex that)
qed
lemma pasting_lemma_locally_finite:
assumes fin: "⋀x. x ∈ topspace X ⟹ ∃V. openin X V ∧ x ∈ V ∧ finite {i ∈ I. T i ∩ V ≠ {}}"
and clo: "⋀i. i ∈ I ⟹ closedin X (T i)"
and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)"
and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x"
and g: "⋀x. x ∈ topspace X ⟹ ∃j. j ∈ I ∧ x ∈ T j ∧ g x = f j x"
shows "continuous_map X Y g"
unfolding continuous_map_closedin_preimage_eq
proof (intro conjI allI impI)
show "g ∈ topspace X → topspace Y"
using g cont continuous_map_image_subset_topspace by fastforce
next
fix U
assume Y: "closedin Y U"
have T: "T i ⊆ topspace X" if "i ∈ I" for i
using clo by (simp add: closedin_subset that)
have *: "topspace X ∩ g -` U = (⋃i ∈ I. T i ∩ f i -` U)"
using f g T by fastforce
have cTf: "⋀i. i ∈ I ⟹ closedin X (T i ∩ f i -` U)"
using cont unfolding continuous_map_closedin_preimage_eq topspace_subtopology
by (simp add: Int_absorb1 T Y clo closedin_closed_subtopology)
have sub: "{Z ∈ (λi. T i ∩ f i -` U) ` I. Z ∩ V ≠ {}}
⊆ (λi. T i ∩ f i -` U) ` {i ∈ I. T i ∩ V ≠ {}}" for V
by auto
have 1: "(⋃i∈I. T i ∩ f i -` U) ⊆ topspace X"
using T by blast
then have "locally_finite_in X ((λi. T i ∩ f i -` U) ` I)"
unfolding locally_finite_in_def
using finite_subset [OF sub] fin by force
then show "closedin X (topspace X ∩ g -` U)"
by (smt (verit, best) * cTf closedin_locally_finite_Union image_iff)
qed
subsubsection‹Likewise on closed sets, with a finiteness assumption›
lemma pasting_lemma_closed:
assumes fin: "finite I"
and clo: "⋀i. i ∈ I ⟹ closedin X (T i)"
and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)"
and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x"
and g: "⋀x. x ∈ topspace X ⟹ ∃j. j ∈ I ∧ x ∈ T j ∧ g x = f j x"
shows "continuous_map X Y g"
using pasting_lemma_locally_finite [OF _ clo cont f g] fin by auto
lemma pasting_lemma_exists_locally_finite:
assumes fin: "⋀x. x ∈ topspace X ⟹ ∃V. openin X V ∧ x ∈ V ∧ finite {i ∈ I. T i ∩ V ≠ {}}"
and X: "topspace X ⊆ ⋃(T ` I)"
and clo: "⋀i. i ∈ I ⟹ closedin X (T i)"
and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)"
and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x"
and g: "⋀x. x ∈ topspace X ⟹ ∃j. j ∈ I ∧ x ∈ T j ∧ g x = f j x"
obtains g where "continuous_map X Y g" "⋀x i. ⟦i ∈ I; x ∈ topspace X ∩ T i⟧ ⟹ g x = f i x"
proof
show "continuous_map X Y (λx. f(@i. i ∈ I ∧ x ∈ T i) x)"
apply (rule pasting_lemma_locally_finite [OF fin])
apply (blast intro: assms)+
by (metis (no_types, lifting) UN_E X set_rev_mp someI_ex)
next
fix x i
assume "i ∈ I" and "x ∈ topspace X ∩ T i"
then show "f (SOME i. i ∈ I ∧ x ∈ T i) x = f i x"
by (metis (mono_tags, lifting) IntE IntI f someI2)
qed
lemma pasting_lemma_exists_closed:
assumes fin: "finite I"
and X: "topspace X ⊆ ⋃(T ` I)"
and clo: "⋀i. i ∈ I ⟹ closedin X (T i)"
and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)"
and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x"
obtains g where "continuous_map X Y g" "⋀x i. ⟦i ∈ I; x ∈ topspace X ∩ T i⟧ ⟹ g x = f i x"
proof
show "continuous_map X Y (λx. f (SOME i. i ∈ I ∧ x ∈ T i) x)"
apply (rule pasting_lemma_closed [OF ‹finite I› clo cont])
apply (blast intro: f)+
by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff)
next
fix x i
assume "i ∈ I" "x ∈ topspace X ∩ T i"
then show "f (SOME i. i ∈ I ∧ x ∈ T i) x = f i x"
by (metis (no_types, lifting) IntD2 IntI f someI_ex)
qed
lemma continuous_map_cases:
assumes f: "continuous_map (subtopology X (X closure_of {x. P x})) Y f"
and g: "continuous_map (subtopology X (X closure_of {x. ¬ P x})) Y g"
and fg: "⋀x. x ∈ X frontier_of {x. P x} ⟹ f x = g x"
shows "continuous_map X Y (λx. if P x then f x else g x)"
proof (rule pasting_lemma_closed)
let ?f = "λb. if b then f else g"
let ?g = "λx. if P x then f x else g x"
let ?T = "λb. if b then X closure_of {x. P x} else X closure_of {x. ~P x}"
show "finite {True,False}" by auto
have eq: "topspace X - Collect P = topspace X ∩ {x. ¬ P x}"
by blast
show "?f i x = ?f j x"
if "i ∈ {True,False}" "j ∈ {True,False}" and x: "x ∈ topspace X ∩ ?T i ∩ ?T j" for i j x
proof -
have "f x = g x" if "i" "¬ j"
by (smt (verit, best) Diff_Diff_Int closure_of_interior_of closure_of_restrict eq fg
frontier_of_closures interior_of_complement that x)
moreover
have "g x = f x"
if "x ∈ X closure_of {x. ¬ P x}" "x ∈ X closure_of Collect P" "¬ i" "j" for x
by (metis IntI closure_of_restrict eq fg frontier_of_closures that)
ultimately show ?thesis
using that by (auto simp flip: closure_of_restrict)
qed
show "∃j. j ∈ {True,False} ∧ x ∈ ?T j ∧ (if P x then f x else g x) = ?f j x"
if "x ∈ topspace X" for x
by simp (metis in_closure_of mem_Collect_eq that)
qed (auto simp: f g)
lemma continuous_map_cases_alt:
assumes f: "continuous_map (subtopology X (X closure_of {x ∈ topspace X. P x})) Y f"
and g: "continuous_map (subtopology X (X closure_of {x ∈ topspace X. ~P x})) Y g"
and fg: "⋀x. x ∈ X frontier_of {x ∈ topspace X. P x} ⟹ f x = g x"
shows "continuous_map X Y (λx. if P x then f x else g x)"
apply (rule continuous_map_cases)
using assms
apply (simp_all add: Collect_conj_eq closure_of_restrict [symmetric] frontier_of_restrict [symmetric])
done
lemma continuous_map_cases_function:
assumes contp: "continuous_map X Z p"
and contf: "continuous_map (subtopology X {x ∈ topspace X. p x ∈ Z closure_of U}) Y f"
and contg: "continuous_map (subtopology X {x ∈ topspace X. p x ∈ Z closure_of (topspace Z - U)}) Y g"
and fg: "⋀x. ⟦x ∈ topspace X; p x ∈ Z frontier_of U⟧ ⟹ f x = g x"
shows "continuous_map X Y (λx. if p x ∈ U then f x else g x)"
proof (rule continuous_map_cases_alt)
show "continuous_map (subtopology X (X closure_of {x ∈ topspace X. p x ∈ U})) Y f"
proof (rule continuous_map_from_subtopology_mono)
let ?T = "{x ∈ topspace X. p x ∈ Z closure_of U}"
show "continuous_map (subtopology X ?T) Y f"
by (simp add: contf)
show "X closure_of {x ∈ topspace X. p x ∈ U} ⊆ ?T"
by (rule continuous_map_closure_preimage_subset [OF contp])
qed
show "continuous_map (subtopology X (X closure_of {x ∈ topspace X. p x ∉ U})) Y g"
proof (rule continuous_map_from_subtopology_mono)
let ?T = "{x ∈ topspace X. p x ∈ Z closure_of (topspace Z - U)}"
show "continuous_map (subtopology X ?T) Y g"
by (simp add: contg)
have "X closure_of {x ∈ topspace X. p x ∉ U} ⊆ X closure_of {x ∈ topspace X. p x ∈ topspace Z - U}"
by (smt (verit) Collect_mono_iff DiffI closure_of_mono continuous_map contp image_subset_iff)
then show "X closure_of {x ∈ topspace X. p x ∉ U} ⊆ ?T"
by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]])
qed
next
show "f x = g x" if "x ∈ X frontier_of {x ∈ topspace X. p x ∈ U}" for x
using that continuous_map_frontier_frontier_preimage_subset [OF contp, of U] fg by blast
qed
subsection ‹Retractions›
definition retraction :: "('a::topological_space) set ⇒ 'a set ⇒ ('a ⇒ 'a) ⇒ bool"
where "retraction S T r ⟷
T ⊆ S ∧ continuous_on S r ∧ r ∈ S → T ∧ (∀x∈T. r x = x)"
definition retract_of (infixl "retract'_of" 50) where
"T retract_of S ⟷ (∃r. retraction S T r)"
lemma retraction_idempotent: "retraction S T r ⟹ x ∈ S ⟹ r (r x) = r x"
unfolding retraction_def by auto
text ‹Preservation of fixpoints under (more general notion of) retraction›
lemma invertible_fixpoint_property:
fixes S :: "'a::topological_space set"
and T :: "'b::topological_space set"
assumes contt: "continuous_on T i"
and "i ∈ T → S"
and contr: "continuous_on S r"
and "r ∈ S → T"
and ri: "⋀y. y ∈ T ⟹ r (i y) = y"
and FP: "⋀f. ⟦continuous_on S f; f ∈ S → S⟧ ⟹ ∃x∈S. f x = x"
and contg: "continuous_on T g"
and "g ∈ T → T"
obtains y where "y ∈ T" and "g y = y"
proof -
have "∃x∈S. (i ∘ g ∘ r) x = x"
proof (rule FP)
show "continuous_on S (i ∘ g ∘ r)"
by (metis assms(4) assms(8) contg continuous_on_compose continuous_on_subset contr contt funcset_image)
show "(i ∘ g ∘ r) ∈ S → S"
using assms(2,4,8) by force
qed
then obtain x where x: "x ∈ S" "(i ∘ g ∘ r) x = x" ..
then have *: "g (r x) ∈ T"
using assms(4,8) by auto
have "r ((i ∘ g ∘ r) x) = r x"
using x by auto
then show ?thesis
using "*" ri that by auto
qed
lemma homeomorphic_fixpoint_property:
fixes S :: "'a::topological_space set"
and T :: "'b::topological_space set"
assumes "S homeomorphic T"
shows "(∀f. continuous_on S f ∧ f ∈ S → S ⟶ (∃x∈S. f x = x)) ⟷
(∀g. continuous_on T g ∧ g ∈ T → T ⟶ (∃y∈T. g y = y))"
(is "?lhs = ?rhs")
proof -
obtain r i where r:
"∀x∈S. i (r x) = x" "r ` S = T" "continuous_on S r"
"∀y∈T. r (i y) = y" "i ` T = S" "continuous_on T i"
using assms unfolding homeomorphic_def homeomorphism_def by blast
show ?thesis
proof
assume ?lhs
with r show ?rhs
by (smt (verit, del_insts) Pi_iff image_eqI invertible_fixpoint_property[of T i S r])
next
assume ?rhs
with r show ?lhs
by (smt (verit, del_insts) Pi_iff image_eqI invertible_fixpoint_property[of S r T i])
qed
qed
lemma retract_fixpoint_property:
fixes f :: "'a::topological_space ⇒ 'b::topological_space"
and S :: "'a set"
assumes "T retract_of S"
and FP: "⋀f. ⟦continuous_on S f; f ∈ S → S⟧ ⟹ ∃x∈S. f x = x"
and contg: "continuous_on T g"
and "g ∈ T → T"
obtains y where "y ∈ T" and "g y = y"
proof -
obtain h where "retraction S T h"
using assms(1) unfolding retract_of_def ..
then show ?thesis
unfolding retraction_def
using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
by (smt (verit, del_insts) Pi_iff assms(4) contg subsetD that)
qed
lemma retraction:
"retraction S T r ⟷ T ⊆ S ∧ continuous_on S r ∧ r ` S = T ∧ (∀x ∈ T. r x = x)"
by (force simp: retraction_def simp flip: image_subset_iff_funcset)
lemma retractionE:
assumes "retraction S T r"
obtains "T = r ` S" "r ∈ S → S" "continuous_on S r" "⋀x. x ∈ S ⟹ r (r x) = r x"
proof (rule that)
from retraction [of S T r] assms
have "T ⊆ S" "continuous_on S r" "r ` S = T" and "∀x ∈ T. r x = x"
by simp_all
then show "r ∈ S → S" "continuous_on S r"
by auto
then show "T = r ` S"
using ‹r ` S = T› by blast
from ‹∀x ∈ T. r x = x› have "r x = x" if "x ∈ T" for x
using that by simp
with ‹r ` S = T› show "r (r x) = r x" if "x ∈ S" for x
using that by auto
qed
lemma retract_ofE:
assumes "T retract_of S"
obtains r where "T = r ` S" "r ∈ S → S" "continuous_on S r" "⋀x. x ∈ S ⟹ r (r x) = r x"
proof -
from assms obtain r where "retraction S T r"
by (auto simp add: retract_of_def)
with that show thesis
by (auto elim: retractionE)
qed
lemma retract_of_imp_extensible:
assumes "S retract_of T" and "continuous_on S f" and "f ∈ S → U"
obtains g where "continuous_on T g" "g ∈ T → U" "⋀x. x ∈ S ⟹ g x = f x"
proof -
from ‹S retract_of T› obtain r where "retraction T S r"
by (auto simp add: retract_of_def)
then have "continuous_on T (f ∘ r)"
by (metis assms(2) continuous_on_compose retraction)
then show thesis
by (smt (verit, best) Pi_iff ‹retraction T S r› assms(3) comp_apply retraction_def that)
qed
lemma idempotent_imp_retraction:
assumes "continuous_on S f" and "f ∈ S → S" and "⋀x. x ∈ S ⟹ f(f x) = f x"
shows "retraction S (f ` S) f"
by (simp add: assms funcset_image retraction)
lemma retraction_subset:
assumes "retraction S T r" and "T ⊆ S'" and "S' ⊆ S"
shows "retraction S' T r"
unfolding retraction_def
by (metis assms continuous_on_subset image_mono image_subset_iff_funcset retraction)
lemma retract_of_subset:
assumes "T retract_of S" and "T ⊆ S'" and "S' ⊆ S"
shows "T retract_of S'"
by (meson assms retract_of_def retraction_subset)
lemma retraction_refl [simp]: "retraction S S (λx. x)"
by (simp add: retraction)
lemma retract_of_refl [iff]: "S retract_of S"
unfolding retract_of_def retraction_def
using continuous_on_id by blast
lemma retract_of_imp_subset:
"S retract_of T ⟹ S ⊆ T"
by (simp add: retract_of_def retraction_def)
lemma retract_of_empty [simp]:
"({} retract_of S) ⟷ S = {}" "(S retract_of {}) ⟷ S = {}"
by (auto simp: retract_of_def retraction_def)
lemma retract_of_singleton [iff]: "({x} retract_of S) ⟷ x ∈ S"
unfolding retract_of_def retraction_def by force
lemma retraction_comp:
"⟦retraction S T f; retraction T U g⟧ ⟹ retraction S U (g ∘ f)"
by (smt (verit, best) comp_apply continuous_on_compose image_comp retraction subset_iff)
lemma retract_of_trans [trans]:
assumes "S retract_of T" and "T retract_of U"
shows "S retract_of U"
using assms by (auto simp: retract_of_def intro: retraction_comp)
lemma closedin_retract:
fixes S :: "'a :: t2_space set"
assumes "S retract_of T"
shows "closedin (top_of_set T) S"
proof -
obtain r where r: "S ⊆ T" "continuous_on T r" "r ∈ T → S" "⋀x. x ∈ S ⟹ r x = x"
using assms by (auto simp: retract_of_def retraction_def)
have "S = {x∈T. x = r x}"
using r by force
also have "… = T ∩ ((λx. (x, r x)) -` ({y. ∃x. y = (x, x)}))"
unfolding vimage_def mem_Times_iff fst_conv snd_conv
using r
by auto
also have "closedin (top_of_set T) …"
by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r)
finally show ?thesis .
qed
lemma closedin_self [simp]: "closedin (top_of_set S) S"
by simp
lemma retract_of_closed:
fixes S :: "'a :: t2_space set"
shows "⟦closed T; S retract_of T⟧ ⟹ closed S"
by (metis closedin_retract closedin_closed_eq)
lemma retract_of_compact:
"⟦compact T; S retract_of T⟧ ⟹ compact S"
by (metis compact_continuous_image retract_of_def retraction)
lemma retract_of_connected:
"⟦connected T; S retract_of T⟧ ⟹ connected S"
by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
lemma retraction_openin_vimage_iff:
assumes r: "retraction S T r" and "U ⊆ T"
shows "openin (top_of_set S) (S ∩ r -` U) ⟷ openin (top_of_set T) U" (is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
using r
by (smt (verit, del_insts) assms(2) continuous_right_inverse_imp_quotient_map image_subset_iff_funcset r retractionE retraction_def retraction_subset)
show "?rhs ⟹ ?lhs"
by (metis continuous_on_open r retraction)
qed
lemma retract_of_Times:
"⟦S retract_of S'; T retract_of T'⟧ ⟹ (S × T) retract_of (S' × T')"
apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
apply (rename_tac f g)
apply (rule_tac x="λz. ((f ∘ fst) z, (g ∘ snd) z)" in exI)
apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
done
subsection‹Retractions on a topological space›
definition retract_of_space :: "'a set ⇒ 'a topology ⇒ bool" (infix "retract'_of'_space" 50)
where "S retract_of_space X
≡ S ⊆ topspace X ∧ (∃r. continuous_map X (subtopology X S) r ∧ (∀x ∈ S. r x = x))"
lemma retract_of_space_retraction_maps:
"S retract_of_space X ⟷ S ⊆ topspace X ∧ (∃r. retraction_maps X (subtopology X S) r id)"
by (auto simp: retract_of_space_def retraction_maps_def)
lemma retract_of_space_section_map:
"S retract_of_space X ⟷ S ⊆ topspace X ∧ section_map (subtopology X S) X id"
unfolding retract_of_space_def retraction_maps_def section_map_def
by (auto simp: continuous_map_from_subtopology)
lemma retract_of_space_imp_subset:
"S retract_of_space X ⟹ S ⊆ topspace X"
by (simp add: retract_of_space_def)
lemma retract_of_space_topspace:
"topspace X retract_of_space X"
using retract_of_space_def by force
lemma retract_of_space_empty [simp]:
"{} retract_of_space X ⟷ X = trivial_topology"
by (auto simp: retract_of_space_def)
lemma retract_of_space_singleton [simp]:
"{a} retract_of_space X ⟷ a ∈ topspace X"
proof -
have "continuous_map X (subtopology X {a}) (λx. a) ∧ (λx. a) a = a" if "a ∈ topspace X"
using that by simp
then show ?thesis
by (force simp: retract_of_space_def)
qed
lemma retract_of_space_trans:
assumes "S retract_of_space X" "T retract_of_space subtopology X S"
shows "T retract_of_space X"
using assms
apply (simp add: retract_of_space_retraction_maps)
by (metis id_comp inf.absorb_iff2 retraction_maps_compose subtopology_subtopology)
lemma retract_of_space_subtopology:
assumes "S retract_of_space X" "S ⊆ U"
shows "S retract_of_space subtopology X U"
using assms
apply (clarsimp simp: retract_of_space_def)
by (metis continuous_map_from_subtopology inf.absorb2 subtopology_subtopology)
lemma retract_of_space_clopen:
assumes "openin X S" "closedin X S" "S = {} ⟹ X = trivial_topology"
shows "S retract_of_space X"
proof (cases "S = {}")
case False
then obtain a where "a ∈ S"
by blast
show ?thesis
unfolding retract_of_space_def
proof (intro exI conjI)
show "S ⊆ topspace X"
by (simp add: assms closedin_subset)
have "continuous_map X X (λx. if x ∈ S then x else a)"
proof (rule continuous_map_cases)
show "continuous_map (subtopology X (X closure_of {x. x ∈ S})) X (λx. x)"
by (simp add: continuous_map_from_subtopology)
show "continuous_map (subtopology X (X closure_of {x. x ∉ S})) X (λx. a)"
using ‹S ⊆ topspace X› ‹a ∈ S› by force
show "x = a" if "x ∈ X frontier_of {x. x ∈ S}" for x
using assms that clopenin_eq_frontier_of by fastforce
qed
then show "continuous_map X (subtopology X S) (λx. if x ∈ S then x else a)"
using ‹S ⊆ topspace X› ‹a ∈ S› by (auto simp: continuous_map_in_subtopology)
qed auto
qed (use assms in auto)
lemma retract_of_space_disjoint_union:
assumes "openin X S" "openin X T" and ST: "disjnt S T" "S ∪ T = topspace X" and "S = {} ⟹ X = trivial_topology"
shows "S retract_of_space X"
proof (rule retract_of_space_clopen)
have "S ∩ T = {}"
by (meson ST disjnt_def)
then have "S = topspace X - T"
using ST by auto
then show "closedin X S"
using ‹openin X T› by blast
qed (auto simp: assms)
lemma retraction_maps_section_image1:
assumes "retraction_maps X Y r s"
shows "s ` (topspace Y) retract_of_space X"
unfolding retract_of_space_section_map
proof
show "s ` topspace Y ⊆ topspace X"
using assms continuous_map_image_subset_topspace retraction_maps_def by blast
show "section_map (subtopology X (s ` topspace Y)) X id"
unfolding section_map_def
using assms retraction_maps_to_retract_maps by blast
qed
lemma retraction_maps_section_image2:
"retraction_maps X Y r s
⟹ subtopology X (s ` (topspace Y)) homeomorphic_space Y"
using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map
section_map_def by blast
lemma hereditary_imp_retractive_property:
assumes "⋀X S. P X ⟹ P(subtopology X S)"
"⋀X X'. X homeomorphic_space X' ⟹ (P X ⟷ Q X')"
assumes "retraction_map X X' r" "P X"
shows "Q X'"
by (meson assms retraction_map_def retraction_maps_section_image2)
subsection‹Paths and path-connectedness›
definition pathin :: "'a topology ⇒ (real ⇒ 'a) ⇒ bool" where
"pathin X g ≡ continuous_map (subtopology euclideanreal {0..1}) X g"
lemma pathin_compose:
"⟦pathin X g; continuous_map X Y f⟧ ⟹ pathin Y (f ∘ g)"
by (simp add: continuous_map_compose pathin_def)
lemma pathin_subtopology:
"pathin (subtopology X S) g ⟷ pathin X g ∧ (∀x ∈ {0..1}. g x ∈ S)"
by (auto simp: pathin_def continuous_map_in_subtopology)
lemma pathin_const [simp]: "pathin X (λx. a) ⟷ a ∈ topspace X"
using pathin_subtopology by (fastforce simp add: pathin_def)
lemma path_start_in_topspace: "pathin X g ⟹ g 0 ∈ topspace X"
by (force simp: pathin_def continuous_map)
lemma path_finish_in_topspace: "pathin X g ⟹ g 1 ∈ topspace X"
by (force simp: pathin_def continuous_map)
lemma path_image_subset_topspace: "pathin X g ⟹ g ∈ ({0..1}) → topspace X"
by (force simp: pathin_def continuous_map)
definition path_connected_space :: "'a topology ⇒ bool"
where "path_connected_space X ≡ ∀x ∈ topspace X. ∀ y ∈ topspace X. ∃g. pathin X g ∧ g 0 = x ∧ g 1 = y"
definition path_connectedin :: "'a topology ⇒ 'a set ⇒ bool"
where "path_connectedin X S ≡ S ⊆ topspace X ∧ path_connected_space(subtopology X S)"
lemma path_connectedin_absolute [simp]:
"path_connectedin (subtopology X S) S ⟷ path_connectedin X S"
by (simp add: path_connectedin_def subtopology_subtopology)
lemma path_connectedin_subset_topspace:
"path_connectedin X S ⟹ S ⊆ topspace X"
by (simp add: path_connectedin_def)
lemma path_connectedin_subtopology:
"path_connectedin (subtopology X S) T ⟷ path_connectedin X T ∧ T ⊆ S"
by (auto simp: path_connectedin_def subtopology_subtopology inf.absorb2)
lemma path_connectedin:
"path_connectedin X S ⟷
S ⊆ topspace X ∧
(∀x ∈ S. ∀y ∈ S. ∃g. pathin X g ∧ g ∈ {0..1} → S ∧ g 0 = x ∧ g 1 = y)"
unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology
by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 flip: image_subset_iff_funcset)
lemma path_connectedin_topspace:
"path_connectedin X (topspace X) ⟷ path_connected_space X"
by (simp add: path_connectedin_def)
lemma path_connected_imp_connected_space:
assumes "path_connected_space X"
shows "connected_space X"
proof -
have *: "∃S. connectedin X S ∧ g 0 ∈ S ∧ g 1 ∈ S" if "pathin X g" for g
proof (intro exI conjI)
have "continuous_map (subtopology euclideanreal {0..1}) X g"
using connectedin_absolute that by (simp add: pathin_def)
then show "connectedin X (g ` {0..1})"
by (rule connectedin_continuous_map_image) auto
qed auto
show ?thesis
using assms
by (auto intro: * simp add: path_connected_space_def connected_space_subconnected Ball_def)
qed
lemma path_connectedin_imp_connectedin:
"path_connectedin X S ⟹ connectedin X S"
by (simp add: connectedin_def path_connected_imp_connected_space path_connectedin_def)
lemma path_connected_space_topspace_empty:
"path_connected_space trivial_topology"
by (simp add: path_connected_space_def)
lemma path_connectedin_empty [simp]: "path_connectedin X {}"
by (simp add: path_connectedin)
lemma path_connectedin_singleton [simp]: "path_connectedin X {a} ⟷ a ∈ topspace X"
proof
show "path_connectedin X {a} ⟹ a ∈ topspace X"
by (simp add: path_connectedin)
show "a ∈ topspace X ⟹ path_connectedin X {a}"
unfolding path_connectedin
using pathin_const by fastforce
qed
lemma path_connectedin_continuous_map_image:
assumes f: "continuous_map X Y f" and S: "path_connectedin X S"
shows "path_connectedin Y (f ` S)"
proof -
have fX: "f ∈ (topspace X) → topspace Y"
using continuous_map_def f by fastforce
show ?thesis
unfolding path_connectedin
proof (intro conjI ballI; clarify?)
fix x
assume "x ∈ S"
show "f x ∈ topspace Y"
using S ‹x ∈ S› fX path_connectedin_subset_topspace by fastforce
next
fix x y
assume "x ∈ S" and "y ∈ S"
then obtain g where g: "pathin X g" "g ∈ {0..1} → S" "g 0 = x" "g 1 = y"
using S by (force simp: path_connectedin)
show "∃g. pathin Y g ∧ g ∈ {0..1} → f ` S ∧ g 0 = f x ∧ g 1 = f y"
proof (intro exI conjI)
show "pathin Y (f ∘ g)"
using ‹pathin X g› f pathin_compose by auto
qed (use g in auto)
qed
qed
lemma path_connectedin_discrete_topology:
"path_connectedin (discrete_topology U) S ⟷ S ⊆ U ∧ (∃a. S ⊆ {a})" (is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
by (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
show "?rhs ⟹ ?lhs"
using subset_singletonD by fastforce
qed
lemma path_connected_space_discrete_topology:
"path_connected_space (discrete_topology U) ⟷ (∃a. U ⊆ {a})"
by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty
subset_singletonD topspace_discrete_topology)
lemma homeomorphic_path_connected_space_imp:
"⟦path_connected_space X; X homeomorphic_space Y⟧ ⟹ path_connected_space Y"
unfolding homeomorphic_space_def homeomorphic_maps_def
by (smt (verit, ccfv_threshold) homeomorphic_imp_surjective_map homeomorphic_maps_def homeomorphic_maps_map path_connectedin_continuous_map_image path_connectedin_topspace)
lemma homeomorphic_path_connected_space:
"X homeomorphic_space Y ⟹ path_connected_space X ⟷ path_connected_space Y"
by (meson homeomorphic_path_connected_space_imp homeomorphic_space_sym)
lemma homeomorphic_map_path_connectedness:
assumes "homeomorphic_map X Y f" "U ⊆ topspace X"
shows "path_connectedin Y (f ` U) ⟷ path_connectedin X U"
unfolding path_connectedin_def
proof (intro conj_cong homeomorphic_path_connected_space)
show "f ` U ⊆ topspace Y ⟷ (U ⊆ topspace X)"
using assms homeomorphic_imp_surjective_map by blast
next
assume "U ⊆ topspace X"
show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
using assms unfolding homeomorphic_eq_everything_map
by (metis (no_types, opaque_lifting) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2)
qed
lemma homeomorphic_map_path_connectedness_eq:
"homeomorphic_map X Y f ⟹ path_connectedin X U ⟷ U ⊆ topspace X ∧ path_connectedin Y (f ` U)"
by (meson homeomorphic_map_path_connectedness path_connectedin_def)
subsection‹Connected components›
definition connected_component_of :: "'a topology ⇒ 'a ⇒ 'a ⇒ bool"
where "connected_component_of X x y ≡
∃T. connectedin X T ∧ x ∈ T ∧ y ∈ T"
abbreviation connected_component_of_set
where "connected_component_of_set X x ≡ Collect (connected_component_of X x)"
definition connected_components_of :: "'a topology ⇒ ('a set) set"
where "connected_components_of X ≡ connected_component_of_set X ` topspace X"
lemma connected_component_in_topspace:
"connected_component_of X x y ⟹ x ∈ topspace X ∧ y ∈ topspace X"
by (meson connected_component_of_def connectedin_subset_topspace in_mono)
lemma connected_component_of_refl:
"connected_component_of X x x ⟷ x ∈ topspace X"
by (meson connected_component_in_topspace connected_component_of_def connectedin_sing insertI1)
lemma connected_component_of_sym:
"connected_component_of X x y ⟷ connected_component_of X y x"
by (meson connected_component_of_def)
lemma connected_component_of_trans:
"⟦connected_component_of X x y; connected_component_of X y z⟧
⟹ connected_component_of X x z"
unfolding connected_component_of_def
using connectedin_Un by blast
lemma connected_component_of_mono:
"⟦connected_component_of (subtopology X S) x y; S ⊆ T⟧
⟹ connected_component_of (subtopology X T) x y"
by (metis connected_component_of_def connectedin_subtopology inf.absorb_iff2 subtopology_subtopology)
lemma connected_component_of_set:
"connected_component_of_set X x = {y. ∃T. connectedin X T ∧ x ∈ T ∧ y ∈ T}"
by (meson connected_component_of_def)
lemma connected_component_of_subset_topspace:
"connected_component_of_set X x ⊆ topspace X"
using connected_component_in_topspace by force
lemma connected_component_of_eq_empty:
"connected_component_of_set X x = {} ⟷ (x ∉ topspace X)"
using connected_component_in_topspace connected_component_of_refl by fastforce
lemma connected_space_iff_connected_component:
"connected_space X ⟷ (∀x ∈ topspace X. ∀y ∈ topspace X. connected_component_of X x y)"
by (simp add: connected_component_of_def connected_space_subconnected)
lemma connected_space_imp_connected_component_of:
"⟦connected_space X; a ∈ topspace X; b ∈ topspace X⟧
⟹ connected_component_of X a b"
by (simp add: connected_space_iff_connected_component)
lemma connected_space_connected_component_set:
"connected_space X ⟷ (∀x ∈ topspace X. connected_component_of_set X x = topspace X)"
using connected_component_of_subset_topspace connected_space_iff_connected_component by fastforce
lemma connected_component_of_maximal:
"⟦connectedin X S; x ∈ S⟧ ⟹ S ⊆ connected_component_of_set X x"
by (meson Ball_Collect connected_component_of_def)
lemma connected_component_of_equiv:
"connected_component_of X x y ⟷
x ∈ topspace X ∧ y ∈ topspace X ∧ connected_component_of X x = connected_component_of X y"
apply (simp add: connected_component_in_topspace fun_eq_iff)
by (meson connected_component_of_refl connected_component_of_sym connected_component_of_trans)
lemma connected_component_of_disjoint:
"disjnt (connected_component_of_set X x) (connected_component_of_set X y)
⟷ ~(connected_component_of X x y)"
using connected_component_of_equiv unfolding disjnt_iff by force
lemma connected_component_of_eq:
"connected_component_of X x = connected_component_of X y ⟷
(x ∉ topspace X) ∧ (y ∉ topspace X) ∨
x ∈ topspace X ∧ y ∈ topspace X ∧
connected_component_of X x y"
by (metis Collect_empty_eq_bot connected_component_of_eq_empty connected_component_of_equiv)
lemma connectedin_connected_component_of:
"connectedin X (connected_component_of_set X x)"
proof -
have "connected_component_of_set X x = ⋃ {T. connectedin X T ∧ x ∈ T}"
by (auto simp: connected_component_of_def)
then show ?thesis
by (metis (no_types, lifting) InterI connectedin_Union emptyE mem_Collect_eq)
qed
lemma Union_connected_components_of:
"⋃(connected_components_of X) = topspace X"
unfolding connected_components_of_def
using connected_component_in_topspace connected_component_of_refl by fastforce
lemma connected_components_of_maximal:
"⟦C ∈ connected_components_of X; connectedin X S; ~disjnt C S⟧ ⟹ S ⊆ C"
unfolding connected_components_of_def disjnt_def
apply clarify
by (metis Int_emptyI connected_component_of_def connected_component_of_trans mem_Collect_eq)
lemma pairwise_disjoint_connected_components_of:
"pairwise disjnt (connected_components_of X)"
unfolding connected_components_of_def pairwise_def
by (smt (verit, best) connected_component_of_disjoint connected_component_of_eq imageE)
lemma complement_connected_components_of_Union:
"C ∈ connected_components_of X
⟹ topspace X - C = ⋃ (connected_components_of X - {C})"
by (metis Union_connected_components_of bot.extremum ccpo_Sup_singleton diff_Union_pairwise_disjoint
insert_subset pairwise_disjoint_connected_components_of)
lemma nonempty_connected_components_of:
"C ∈ connected_components_of X ⟹ C ≠ {}"
unfolding connected_components_of_def
by (metis (no_types, lifting) connected_component_of_eq_empty imageE)
lemma connected_components_of_subset:
"C ∈ connected_components_of X ⟹ C ⊆ topspace X"
using Union_connected_components_of by fastforce
lemma connectedin_connected_components_of:
assumes "C ∈ connected_components_of X"
shows "connectedin X C"
proof -
have "C ∈ connected_component_of_set X ` topspace X"
using assms connected_components_of_def by blast
then show ?thesis
using connectedin_connected_component_of by fastforce
qed
lemma connected_component_in_connected_components_of:
"connected_component_of_set X a ∈ connected_components_of X ⟷ a ∈ topspace X"
by (metis (no_types, lifting) connected_component_of_eq_empty connected_components_of_def image_iff)
lemma connected_space_iff_components_eq:
"connected_space X ⟷ (∀C ∈ connected_components_of X. ∀C' ∈ connected_components_of X. C = C')"
(is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
by (simp add: connected_components_of_def connected_space_connected_component_set)
show "?rhs ⟹ ?lhs"
by (metis Union_connected_components_of Union_iff connected_space_subconnected connectedin_connected_components_of)
qed
lemma connected_components_of_eq_empty:
"connected_components_of X = {} ⟷ X = trivial_topology"
by (simp add: connected_components_of_def)
lemma connected_components_of_empty_space:
"connected_components_of trivial_topology = {}"
by (simp add: connected_components_of_eq_empty)
lemma connected_components_of_subset_sing:
"connected_components_of X ⊆ {S} ⟷ connected_space X ∧ (X = trivial_topology ∨ topspace X = S)"
proof (cases "X = trivial_topology")
case True
then show ?thesis
by (simp add: connected_components_of_empty_space)
next
case False
then have "⟦connected_components_of X ⊆ {S}⟧ ⟹ topspace X = S"
using Union_connected_components_of connected_components_of_eq_empty by fastforce
with False show ?thesis
unfolding connected_components_of_def
by (metis connected_space_connected_component_set empty_iff image_subset_iff insert_iff)
qed
lemma connected_space_iff_components_subset_singleton:
"connected_space X ⟷ (∃a. connected_components_of X ⊆ {a})"
by (simp add: connected_components_of_subset_sing)
lemma connected_components_of_eq_singleton:
"connected_components_of X = {S} ⟷ connected_space X ∧ X ≠ trivial_topology ∧ S = topspace X"
by (metis connected_components_of_eq_empty connected_components_of_subset_sing insert_not_empty subset_singleton_iff)
lemma connected_components_of_connected_space:
"connected_space X ⟹ connected_components_of X = (if X = trivial_topology then {} else {topspace X})"
by (simp add: connected_components_of_eq_empty connected_components_of_eq_singleton)
lemma exists_connected_component_of_superset:
assumes "connectedin X S" and ne: "X ≠ trivial_topology"
shows "∃C. C ∈ connected_components_of X ∧ S ⊆ C"
proof (cases "S = {}")
case True
then show ?thesis
using ne connected_components_of_eq_empty by fastforce
next
case False
then show ?thesis
by (meson all_not_in_conv assms(1) connected_component_in_connected_components_of connected_component_of_maximal connectedin_subset_topspace in_mono)
qed
lemma closedin_connected_components_of:
assumes "C ∈ connected_components_of X"
shows "closedin X C"
proof -
obtain x where "x ∈ topspace X" and x: "C = connected_component_of_set X x"
using assms by (auto simp: connected_components_of_def)
have "connected_component_of_set X x ⊆ topspace X"
by (simp add: connected_component_of_subset_topspace)
moreover have "X closure_of connected_component_of_set X x ⊆ connected_component_of_set X x"
proof (rule connected_component_of_maximal)
show "connectedin X (X closure_of connected_component_of_set X x)"
by (simp add: connectedin_closure_of connectedin_connected_component_of)
show "x ∈ X closure_of connected_component_of_set X x"
by (simp add: ‹x ∈ topspace X› closure_of connected_component_of_refl)
qed
ultimately
show ?thesis
using closure_of_subset_eq x by auto
qed
lemma closedin_connected_component_of:
"closedin X (connected_component_of_set X x)"
by (metis closedin_connected_components_of closedin_empty connected_component_in_connected_components_of connected_component_of_eq_empty)
lemma connected_component_of_eq_overlap:
"connected_component_of_set X x = connected_component_of_set X y ⟷
(x ∉ topspace X) ∧ (y ∉ topspace X) ∨
~(connected_component_of_set X x ∩ connected_component_of_set X y = {})"
using connected_component_of_equiv by fastforce
lemma connected_component_of_nonoverlap:
"connected_component_of_set X x ∩ connected_component_of_set X y = {} ⟷
(x ∉ topspace X) ∨ (y ∉ topspace X) ∨
~(connected_component_of_set X x = connected_component_of_set X y)"
by (metis connected_component_of_eq_empty connected_component_of_eq_overlap inf.idem)
lemma connected_component_of_overlap:
"~(connected_component_of_set X x ∩ connected_component_of_set X y = {}) ⟷
x ∈ topspace X ∧ y ∈ topspace X ∧
connected_component_of_set X x = connected_component_of_set X y"
by (meson connected_component_of_nonoverlap)
subsection‹Combining theorems for continuous functions into the reals›
text ‹The homeomorphism between the real line and the open interval $(-1,1)$›
lemma continuous_map_real_shrink:
"continuous_map euclideanreal (top_of_set {-1<..<1}) (λx. x / (1 + ¦x¦))"
proof -
have "continuous_on UNIV (λx::real. x / (1 + ¦x¦))"
by (intro continuous_intros) auto
then show ?thesis
by (auto simp: continuous_map_in_subtopology divide_simps)
qed
lemma continuous_on_real_grow:
"continuous_on {-1<..<1} (λx::real. x / (1 - ¦x¦))"
by (intro continuous_intros) auto
lemma real_grow_shrink:
fixes x::real
shows "x / (1 + ¦x¦) / (1 - ¦x / (1 + ¦x¦)¦) = x"
by (force simp: divide_simps)
lemma homeomorphic_maps_real_shrink:
"homeomorphic_maps euclideanreal (subtopology euclideanreal {-1<..<1})
(λx. x / (1 + ¦x¦)) (λy. y / (1 - ¦y¦))"
by (force simp: homeomorphic_maps_def continuous_map_real_shrink continuous_on_real_grow divide_simps)
lemma real_shrink_Galois:
fixes x::real
shows "(x / (1 + ¦x¦) = y) ⟷ (¦y¦ < 1 ∧ y / (1 - ¦y¦) = x)"
using real_grow_shrink by (fastforce simp add: distrib_left)
lemma real_shrink_eq:
fixes x y::real
shows "(x / (1 + ¦x¦) = y / (1 + ¦y¦)) ⟷ x = y"
by (metis real_shrink_Galois)
lemma real_shrink_lt:
fixes x::real
shows "x / (1 + ¦x¦) < y / (1 + ¦y¦) ⟷ x < y"
using zero_less_mult_iff [of x y] by (auto simp: field_simps abs_if not_less)
lemma real_shrink_le:
fixes x::real
shows "x / (1 + ¦x¦) ≤ y / (1 + ¦y¦) ⟷ x ≤ y"
by (meson linorder_not_le real_shrink_lt)
lemma real_shrink_grow:
fixes x::real
shows "¦x¦ < 1 ⟹ x / (1 - ¦x¦) / (1 + ¦x / (1 - ¦x¦)¦) = x"
using real_shrink_Galois by blast
lemma continuous_shrink:
"continuous_on UNIV (λx::real. x / (1 + ¦x¦))"
by (intro continuous_intros) auto
lemma strict_mono_shrink:
"strict_mono (λx::real. x / (1 + ¦x¦))"
by (simp add: monotoneI real_shrink_lt)
lemma shrink_range: "(λx::real. x / (1 + ¦x¦)) ` S ⊆ {-1<..<1}"
by (auto simp: divide_simps)
text ‹Note: connected sets of real numbers are the same thing as intervals›
lemma connected_shrink:
fixes S :: "real set"
shows "connected ((λx. x / (1 + ¦x¦)) ` S) ⟷ connected S" (is "?lhs = ?rhs")
proof
assume "?lhs"
then have "connected ((λx. x / (1 - ¦x¦)) ` (λx. x / (1 + ¦x¦)) ` S)"
by (metis continuous_on_real_grow shrink_range connected_continuous_image
continuous_on_subset)
then show "?rhs"
using real_grow_shrink by (force simp add: image_comp)
next
assume ?rhs
then show ?lhs
using connected_continuous_image
by (metis continuous_on_subset continuous_shrink subset_UNIV)
qed
subsection ‹A few cardinality results›
lemma eqpoll_real_subset:
fixes a b::real
assumes "a < b" and S: "⋀x. ⟦a < x; x < b⟧ ⟹ x ∈ S"
shows "S ≈ (UNIV::real set)"
proof (rule lepoll_antisym)
show "S ≲ (UNIV::real set)"
by (simp add: subset_imp_lepoll)
define f where "f ≡ λx. (a+b) / 2 + (b-a) / 2 * (x / (1 + ¦x¦))"
show "(UNIV::real set) ≲ S"
unfolding lepoll_def
proof (intro exI conjI)
show "inj f"
unfolding inj_on_def f_def
by (smt (verit, ccfv_SIG) real_shrink_eq ‹a<b› divide_eq_0_iff mult_cancel_left times_divide_eq_right)
have pos: "(b-a) / 2 > 0"
using ‹a<b› by auto
have *: "a < (a + b) / 2 + (b - a) / 2 * x ⟷ (b - a) > (b - a) * -x"
"(a + b) / 2 + (b - a) / 2 * x < b ⟷ (b - a) * x < (b - a)" for x
by (auto simp: field_simps)
show "range f ⊆ S"
using shrink_range [of UNIV] ‹a < b›
unfolding subset_iff f_def greaterThanLessThan_iff image_iff
by (smt (verit, best) S * mult_less_cancel_left2 mult_minus_right)
qed
qed
lemma reals01_lepoll_nat_sets: "{0..<1::real} ≲ (UNIV::nat set set)"
proof -
define nxt where "nxt ≡ λx::real. if x < 1/2 then (True, 2*x) else (False, 2*x - 1)"
have nxt_fun: "nxt ∈ {0..<1} → UNIV × {0..<1}"
by (simp add: nxt_def Pi_iff)
define σ where "σ ≡ λx. rec_nat (True, x) (λn (b,y). nxt y)"
have σSuc [simp]: "σ x (Suc k) = nxt (snd (σ x k))" for k x
by (simp add: σ_def case_prod_beta')
have σ01: "x ∈ {0..<1} ⟹ σ x n ∈ UNIV × {0..<1}" for x n
proof (induction n)
case 0
then show ?case
by (simp add: σ_def)
next
case (Suc n)
with nxt_fun show ?case
by (force simp add: Pi_iff split: prod.split)
qed
define f where "f ≡ λx. {n. fst (σ x (Suc n))}"
have snd_nxt: "snd (nxt y) - snd (nxt x) = 2 * (y-x)"
if "fst (nxt x) = fst (nxt y)" for x y
using that by (simp add: nxt_def split: if_split_asm)
have False if "f x = f y" "x < y" "0 ≤ x" "x < 1" "0 ≤ y" "y < 1" for x y :: real
proof -
have "⋀k. fst (σ x (Suc k)) = fst (σ y (Suc k))"
using that by (force simp add: f_def)
then have eq: "⋀k. fst (nxt (snd (σ x k))) = fst (nxt (snd (σ y k)))"
by (metis σ_def case_prod_beta' rec_nat_Suc_imp)
have *: "snd (σ y k) - snd (σ x k) = 2 ^ k * (y-x)" for k
proof (induction k)
case 0
then show ?case
by (simp add: σ_def)
next
case (Suc k)
then show ?case
by (simp add: eq snd_nxt)
qed
define n where "n ≡ nat (⌈log 2 (1 / (y - x))⌉)"
have "2^n ≥ 1 / (y - x)"
by (simp add: n_def power_of_nat_log_ge)
then have "2^n * (y-x) ≥ 1"
using ‹x < y› by (simp add: n_def field_simps)
with * have "snd (σ y n) - snd (σ x n) ≥ 1"
by presburger
moreover have "snd (σ x n) ∈ {0..<1}" "snd (σ y n) ∈ {0..<1}"
using that by (meson σ01 atLeastLessThan_iff mem_Times_iff)+
ultimately show False by simp
qed
then have "inj_on f {0..<1}"
by (meson atLeastLessThan_iff linorder_inj_onI')
then show ?thesis
unfolding lepoll_def by blast
qed
lemma nat_sets_lepoll_reals01: "(UNIV::nat set set) ≲ {0..<1::real}"
proof -
define F where "F ≡ λS i. if i∈S then (inverse 3::real) ^ i else 0"
have Fge0: "F S i ≥ 0" for S i
by (simp add: F_def)
have F: "summable (F S)" for S
unfolding F_def by (force intro: summable_comparison_test_ev [where g = "power (inverse 3)"])
have "sum (F S) {..<n} ≤ 3/2" for n S
proof (cases n)
case (Suc n')
have "sum (F S) {..<n} ≤ (∑i<n. inverse 3 ^ i)"
by (simp add: F_def sum_mono)
also have "… = (∑i=0..n'. inverse 3 ^ i)"
using Suc atLeast0AtMost lessThan_Suc_atMost by presburger
also have "… = (3/2) * (1 - inverse 3 ^ n)"
using sum_gp_multiplied [of 0 n' "inverse (3::real)"] by (simp add: Suc field_simps)
also have "… ≤ 3/2"
by (simp add: field_simps)
finally show ?thesis .
qed auto
then have F32: "suminf (F S) ≤ 3/2" for S
using F suminf_le_const by blast
define f where "f ≡ λS. suminf (F S) / 2"
have monoF: "F S n ≤ F T n" if "S ⊆ T" for S T n
using F_def that by auto
then have monof: "f S ≤ f T" if "S ⊆ T" for S T
using that F by (simp add: f_def suminf_le)
have "f S ∈ {0..<1::real}" for S
proof -
have "0 ≤ suminf (F S)"
using F by (simp add: F_def suminf_nonneg)
with F32[of S] show ?thesis
by (auto simp: f_def)
qed
moreover have "inj f"
proof
fix S T
assume "f S = f T"
show "S = T"
proof (rule ccontr)
assume "S ≠ T"
then have ST_ne: "(S-T) ∪ (T-S) ≠ {}"
by blast
define n where "n ≡ LEAST n. n ∈ (S-T) ∪ (T-S)"
have sum_split: "suminf (F U) = sum (F U) {..<Suc n} + (∑k. F U (k + Suc n))" for U
by (metis F add.commute suminf_split_initial_segment)
have yes: "f U ≥ (sum (F U) {..<n} + (inverse 3::real) ^ n) / 2"
if "n ∈ U" for U
proof -
have "0 ≤ (∑k. F U (k + Suc n))"
by (metis F Fge0 suminf_nonneg summable_iff_shift)
moreover have "F U n = (1/3) ^ n"
by (simp add: F_def that)
ultimately show ?thesis
by (simp add: sum_split f_def)
qed
have *: "(∑k. F UNIV (k + n)) = (∑k. F UNIV k) * (inverse 3::real) ^ n" for n
by (simp add: F_def power_add suminf_mult2)
have no: "f U < (sum (F U) {..<n} + (inverse 3::real) ^ n) / 2"
if "n ∉ U" for U
proof -
have [simp]: "F U n = 0"
by (simp add: F_def that)
have "(∑k. F U (k + Suc n)) ≤ (∑k. F UNIV (k + Suc n))"
by (metis F monoF subset_UNIV suminf_le summable_ignore_initial_segment)
then have "suminf (F U) ≤ (∑k. F UNIV (k + Suc n)) + (∑i<n. F U i)"
by (simp add: sum_split)
also have "… < (inverse 3::real) ^ n + (∑i<n. F U i)"
unfolding * using F32[of UNIV] by simp
finally have "suminf (F U) < inverse 3 ^ n + sum (F U) {..<n}" .
then show ?thesis
by (simp add: f_def)
qed
have "S ∩ {..<n} = T ∩ {..<n}"
using not_less_Least by (fastforce simp add: n_def)
then have "sum (F S) {..<n} = sum (F T) {..<n}"
by (metis (no_types, lifting) F_def Int_iff sum.cong)
moreover consider "n ∈ S-T" | "n ∈ T-S"
by (metis LeastI_ex ST_ne UnE ex_in_conv n_def)
ultimately show False
by (smt (verit, best) Diff_iff ‹f S = f T› yes no)
qed
qed
ultimately show ?thesis
by (meson image_subsetI lepoll_def)
qed
lemma open_interval_eqpoll_reals:
fixes a b::real
shows "{a<..<b} ≈ (UNIV::real set) ⟷ a<b"
using bij_betw_tan bij_betw_open_intervals eqpoll_def
by (smt (verit, best) UNIV_I eqpoll_real_subset eqpoll_iff_bijections greaterThanLessThan_iff)
lemma closed_interval_eqpoll_reals:
fixes a b::real
shows "{a..b} ≈ (UNIV::real set) ⟷ a < b"
proof
show "{a..b} ≈ (UNIV::real set) ⟹ a < b"
using eqpoll_finite_iff infinite_Icc_iff infinite_UNIV_char_0 by blast
qed (auto simp: eqpoll_real_subset)
lemma reals_lepoll_reals01: "(UNIV::real set) ≲ {0..<1::real}"
proof -
have "(UNIV::real set) ≈ {0<..<1::real}"
by (simp add: open_interval_eqpoll_reals eqpoll_sym)
also have "… ≲ {0..<1::real}"
by (simp add: greaterThanLessThan_subseteq_atLeastLessThan_iff subset_imp_lepoll)
finally show ?thesis .
qed
lemma nat_sets_eqpoll_reals: "(UNIV::nat set set) ≈ (UNIV::real set)"
by (metis (mono_tags, opaque_lifting) reals_lepoll_reals01 lepoll_antisym lepoll_trans
nat_sets_lepoll_reals01 reals01_lepoll_nat_sets subset_UNIV subset_imp_lepoll)
end