Theory Uniform_Structure
section ‹Uniform spaces›
theory Uniform_Structure
imports "HOL-Analysis.Abstract_Topology" "HOL-Analysis.Abstract_Metric_Spaces"
begin
paragraph ‹Summary›
text ‹
This section introduces a set-based notion of uniformities and connects it to the
@{class "uniform_space"} type class.
›
subsection ‹Definitions and basic results›
definition uniformity_on :: "'a set ⇒ (('a × 'a) set ⇒ bool) ⇒ bool" where
"uniformity_on X ℰ ⟷
(∃E. ℰ E) ∧
(∀E. ℰ E ⟶ E ⊆ X × X ∧ Id_on X ⊆ E ∧ ℰ (E¯) ∧ (∃F. ℰ F ∧ F O F ⊆ E) ∧
(∀F. E ⊆ F ∧ F ⊆ X × X ⟶ ℰ F)) ∧
(∀E F. ℰ E ⟶ ℰ F ⟶ ℰ (E ∩ F))"
typedef 'a uniformity = "{(X :: 'a set, ℰ). uniformity_on X ℰ}"
morphisms uniformity_rep uniformity
proof -
have "uniformity_on UNIV (λE. E = UNIV × UNIV)"
unfolding uniformity_on_def Id_on_def relcomp_def by auto
then show ?thesis by fast
qed
definition uspace :: "'a uniformity ⇒ 'a set" where
"uspace Φ = (let (X, ℰ) = uniformity_rep Φ in X)"
definition entourage_in :: "'a uniformity ⇒ ('a × 'a) set ⇒ bool" where
"entourage_in Φ = (let (X, ℰ) = uniformity_rep Φ in ℰ)"
lemma uniformity_inverse'[simp]:
assumes "uniformity_on X ℰ"
shows "uspace (uniformity (X, ℰ)) = X ∧ entourage_in (uniformity (X, ℰ)) = ℰ"
proof -
from assms have "uniformity_rep (uniformity (X, ℰ)) = (X, ℰ)"
using uniformity_inverse by blast
then show ?thesis by (auto simp: prod.splits uspace_def entourage_in_def)
qed
lemma uniformity_entourages:
shows "uniformity_on (uspace Φ) (entourage_in Φ)"
by (metis Product_Type.Collect_case_prodD entourage_in_def split_beta uspace_def uniformity_rep)
lemma entourages_exist: "∃E. entourage_in Φ E"
using uniformity_entourages unfolding uniformity_on_def by blast
lemma entourage_in_space[elim]: "entourage_in Φ E ⟹ E ⊆ uspace Φ × uspace Φ"
using uniformity_entourages unfolding uniformity_on_def by metis
lemma entourage_superset[intro]:
"entourage_in Φ E ⟹ E ⊆ F ⟹ F ⊆ uspace Φ × uspace Φ ⟹ entourage_in Φ F"
using uniformity_entourages unfolding uniformity_on_def by blast
lemma entourage_intersection[intro]: "entourage_in Φ E ⟹ entourage_in Φ F ⟹ entourage_in Φ (E ∩ F)"
using uniformity_entourages unfolding uniformity_on_def by metis
lemma entourage_converse[intro]: "entourage_in Φ E ⟹ entourage_in Φ (E¯)"
using uniformity_entourages unfolding uniformity_on_def by fast
lemma entourage_diagonal[dest]:
assumes entourage: "entourage_in Φ E" and in_space: "x ∈ uspace Φ"
shows "(x,x) ∈ E"
proof -
have "Id_on (uspace Φ) ⊆ E"
using uniformity_entourages entourage unfolding uniformity_on_def by fast
then show ?thesis using Id_onI[OF in_space] by blast
qed
lemma smaller_entourage:
assumes entourage: "entourage_in Φ E"
shows "∃F. entourage_in Φ F ∧ (∀x y z. (x,y) ∈ F ∧ (y,z) ∈ F ⟶ (x,z) ∈ E)"
proof -
from entourage obtain F where "entourage_in Φ F ∧ F O F ⊆ E"
using uniformity_entourages entourage unfolding uniformity_on_def by meson
moreover from this have "(x,z) ∈ E" if "(x,y) ∈ F ∧ (y,z) ∈ F" for x y z using that by blast
ultimately show ?thesis by blast
qed
lemma entire_space_entourage: "entourage_in Φ (uspace Φ × uspace Φ)"
by (metis entourages_exist entourage_in_space entourage_superset subset_refl)
definition utopology :: "'a uniformity ⇒ 'a topology" where
"utopology Φ = topology (λU. U ⊆ uspace Φ ∧ (∀x∈U. ∃E. entourage_in Φ E ∧ E``{x} ⊆ U))"
lemma openin_utopology [iff]:
fixes Φ :: "'a uniformity"
defines "uopen U ≡ U ⊆ uspace Φ ∧ (∀x∈U. ∃E. entourage_in Φ E ∧ E``{x} ⊆ U)"
shows "openin (utopology Φ) = uopen"
proof -
have "uopen (U ∩ V)" if hUV: "uopen U ∧ uopen V" for U V
proof -
have "∃E. entourage_in Φ E ∧ E``{x} ⊆ U ∩ V" if hx: "x ∈ U ∩ V" for x
proof -
from hUV hx obtain E⇩1 E⇩2 where
"entourage_in Φ E⇩1 ∧ entourage_in Φ E⇩2 ∧ E⇩1``{x} ⊆ U ∧ E⇩2``{x} ⊆ V" unfolding uopen_def by blast
then have "entourage_in Φ (E⇩1 ∩ E⇩2) ∧ (E⇩1 ∩ E⇩2)``{x} ⊆ U ∩ V" by blast
then show ?thesis by fast
qed
then show ?thesis using le_infI1 hUV unfolding uopen_def by auto
qed
moreover have "uopen (⋃𝒰)" if h𝒰: "∀U∈𝒰. uopen U" for 𝒰
proof -
have "∃E. entourage_in Φ E ∧ E``{x} ⊆ ⋃𝒰" if hx: "x ∈ ⋃𝒰" for x
proof -
from hx obtain U where hU: "U ∈ 𝒰 ∧ x ∈ U" by blast
from this h𝒰 obtain E where "entourage_in Φ E ∧ E``{x} ⊆ U" unfolding uopen_def by fast
moreover from this hU have "E``{x} ⊆ ⋃𝒰" by fast
ultimately show ?thesis by blast
qed
then show ?thesis using Union_least h𝒰 unfolding uopen_def by auto
qed
ultimately have "istopology uopen" unfolding istopology_def by presburger
from topology_inverse'[OF this] show ?thesis unfolding utopology_def uopen_def by blast
qed
lemma topspace_utopology[simp]:
shows "topspace (utopology Φ) = uspace Φ"
proof -
let ?T = "utopology Φ"
have "topspace ?T ⊆ uspace Φ"
using openin_topspace openin_utopology by meson
moreover have "openin ?T (uspace Φ)"
unfolding openin_utopology by (auto intro: entire_space_entourage)
ultimately show ?thesis using topspace_def by fast
qed
definition ucontinuous :: "'a uniformity ⇒ 'b uniformity ⇒ ('a ⇒ 'b) ⇒ bool" where
"ucontinuous Φ Ψ f ⟷
f ∈ uspace Φ → uspace Ψ ∧
(∀E. entourage_in Ψ E ⟶ entourage_in Φ {(x, y) ∈ uspace Φ × uspace Φ. (f x, f y) ∈ E})"
lemma ucontinuous_image_subset [dest]: "ucontinuous Φ Ψ f ⟹ f`(uspace Φ) ⊆ uspace Ψ"
unfolding ucontinuous_def by blast
lemma entourage_preimage_ucontinuous [dest]:
assumes "ucontinuous Φ Ψ f" and "entourage_in Ψ E"
shows "entourage_in Φ {(x, y) ∈ uspace Φ × uspace Φ. (f x, f y) ∈ E}"
using assms unfolding ucontinuous_def by blast
lemma ucontinuous_imp_continuous:
assumes "ucontinuous Φ Ψ f"
shows "continuous_map (utopology Φ) (utopology Ψ) f"
proof (unfold continuous_map_def, intro conjI allI impI)
show "f ∈ topspace (utopology Φ) → topspace (utopology Ψ)"
using assms unfolding ucontinuous_def by auto
next
fix U assume hU: "openin (utopology Ψ) U"
let ?V = "{x ∈ topspace (utopology Φ). f x ∈ U}"
have "∃F. entourage_in Φ F ∧ F``{x} ⊆ ?V" if hx: "x ∈ uspace Φ ∧ f x ∈ U" for x
proof -
from that hU obtain E where hE: "entourage_in Ψ E ∧ E``{f x} ⊆ U"
unfolding openin_utopology by blast
let ?F = "{(x, y) ∈ uspace Φ × uspace Φ. (f x, f y) ∈ E}"
have "?F``{x} = {y ∈ uspace Φ. f y ∈ E``{f x}}" unfolding Image_def using hx by auto
then have "?F``{x} ⊆ ?V" using hE by auto
moreover have "entourage_in Φ ?F"
using assms entourage_preimage_ucontinuous hE unfolding topspace_utopology by blast
ultimately show ?thesis by blast
qed
then show "openin (utopology Φ) ?V" unfolding openin_utopology by force
qed
subsection ‹Metric spaces as uniform spaces›
context Metric_space
begin
abbreviation mentourage :: "real ⇒ ('a × 'a) set" where
"mentourage ε ≡ {(x,y) ∈ M × M. d x y < ε}"
definition muniformity :: "'a uniformity" where
"muniformity = uniformity (M, λE. E ⊆ M × M ∧ (∃ε > 0. mentourage ε ⊆ E))"
lemma
uspace_muniformity[simp]: "uspace muniformity = M" and
entourage_muniformity: "entourage_in muniformity = (λE. E ⊆ M × M ∧ (∃ε > 0. mentourage ε ⊆ E))"
proof -
have "uniformity_on M (λE. E ⊆ M × M ∧ (∃ε > 0. mentourage ε ⊆ E))"
unfolding uniformity_on_def Id_on_def converse_def
proof (intro conjI allI impI, goal_cases)
case 1
then show ?case by (rule exI[of _ "mentourage 1"]) force
next
case (5 E)
then obtain ε where hε: "ε > 0 ∧ mentourage ε ⊆ E" by blast
then have "{(y, x). (x, y) ∈ mentourage ε} ⊆ E" using commute by auto
then have "mentourage ε ⊆ E¯" by blast
then show ?case using hε by auto
next
case (6 E)
then obtain ε where hε: "ε > 0 ∧ mentourage ε ⊆ E" by blast
let ?F = "mentourage (ε/2)"
have "(x,z) ∈ E" if "(x,y) ∈ ?F ∧ (y,z) ∈ ?F" for x y z
proof -
have "d x z < ε" using that triangle by fastforce
then show ?thesis using that hε by blast
qed
then have "?F ⊆ M × M ∧ ?F O ?F ⊆ E" by blast
then show ?case by (meson hε order_refl zero_less_divide_iff zero_less_numeral)
next
case (8 E F)
then show ?case by fast
next
case (10 E F)
then obtain ε δ where
"ε > 0 ∧ mentourage ε ⊆ E" and
"δ > 0 ∧ mentourage δ ⊆ F" by presburger
then have "min ε δ > 0 ∧ mentourage (min ε δ) ⊆ E ∩ F" by auto
then show ?case by blast
qed (auto)
then show
"uspace muniformity = M" and
"entourage_in muniformity = (λE. E ⊆ M × M ∧ (∃ε > 0. mentourage ε ⊆ E))"
unfolding muniformity_def using uniformity_inverse' by auto
qed
lemma uniformity_induces_mtopology [simp]: "utopology muniformity = mtopology"
proof -
have mentourage_image: "mball x ε = (mentourage ε)``{x}" for x ε unfolding mball_def by auto
have "openin (utopology muniformity) U ⟷ openin mtopology U" for U
proof
assume hU: "openin (utopology muniformity) U"
have "∃ε > 0. mball x ε ⊆ U" if "x ∈ U" for x
proof -
from hU that obtain E where hE: "entourage_in muniformity E ∧ E``{x} ⊆ U" unfolding openin_utopology by blast
then obtain ε where hε: "ε > 0 ∧ mentourage ε ⊆ E" unfolding entourage_muniformity by presburger
then have "(mentourage ε)``{x} ⊆ U" using hE by fast
then show ?thesis using mentourage_image hε by auto
qed
then show "openin mtopology U" unfolding openin_mtopology using hU openin_subset by fastforce
next
assume hU: "openin mtopology U"
have "∃E. entourage_in muniformity E ∧ E``{x} ⊆ U" if "x ∈ U" for x
proof -
from hU that obtain ε where "ε > 0 ∧ mball x ε ⊆ U" unfolding openin_mtopology by blast
then show ?thesis unfolding mentourage_image entourage_muniformity by auto
qed
then show "openin (utopology muniformity) U" unfolding openin_utopology using hU openin_subset by fastforce
qed
then show ?thesis using topology_eq by blast
qed
subsection ‹Connection to type class›
end
text ‹The following connects the @{class "uniform_space"} class to the set based notion
@{term "uniformity_on"}.
Given a type @{typ "'a"} which is an instance of the class @{class "uniform_space"}, it is possible
to introduce an @{typ "'a uniformity"} on the entire universe: @{term "UNIV"}:›
definition uniformity_of_space :: "('a :: uniform_space) uniformity" where
"uniformity_of_space = uniformity (UNIV :: 'a set, (λS. ∀⇩F x in uniformity_class.uniformity. x∈S))"
text ‹The induced uniformity fulfills the required conditions, i.e., the class based notion implies
the set-based notion.›
lemma uniformity_on_uniformity_of_space_aux:
"uniformity_on (UNIV :: ('a :: uniform_space) set) (λS. ∀⇩F x in uniformity_class.uniformity. x∈S)"
proof -
let ?u = " uniformity_class.uniformity :: ('a × 'a) filter"
have "∃S. (∀⇩F x in ?u.x ∈ S)" by (intro exI[where x="UNIV × UNIV"]) simp
moreover have "(∀⇩F x in ?u.x ∈ E ∩ F)" if "(∀⇩F x in ?u.x ∈ E)" "(∀⇩F x in ?u.x ∈ F)" for E F
using that eventually_conj by auto
moreover have "Id_on UNIV ⊆ E" if "∀⇩F x in ?u. x ∈ E" for E
proof -
have "(x,x) ∈ E" for x using uniformity_refl[OF that] by auto
thus ?thesis unfolding Id_on_def by auto
qed
moreover have "(∀⇩F x in ?u. x ∈ E¯)" if "∀⇩F x in ?u. x ∈ E" for E
using uniformity_sym[OF that] by (simp add: converse_unfold)
moreover have "∃F. (∀⇩F x in ?u. x ∈ F) ∧ F O F ⊆ E" if "∀⇩F x in ?u. x ∈ E" for E
proof -
from uniformity_trans[OF that]
obtain D where "eventually D ?u" "(∀x y z. D (x, y) ⟶ D (y, z) ⟶ (x, z) ∈ E)" by auto
thus ?thesis by (intro exI[where x="Collect D"]) auto
qed
moreover have "∀⇩F x in ?u. x ∈ F" if "∀⇩F x in ?u. x ∈ E" "E ⊆ F" for E F
using that(2) by (intro eventually_mono[OF that(1)]) auto
ultimately show ?thesis
unfolding uniformity_on_def by auto
qed
lemma uniformity_rep_uniformity_of_space:
"uniformity_rep uniformity_of_space = (UNIV, (λS. ∀⇩F x in uniformity_class.uniformity. x ∈ S))"
unfolding uniformity_of_space_def using uniformity_on_uniformity_of_space_aux
by (intro uniformity_inverse) auto
lemma uspace_uniformity_space [simp, iff]:
"uspace uniformity_of_space = UNIV"
unfolding uspace_def uniformity_rep_uniformity_of_space by simp
lemma entourage_in_uniformity_space:
"entourage_in uniformity_of_space S =(∀⇩F x in uniformity_class.uniformity. x ∈ S)"
unfolding entourage_in_def uniformity_rep_uniformity_of_space by simp
text ‹Compatibility of the @{term "Metric_space.muniformity"} with the uniformity based on
the class based hierarchy.›
lemma "(uniformity_of_space :: ('a :: metric_space) uniformity) = Met_TC.muniformity"
proof -
have "(∀x y. dist x y < ε ⟶ (x, y) ∈ E) = ({(x, y). dist x y < ε} ⊆ E)"
for ε and E :: "('a × 'a) set"
by auto
thus ?thesis
unfolding Met_TC.muniformity_def uniformity_of_space_def eventually_uniformity_metric by simp
qed
end