SSL Stone_Cech.thy

(*
  Author: Mike Stannett (m.stannett@sheffield.ac.uk)
  Maintainer: Mike Stannett (m.stannett@sheffield.ac.uk)
  Title:  Stone_Cech.thy
  Date:   May 2024
  Topic:  The Stone-Cech Compactification (Part 1. Definitions and Extension Property)
*)

(* The Stone-{\v{C}}ech Compactification} *)

text ‹
 Building on parts of HOL-Analysis, we provide mathematical components for work on the
 Stone-{\v{C}}ech compactification. The main concepts covered are: $C^*$-embedding, weak topologies
 and compactification, focusing in particular on the Stone-{\v{C}}ech compactification of an
 arbitrary Tychonov space $X$. Many of the proofs given here derive from those of Willard
 (\textit{General Topology}, 1970, Addison-Wesley) and Walker (\textit{The Stone-{\v C}ech
 Compactification}, 1974, Springer-Verlag).

 Using traditional topological proof strategies we define the evaluation and
 projection functions for product spaces, and show that product spaces carry the weak
 topology induced by their projections whenever those projections separate points both
 from each other and from closed sets.

 In particular, we show that the evaluation map from
 an arbitrary Tychonov space $X$ into $\beta{X}$ is a dense $C^*$-embedding, and then verify the
 Stone-{\v C}ech Extension Property: any continuous map from $X$ to a compact Hausdorff space $K$
 extends
 uniquely to a continuous map from $\beta{X}$ to $K$.

 \vspace{24pt}

 ›

theory Stone_Cech
  imports "HOL.Topological_Spaces" 
          "HOL.Set" 
          "HOL-Analysis.Urysohn"

begin

text ‹
 Concrete definitions of finite intersections and arbitrary unions, and their
 relationship to the Analysis.Abstract\_Topology versions.
 ›

definition finite_intersections_of :: "'a set set ==> 'a set set"
  where "finite_intersections_of S = { (∩ F) | F . F ⊆ S ∧ finite' F }"

definition arbitrary_unions_of :: "'a set set ==> 'a set set"
  where "arbitrary_unions_of S = { (∪ F) | F . F ⊆ S }"

lemma generator_imp_arbitrary_union:
  shows "S ⊆ arbitrary_unions_of S"
  unfolding arbitrary_unions_of_def by blast

lemma finite_intersections_container:
  shows "∀ s ∈ finite_intersections_of S . ∪S ∩ s = s"
  unfolding finite_intersections_of_def by blast

lemma generator_imp_finite_intersection:
  shows "S ⊆ finite_intersections_of S"
  unfolding finite_intersections_of_def by blast

lemma finite_intersections_equiv:
  shows "(finite' intersection_of (λx. x ∈ S)) U ⟷ U ∈ finite_intersections_of S"
  unfolding finite_intersections_of_def intersection_of_def
  by auto

lemma arbitrary_unions_equiv:
  shows "(arbitrary union_of (λ x . x ∈ S)) U ⟷ U ∈ arbitrary_unions_of S"
  unfolding arbitrary_unions_of_def union_of_def arbitrary_def
  by auto


text ‹
 Supplementary information about topological bases and the topologies they generate
 ›

definition base_generated_on_by :: "'a set ==> 'a set set ==> 'a set set"
  where "base_generated_on_by X S = { X ∩ s | s . s ∈ finite_intersections_of S}"

definition opens_generated_on_by :: "'a set ==> 'a set set ==> 'a set set"
  where "opens_generated_on_by X S = arbitrary_unions_of (base_generated_on_by X S)"

definition base_generated_by :: "'a set set ==> 'a set set"
  where "base_generated_by S = finite_intersections_of S"

definition opens_generated_by :: "'a set set ==> 'a set set"
  where "opens_generated_by S = arbitrary_unions_of (base_generated_by S)"

lemma generators_are_basic:
  shows "S ⊆ base_generated_by S"
  unfolding base_generated_by_def finite_intersections_of_def
  by blast

lemma basics_are_open:
  shows "base_generated_by S ⊆ opens_generated_by S"
  unfolding opens_generated_by_def arbitrary_unions_of_def
  by blast

lemma generators_are_open:
  shows   "S ⊆ opens_generated_by S"
  using generators_are_basic basics_are_open 
  by blast

lemma generated_topspace:
  assumes "T = topology_generated_by S"
  shows "topspace T = ∪S" 
  using assms by simp

lemma base_generated_by_alt:
  shows "base_generated_by S = base_generated_on_by (∪S) S"
  unfolding base_generated_by_def base_generated_on_by_def
  using finite_intersections_container[of S]
  by auto

lemma opens_generated_by_alt:
  shows "opens_generated_by S = arbitrary_unions_of (finite_intersections_of S)"
  unfolding opens_generated_by_def base_generated_by_def
  by simp

lemma opens_generated_unfolded:
  shows "opens_generated_by S = {∪ A | A . A ⊆ { ∩ B | B . finite' B ∧ B ⊆ S}}"
  apply (simp add: opens_generated_by_alt)
  unfolding finite_intersections_of_def arbitrary_unions_of_def
  by blast

lemma opens_eq_generated_topology:
  shows   "openin (topology_generated_by S) U ⟷ U ∈ opens_generated_by S"
proof -
  have "openin (topology_generated_by S) = arbitrary union_of finite' intersection_of (λx. x ∈ S)"
    by (metis generate_topology_on_eq istopology_generate_topology_on topology_inverse')
  also have "… = arbitrary union_of (λ U . U ∈ finite_intersections_of S)"
    using finite_intersections_equiv[of S] by presburger
  also have "… = (λ U . U ∈ arbitrary_unions_of (finite_intersections_of S))"
    using arbitrary_unions_equiv[of "finite_intersections_of S"] by presburger
  finally show ?thesis 
    using opens_generated_by_alt by auto
qed


section ‹
 $C^*$-embedding
 ›

abbreviation continuous_from_to 
    :: "'a topology ==> 'b topology ==> ('a ==> 'b) set" (‹cts[ _, _]›) 
  where "continuous_from_to X Y ≡ { f . continuous_map X Y f }"

abbreviation continuous_from_to_extensional 
     :: "'a topology ==> 'b topology ==> ('a ==> 'b) set" (‹cts_E[ _, _ ]›)
  where "continuous_from_to_extensional X Y ≡ (topspace X →_E topspace Y) ∩ cts[X,Y]"

(* Sets of continuous functions from a space X to any common space satisfying condition P *)
abbreviation continuous_maps_from_to_shared_where ::
    "'a topology ==> ('b topology ==> bool) ==> ('a ==> 'b) set ==> bool" (‹cts'_on _ to'_shared _›)
  where "continuous_maps_from_to_shared_where X P
            ≡ (λ fs . (∃ Y . P Y ∧ fs ⊆ cts[X,Y]))"

(* dense embeddings *)
definition dense_in :: "'a topology ==> 'a set ==> 'a set ==> bool"
  where "dense_in T A B ≡ T closure_of A = B"

lemma dense_in_closure:
  assumes "dense_in T A B"
  shows   "dense_in (subtopology T B) A B"
  by (metis Int_UNIV_right Int_absorb Int_commute assms closure_of_UNIV closure_of_restrict 
            closure_of_subtopology dense_in_def topspace_subtopology)
abbreviation dense_embedding :: "'a topology ==> 'b topology ==> ('a ==> 'b) ==> bool"
  where "dense_embedding small big f ≡ (embedding_map small big f)
                                         ∧ dense_in big (f`topspace small) (topspace big)"

lemma continuous_maps_on_dense_subset:
  assumes "(cts_on X to_shared Hausdorff_space) {f,g}"
and       "dense_in X D (topspace X)"
and       "∀ x ∈ D . f x = g x"
shows     "∀ x ∈ topspace X . f x = g x"
proof -
  obtain Y where "continuous_map X Y f ∧ continuous_map X Y g ∧ Hausdorff_space Y"
    using assms(1) by auto
  thus ?thesis using assms dense_in_def forall_in_closure_of_eq by fastforce
qed

lemma continuous_map_on_dense_embedding:
  assumes "(cts_on X to_shared Hausdorff_space) {f,g}"
and       "dense_embedding D X e"
and       "∀ d ∈ topspace D . (f o e) d = (g o e) d"
shows     "∀ x ∈ topspace X . f x = g x"
  using assms continuous_maps_on_dense_subset[of f g X "e ` topspace D"]
  unfolding dense_in_def by fastforce


(* closure of range *)
definition range' :: "'a topology ==> ('a ==> real) ==> real set"
  where "range' X f = euclideanreal closure_of (f ` topspace X)"

(* functions defining boundedness  of a C(X) function on its domain *)
abbreviation fbounded_below :: "('a ==> real) ==> 'a topology ==> bool"
  where "fbounded_below f X ≡ (∃ m . ∀ y ∈ topspace X . f y ≥ m)"

abbreviation fbounded_above :: "('a ==> real) ==> 'a topology ==> bool"
  where "fbounded_above f X ≡ (∃ M . ∀ y ∈ topspace X . f y ≤ M)"

abbreviation fbounded :: "('a ==> real) ==> 'a topology ==> bool"
  where "fbounded f X ≡ (∃ m M . ∀ y ∈ topspace X . m ≤ f y ∧ f y ≤ M)"

lemma fbounded_iff:
  shows "fbounded f X ⟷ fbounded_below f X ∧ fbounded_above f X"
  by auto

abbreviation c_of :: "'a topology ==> ('a ==> real) set" (‹ C( _ ) ›)
  where "C(X) ≡ { f . continuous_map X euclideanreal f }"

abbreviation cstar_of :: "'a topology ==> ('a ==> real) set"  (‹ C*( _ ) ›)
  where "C* X ≡ { f | f . f ∈ c_of X ∧ fbounded f X }"

definition cstar_id :: "'a topology ==> ('a ==> real) ==> 'a ==> real"
  where "cstar_id X = (λ f ∈ C* X . f)"

abbreviation c_embedding :: "'a topology ==> 'b topology ==> ('a ==> 'b) ==> bool"
  where "c_embedding S X e ≡ embedding_map S X e ∧
                            (∀ fS ∈ C(S) . ∃ fX ∈ C(X) . ∀ x ∈ topspace S . fS x = fX (e x))"

abbreviation cstar_embedding :: "'a topology ==> 'b topology ==> ('a ==> 'b) ==> bool"
  where "cstar_embedding S X e ≡ embedding_map S X e ∧
                            (∀ fS ∈ C*(S) . ∃ fX ∈ C*(X) . ∀ x ∈ topspace S . fS x = fX (e x))"

definition c_embedded :: "'a topology ==> 'b topology ==> bool"
  where "c_embedded S X ≡ (∃ e . c_embedding S X e)"

definition cstar_embedded :: "'a topology ==> 'b topology ==> bool"
  where "cstar_embedded S X ≡ (∃ e . cstar_embedding S X e)"

lemma bounded_range_iff_fbounded:
  assumes "f ∈ C X"
  shows "bounded (f ` topspace X) ⟷ fbounded f X"
(is "?lhs ⟷ ?rhs")
proof 
  assume ?lhs
  then obtain x e where "∀ y ∈ f ` topspace X . dist x y ≤ e"
    using bounded_def[of "f ` topspace X"] by auto
  hence "∀ y ∈ f ` topspace X . y ∈ { (x-e) .. (x+e) }"
    using dist_real_def by auto
  thus ?rhs by auto
next
  assume ?rhs
  then obtain m M where "∀ y ∈ f ` topspace X . y ∈ {m..M}" by auto
  thus ?lhs using bounded_closed_interval[of m M] subsetI bounded_subset
    by meson
qed


text ‹
 Combinations of functions in $C(X)$ and $C^*(X)$
 ›

(* building members of C(X) and C*(X) *)
abbreviation fconst :: "real ==> 'a ==> real"
  where "fconst v ≡ (λ x . v)"

definition fmin :: "('a ==> real) ==> ('a ==> real) ==> ('a ==> real)"
  where "fmin f g = (λ x . min (f x) (g x))"

definition fmax :: "('a ==> real) ==> ('a ==> real) ==> ('a ==> real)"
  where "fmax f g = (λ x . max (f x) (g x))"

(* truncate f above and below specified bounds *)
definition fmid :: "('a ==> real) ==> ('a ==> real) ==> ('a ==> real) ==> 'a ==> real"
  where "fmid f m M = fmax m (fmin f M)"

(* Used to convert a C(X) function into a C*(X) one *)
definition fbound :: "('a ==> real) ==> real ==> real ==> 'a ==> real"
  where "fbound f m M = fmid f (fconst m) (fconst M)"

(* alias for continuous_map_real_min *)
lemma fmin_cts:
  assumes "(f ∈ C X) ∧ (g ∈ C X)"
  shows "fmin f g ∈ C X"
  using assms continuous_map_real_min[of X f g] fmin_def[of f g] by auto

(* alias for continuous_map_real_max *)
lemma fmax_cts:
  assumes "(f ∈ C X) ∧ (g ∈ C X)"
  shows "fmax f g ∈ C X"
  using assms continuous_map_real_max[of X f g] fmax_def[of f g] by auto

lemma fmid_cts:
  assumes "(f ∈ C X) ∧ (m ∈ C X) ∧ (M ∈ C X)"
  shows "fmid f m M ∈ C X"
  unfolding fmid_def using assms fmin_cts[of f X M] fmax_cts[of m X "(fmin f M)"] 
  by auto

lemma fconst_cts:
  shows "fconst v ∈ C X"
  by simp

lemma fbound_cts:
  assumes "f ∈ C X"
  shows "fbound f m M ∈ C X"
  unfolding fbound_def 
  using assms fmid_cts[of f X "fconst m" "fconst M"] fconst_cts[of m X] fconst_cts[of M X] 
  by auto
 

text ‹
 Bounded and bounding functions
 ›

lemma fconst_bounded:
  shows "fbounded (fconst v) X"
  by auto

lemma fmin_bounded_below:
  assumes "fbounded_below f X ∧ fbounded_below g X"
  shows "fbounded_below (fmin f g) X"
proof -
  obtain mf mg where "∀ y ∈ topspace X . f y ≥ mf ∧ g y ≥ mg" using assms by auto
  hence "∀ y ∈ topspace X . fmin f g y ≥ min mf mg" unfolding fmin_def min_def by auto
  thus ?thesis by auto
qed

lemma fmax_bounded_above:
  assumes "fbounded_above f X ∧ fbounded_above g X"
  shows "fbounded_above (fmax f g) X"
proof -
  obtain mf mg where "∀ y ∈ topspace X . f y ≤ mf ∧ g y ≤ mg" using assms by auto
  hence "∀ y ∈ topspace X . fmax f g y ≤ max mf mg" unfolding fmax_def max_def by auto
  thus ?thesis by auto
qed

lemma fmid_bounded:
  assumes "fbounded m X ∧ fbounded M X"
  shows "fbounded (fmid f m M) X"
proof -
  obtain mmin mmax Mmin Mmax 
    where "∀ y ∈ topspace X . mmin ≤ m y ∧ m y ≤ mmax ∧ Mmin ≤ M y ∧ M y ≤ Mmax"
    using assms by blast
  hence "∀ y ∈ topspace X . min mmin Mmin ≤ (fmid f m M y) ∧ (fmid f m M y) ≤ max mmax Mmax"
    unfolding fmid_def fmax_def fmin_def max_def min_def by auto
  thus ?thesis by auto
qed

lemma fbound_bounded:
  shows "fbounded (fbound f m M) X"
  using fmid_bounded[of X "fconst m" "fconst M"] fconst_bounded[of X m] fconst_bounded[of X M]
  unfolding fbound_def by simp


text ‹
 Members of $C^*(X)$
 ›

lemma fconst_cstar:
  shows "fconst v ∈ C* X"
  using fconst_cts[of v X] fconst_bounded[of X v]
  by auto

lemma fbound_cstar:
  assumes "f ∈ C X"
  shows "fbound f m M ∈ C* X"
  using assms fbound_cts[of f X m M] fbound_bounded[of X f m M]
  by auto

lemma cstar_nonempty: 
  shows "{} ≠ C* X"
  using fconst_cstar by blast


section ‹
 Weak topologies
 ›

definition funcset_types :: "'a set ==> ('b ==> 'a ==> 'c) ==> ('b ==> 'c topology) ==> 'b set ==> bool"
  where "funcset_types S F T I = (∀ i ∈ I . F i ∈ S → topspace (T i))"

lemma cstar_types:
  shows "funcset_types (topspace X) (cstar_id X) (λf ∈ C* X . euclideanreal) (C* X)"
  unfolding funcset_types_def 
  by simp

lemma cstar_types_restricted:
  shows "funcset_types (topspace X) (cstar_id X)
           (λf ∈ C* X. (subtopology euclideanreal (range' X f))) (C* X)"
proof -
  have "∀ f ∈ C* X . f ` topspace X ⊆ range' X f" using range'_def[of X] 
    by (metis closedin_subtopology_refl closedin_topspace closure_of_subset 
              topspace_euclidean_subtopology)
  thus ?thesis unfolding funcset_types_def
    by (simp add: image_subset_iff cstar_id_def)
qed


(* Inverse image of f, restricted to R *)
definition inverse' :: "('a ==> 'b) ==> 'a set ==> 'b set ==> 'a set"
where "inverse' f source target = { x ∈ source . f x ∈ target }"

lemma inverse'_alt:
  shows "inverse' f s t = (f -` t) ∩ s"
  using inverse'_def[of f s t] by auto
(*
  The weak topology induced on a set S by a collection of total functions (F i) : S \<Rightarrow> (T i)
  where each (T i) is a topological space.
*)

definition open_sets_induced_by_func :: "('a ==> 'b) ==> 'a set ==> 'b topology ==> 'a set set"
  where "open_sets_induced_by_func f source T
              = { (inverse' f source V) | V . openin T V ∧ f ∈ source → topspace T}"

definition weak_generators :: "'a set ==> ('b ==> 'a ==> 'c) ==> ('b ==> 'c topology) ==> 'b set ==> 'a set set"
  where "weak_generators source funcs tops index
          = ∪ { open_sets_induced_by_func (funcs i) source (tops i) | i. i ∈ index }"

definition weak_base :: "'a set ==> ('b ==> 'a ==> 'c) ==> ('b ==> 'c topology) ==> 'b set ==> 'a set set"
  where "weak_base source funcs tops index = base_generated_by (weak_generators source funcs tops index)"

definition weak_opens :: "'a set ==> ('b ==> 'a ==> 'c) ==> ('b ==> 'c topology) ==> 'b set ==> 'a set set"
  where "weak_opens source funcs tops index = opens_generated_by (weak_generators source funcs tops index)"

definition weak_topology :: "'a set ==> ('b ==> 'a ==> 'c) ==> ('b ==> 'c topology) ==> 'b set ==> 'a topology"
  where "weak_topology source funcs tops index
          = topology_generated_by (weak_generators source funcs tops index)"

lemma weak_topology_alt:
  shows "openin (weak_topology S F T I) U ⟷ U ∈ weak_opens S F T I"
  using weak_topology_def[of S F T I] weak_opens_def[of S F T I]
        opens_eq_generated_topology[of "weak_generators S F T I" U]
  by auto

lemma weak_generators_exist_for_each_point_and_axis:
  assumes "x ∈ S"
and       "funcset_types S F T I"
and       "i ∈ I"
and       "b = inverse' (F i) S (topspace (T i))"
and       "F i ∈ S → topspace (T i)"
shows     "x ∈ b ∧ b ∈ weak_generators S F T I"
proof -
  have xprops: "x ∈ {r ∈ S . F i r ∈ topspace (T i)}" 
    using assms(2) funcset_types_def[of S F T I] assms(3) assms(1)
    by blast     
  hence part1: "x ∈ b" using assms(4) inverse'_def[of "F i" S "topspace (T i)"]
    by auto

  have "openin (T i) (topspace (T i))" by simp
  hence "b ∈ open_sets_induced_by_func (F i) S (T i)"
    using open_sets_induced_by_func_def[of "F i" S "T i"] assms(4) assms(5)
          inverse'_def[of "F i" S "topspace (T i)"] xprops
    by auto    
  thus ?thesis using part1 weak_generators_def[of S F T I] assms(3) by auto
qed

lemma weak_generators_topspace:
  assumes "W = weak_topology S F T I"
  shows "topspace W = ∪ (weak_generators S F T I)"
  using weak_topology_def[of S F T I] assms by simp

lemma weak_topology_topspace:
  assumes "W = weak_topology S F T I"
and       "funcset_types S F T I"
shows     "(I = {} ⟶ topspace W = {}) ∧ (I ≠ {} ⟶ topspace W = S)"
proof (cases "I = {}")
  case True
  hence "weak_generators S F T I = {}" using assms(1) weak_generators_def[of S F T I] by auto
  hence "topspace W = {}" using assms(1) weak_generators_topspace[of W S F T I] by simp
  then show ?thesis using True by simp
next
  case False
  then obtain i where iprops: "i ∈ I"  by auto
  hence "(F i) ` S ⊆ topspace (T i)" 
    using assms(2) unfolding funcset_types_def by auto
  hence "inverse' (F i) S (topspace (T i)) = S"
    using inverse'_def[of "F i" S "topspace (T i)"] by auto
  moreover have "openin (T i) (topspace (T i))" using weak_generators_def by simp
  ultimately have "S ∈ open_sets_induced_by_func (F i) S (T i)"
    using open_sets_induced_by_func_def[of "F i" S "T i"] assms(2) iprops unfolding funcset_types_def
    by auto
  hence "S ∈ weak_generators S F T I" 
    using weak_generators_def[of S F T I] iprops by auto
  hence "S ⊆ topspace W" 
    using weak_generators_topspace[of W S F T I] assms by auto

  moreover have "topspace W ⊆ S" 
  proof -
    have "openin W (topspace W)" by auto
    hence "topspace W ∈ opens_generated_by (weak_generators S F T I)"
      using assms(1) unfolding weak_topology_def
      using opens_eq_generated_topology[of "weak_generators S F T I" "topspace W"]
      by simp
    then obtain A where "topspace W = ∪ A ∧ A ⊆ {∩ B |B. finite' B ∧ B ⊆ weak_generators S F T I}"
      using opens_generated_unfolded[of "weak_generators S F T I"] 
      by auto
    thus ?thesis using assms(2)
      unfolding weak_generators_def open_sets_induced_by_func_def inverse'_def funcset_types_def
      by blast
  qed
  ultimately show ?thesis using False by auto
qed
 
lemma weak_opens_nhood_base:
  assumes "W = weak_topology S F T I"
and       "openin W U"
and       "x ∈ U"
shows     "∃ b ∈ weak_base S F T I . x ∈ b ∧ b ⊆ U"  
proof -
  define G where "G = weak_generators S F T I"
  hence Wprops: "U ∈ opens_generated_by G" 
    using weak_topology_def[ of S F T I] opens_eq_generated_topology[of G] assms(1) assms(2) 
    by presburger
  then obtain B where Bprops: "B ⊆ base_generated_by G ∧ U = ∪B"
    unfolding opens_generated_by_def arbitrary_unions_of_def by auto
  then obtain b where "b ∈ base_generated_by G ∧ x ∈ b"
    using assms(3) by blast
  thus ?thesis using G_def weak_base_def[of S F T I]
    by (metis Union_iff Bprops assms(3) subset_eq)
qed

lemma opens_generate_opens:
assumes "∀ b ∈ S . openin T b"
shows   "∀ U ∈ opens_generated_by S . openin T U"
by (metis assms generate_topology_on_coarsest istopology_openin openin_topology_generated_by 
          opens_eq_generated_topology)

lemma weak_topology_is_weakest:
  assumes "W = weak_topology S F T I"
and       "funcset_types S F T I"
and       "topspace X = topspace W"
and       "∀ i ∈ I . continuous_map X (T i) (F i)"
and       "openin W U"
shows     "openin X U"
proof - 
  { fix b assume bprops: "b ∈ weak_generators S F T I"
    then obtain i where iprops: "i ∈ I ∧ b ∈ open_sets_induced_by_func (F i) S (T i)"
      using weak_generators_def[of S F T I] by auto
    hence Sprops: "S = topspace X"
      using assms(1) assms(2) weak_topology_topspace[of W S F T I]
      unfolding funcset_types_def assms(3) 
      by auto
    obtain V where Vprops: "openin (T i) V ∧ b = inverse' (F i) S V"
      using iprops open_sets_induced_by_func_def[of "F i" S "T i"] by auto
    have cts: "continuous_map X (T i) (F i)" using iprops assms(4) by auto
    hence "∀U. openin (T i) U ⟶ openin X {x ∈ topspace X. F i x ∈ U}" 
      unfolding continuous_map_def by simp
    hence "openin X {x ∈ topspace X. F i x ∈ V}" using Vprops by auto
    hence "openin X b" using Vprops Sprops unfolding inverse'_def by auto
  }
  hence "∀ b ∈ weak_generators S F T I . openin X b" by auto
  hence "∀ c ∈ weak_opens S F T I . openin X c"
    using assms(5) weak_opens_def[of S F T I] opens_generate_opens[of "weak_generators S F T I" X]
    by auto
  moreover have "U ∈ weak_opens S F T I" 
    using assms(1) weak_topology_def[of S F T I]  weak_opens_def[of S F T I]
          opens_eq_generated_topology[of "weak_generators S F T I" U] assms(5)
    by auto
  ultimately show ?thesis by auto
qed

lemma weak_generators_continuous:
  assumes "W = weak_topology S F T I"
and       "funcset_types S F T I"
and       "i ∈ I"
shows     "continuous_map W (T i) (F i)"
proof -
  have "S = topspace W" using assms(1) assms(2) assms(3) weak_topology_topspace[of W S F T I]
    unfolding funcset_types_def by auto
  hence "F i ∈ topspace W → topspace (T i)"
    using assms funcset_types_def[of S F T I] by auto
  moreover have "∀ V . openin (T i) V ⟶ openin W {x ∈ topspace W. (F i) x ∈ V}"
  proof -
    { fix V assume Vprops: "openin (T i) V"
      { assume hyp: "inverse' (F i) (topspace W) V ≠ {}"
        have "{x ∈ topspace W. (F i) x ∈ V} = inverse' (F i) (topspace W) V" 
          using inverse'_def[of "F i" "topspace W" V] by simp
        moreover have  "(inverse' (F i) (topspace W) V) ∈ open_sets_induced_by_func (F i) S (T i)"
          using Vprops assms weak_topology_topspace[of W S F T I] hyp
          unfolding open_sets_induced_by_func_def funcset_types_def
          by fastforce
        ultimately have "{x ∈ topspace W. (F i) x ∈ V} ∈ weak_generators S F T I"
          using weak_generators_def[of S F T I] assms(3) by auto
        hence "openin W {x ∈ topspace W. (F i) x ∈ V}"
          using assms(1) weak_topology_def[of S F T I] 
                generators_are_open[of "weak_generators S F T I"] 
                opens_eq_generated_topology[of "weak_generators S F T I" "{x ∈ topspace W. (F i) x ∈ V}"]
          by auto
      }
      hence "inverse' (F i) (topspace W) V ≠ {} ⟶ openin W {x ∈ topspace W. (F i) x ∈ V}"
        by auto
      moreover have "inverse' (F i) (topspace W) V = {} ⟶ openin W {x ∈ topspace W. (F i) x ∈ V}"
        by (metis openin_empty inverse'_def)
      ultimately have "openin W {x ∈ topspace W. (F i) x ∈ V}" by auto
    }
    thus ?thesis by auto
  qed
  ultimately show ?thesis using continuous_map_def by blast
qed

lemma funcset_types_on_empty:
  shows "funcset_types {} F T I"
  unfolding funcset_types_def by simp

lemma weak_topology_on_empty:
  assumes "W = weak_topology {} F T I"
  shows   "∀ U . openin W U ⟷ U = {}"
proof -
  have "topspace W = {}" 
    using assms(1) weak_topology_topspace[of W "{}" F T I] funcset_types_on_empty[of F T I] 
    by blast
  thus ?thesis by simp
qed




subsection ‹
 Tychonov spaces carry the weak topology induced by $C^*(X)$
 ›

abbreviation tych_space :: "'a topology ==> bool"
  where "tych_space X ≡ t1_space X ∧ completely_regular_space X"

abbreviation compact_Hausdorff :: "'a topology ==> bool"
  where "compact_Hausdorff X ≡ compact_space X ∧ Hausdorff_space X"

lemma compact_Hausdorff_imp_tych:
  assumes "compact_Hausdorff K"
  shows   "tych_space K"
  by (simp add: Hausdorff_imp_t1_space assms compact_Hausdorff_or_regular_imp_normal_space 
                normal_imp_completely_regular_space_A)

lemma tych_space_imp_Hausdorff:
  assumes "tych_space X"
  shows "Hausdorff_space X"
proof -
  have "Hausdorff_space euclideanreal" by auto
  moreover have "(0::real) ≠ (1::real)" by simp
  moreover have "(0::real) ∈ topspace euclideanreal ∧ (1::real) ∈ topspace euclideanreal" by simp
  ultimately have "∃ U V . openin euclideanreal U ∧ openin euclideanreal V ∧ (0::real) ∈ U ∧ (1::real) ∈ V ∧ disjnt U V"
    using Hausdorff_space_def[of euclideanreal] by blast
  then obtain U V 
    where UVprops: "openin euclideanreal U ∧ openin euclideanreal V ∧ (0::real) ∈ U ∧ (1::real) ∈ V ∧ disjnt U V"
    by auto

  { fix x y assume xyprops: "x ∈ topspace X ∧ y ∈ topspace X ∧ x ≠ y"
    hence "closedin X {y} ∧ x ∈ topspace X - {y}" 
      using assms(1) by (simp add: t1_space_closedin_finite)
    then obtain f 
      where fprops: "continuous_map X (top_of_set {0..1}) f ∧ f x = (0::real) ∧ f y ∈ {1::real}"
      using assms(1) completely_regular_space_def[of X] by blast
    hence freal: "continuous_map X euclideanreal f ∧ f x = 0 ∧ f y = 1" 
      using continuous_map_into_fulltopology by auto

    define U' where "U' = { v ∈ topspace X . f v ∈ U }"
    define V' where "V' = { v ∈ topspace X . f v ∈ V }"
    have "openin X U' ∧ openin X V'" 
      using U'_def V'_def UVprops freal continuous_map_def[of X euclideanreal f] 
      by auto
    moreover have "U' ∩ V' = {}" using UVprops U'_def V'_def disjnt_def[of U V] by auto
    moreover have "x ∈ U' ∧ y ∈ V'" using UVprops U'_def V'_def fprops xyprops by auto
    ultimately have "∃ U' V' . openin X U' ∧ openin X V' ∧ x ∈ U' ∧ y ∈ V' ∧ disjnt U' V' "
      using disjnt_def[of U' V'] by auto
  }
  hence "∀ x y . x ∈ topspace X ∧ y ∈ topspace X ∧ x ≠ y
              ⟶ (∃ U' V' . openin X U' ∧ openin X V' ∧ x ∈ U' ∧ y ∈ V' ∧ disjnt U' V' )"
    by auto
  thus ?thesis using Hausdorff_space_def[of X] by blast
qed

(* can restrict to the range-closures of the functions *)
lemma cstar_range_restricted:
  assumes "f ∈ C* X"
  and     "U ⊆ topspace euclideanreal"
shows     "inverse' f (topspace X) U = inverse' f (topspace X) (U ∩ range' X f)"
proof -
  define U' where "U' = U ∩ range' X f"
  hence "inverse' f (topspace X) U' ⊆ inverse' f (topspace X) U"
    unfolding inverse'_def U'_def by auto
  moreover have "inverse' f (topspace X) U ⊆ inverse' f (topspace X) U'"
  proof -
    { fix x assume hyp: "x ∈ inverse' f (topspace X) U"
      hence "f x ∈ U ∩ (f ` topspace X)" unfolding inverse'_def by auto
      hence "f x ∈ U ∩ range' X f" 
        unfolding range'_def
        by (metis Int_iff closure_of_subset_Int inf.orderE inf_top_left topspace_euclidean)
      hence "x ∈ inverse' f (topspace X) U'" 
        unfolding inverse'_def
        using U'_def hyp inverse'_alt by fastforce
    }
    thus ?thesis 
      by (simp add: subsetI)
  qed
  ultimately show ?thesis using U'_def by simp
qed

lemma weak_restricted_topology_eq_weak:
shows   "weak_topology (topspace X) (cstar_id X) (λ f ∈ C* X . euclideanreal) (C* X)
       = weak_topology (topspace X) (cstar_id X) (λ f ∈ C* X . subtopology euclideanreal (range' X f)) (C* X)"
proof -
  define T  where "T = (λ f ∈ C* X . euclideanreal)"
  define T' where "T' = (λ f ∈ C* X . subtopology euclideanreal (range' X f))"
  define W  where "W = weak_topology (topspace X) (cstar_id X) T (C* X)"
  define W' where "W' = weak_topology (topspace X) (cstar_id X) T' (C* X)"

  have "∀ f ∈ C* X . f ∈ topspace X → topspace (T f)"
    using T_def unfolding continuous_map_def T_def by auto

  have generators: "weak_generators (topspace X) (cstar_id X) T (C* X)
                = weak_generators (topspace X) (cstar_id X) T' (C* X)"
  proof -
    (* T \<longrightarrow> T' *)
    have "weak_generators (topspace X) (cstar_id X) T (C* X)
                ⊆ weak_generators (topspace X) (cstar_id X) T' (C* X)"
    proof -
      have "weak_generators (topspace X) (cstar_id X) T (C* X)
                ⊆ weak_generators (topspace X) (cstar_id X) T' (C* X)"
      proof -
        { fix U assume Uprops: "U ∈ weak_generators (topspace X) (cstar_id X) T (C* X)"
          then obtain f where fprops: "f ∈ (C* X) ∧ U ∈ open_sets_induced_by_func f (topspace X) (T f)"
            unfolding weak_generators_def using cstar_id_def[of X]
            by (smt (verit) Union_iff mem_Collect_eq restrict_apply')
          then obtain V where Vprops: "U = inverse' f (topspace X) V ∧ openin (T f) V"
            unfolding open_sets_induced_by_func_def by blast
          hence "U = inverse' f (topspace X) V" by auto
          hence rtp1: "U ⊆ topspace X" unfolding inverse'_def by auto

          have rtp2: "openin (T' f) (V ∩ range' X f)"
          proof -
            have "openin euclideanreal V" using fprops Vprops T_def by auto
            hence "openin (subtopology euclideanreal (range' X f)) (V ∩ range' X f)"
              by (simp add: openin_subtopology_Int) 
            thus ?thesis using fprops T'_def by auto
          qed

          have rtp3: "f ∈ topspace X → topspace (T' f)"
          proof -
            have "f ` topspace X ⊆ topspace euclideanreal" using fprops by auto
            hence "f ` topspace X ⊆ range' X f" unfolding range'_def
              by (meson closure_of_subset)
            thus ?thesis using T'_def fprops by auto
          qed

          hence rtp4: "U = inverse' f (topspace X) (V ∩ range' X f)"
          proof -
            have "inverse' f (topspace X) (V ∩ range' X f) ⊆ U"
              using Vprops fprops unfolding inverse'_def by auto
            moreover have "U ⊆ inverse' f (topspace X) (V ∩ range' X f)"
            proof -
              { fix u assume uprops: "u ∈ U"
                hence "f u ∈ V" using Vprops unfolding inverse'_def by auto
                moreover have "f u ∈ range' X f" using uprops rtp1 unfolding range'_def                   
                  by (metis closure_of_subset_Int imageI inf_top_left subset_iff topspace_euclidean)
                ultimately have "u ∈ inverse' f (topspace X) (V ∩ range' X f)"
                  unfolding inverse'_def range'_def using rtp1 uprops by force
              }
              thus ?thesis by auto
            qed
            ultimately show ?thesis by auto
          qed
          (* ... and hence ... *)
          have "U ∈ open_sets_induced_by_func f (topspace X) (T' f)"
            using rtp1 rtp2 rtp3 rtp4 unfolding open_sets_induced_by_func_def 
            by blast
          hence "U ∈ weak_generators (topspace X) (cstar_id X) T' (C* X)"
            using fprops weak_generators_def[of "(topspace X)" "(cstar_id X)" T' "(C* X)"] cstar_id_def[of X]
            by (smt (verit, best) Sup_upper in_mono mem_Collect_eq restrict_apply')
        }
        thus ?thesis by auto
      qed
      thus ?thesis by auto
    qed
    (* T' \<longrightarrow> T *)
    moreover have "weak_generators (topspace X) (cstar_id X) T' (C* X)
              ⊆ weak_generators (topspace X) (cstar_id X) T (C* X)"
    proof -
      { fix U assume Uprops: "U ∈ weak_generators (topspace X) (cstar_id X) T' (C* X)"
        then obtain f where fprops: "f ∈ (C* X) ∧ U ∈ open_sets_induced_by_func f (topspace X) (T' f)"
          unfolding weak_generators_def using cstar_id_def[of X]
          by (smt (verit) Union_iff mem_Collect_eq restrict_apply')
        (* Vprops:  U = f\<^sup>-\<^sup>1(V) with V open in T' *)
        then obtain V where Vprops: "U = inverse' f (topspace X) V ∧ openin (T' f) V"
          unfolding open_sets_induced_by_func_def by blast
        (* Vbigprops: V = Vbig \<inter> T'   with Vbig open in T *)
        have "T' f = subtopology (T f) (topspace (T' f))" 
          using T_def T'_def fprops unfolding range'_def by auto
        moreover have "openin (T' f) V" using Vprops by simp
        ultimately obtain Vbig where Vbigprops: "openin (T f) Vbig ∧ V = Vbig ∩ (topspace (T' f))"
          using openin_subtopology[of "T f" "topspace (T' f)"]
          by auto
        (* Vrestrict: Vbig \<inter> T' = Vbig \<inter> range *)
        have Vrestrict: "Vbig ∩ topspace (T' f) = Vbig ∩ range' X f" 
          using T'_def fprops by auto
        (* Vrange: f\<^sup>-\<^sup>1(Vbig \<inter> range) = f\<^sup>-\<^sup>1(Vbig) *)
        have Vrange: "inverse' f (topspace X) (Vbig ∩ range' X f) = inverse' f (topspace X) Vbig"
        proof -
          { fix x assume "x ∈ inverse' f (topspace X) Vbig"
            hence "x ∈ topspace X ∧ f x ∈ Vbig ∩ range' X f"
              using range'_def[of X f] 
              by (metis Int_iff closure_of_subset image_subset_iff inverse'_alt subset_UNIV 
                  topspace_euclidean vimage_eq)
            hence "x ∈ inverse' f (topspace X) (Vbig ∩ range' X f)" unfolding inverse'_def by auto
          }
          hence "inverse' f (topspace X) Vbig ⊆ inverse' f (topspace X) (Vbig ∩ range' X f)" by auto
          thus ?thesis unfolding inverse'_def by auto
        qed
        hence "U = inverse' f (topspace X) Vbig ∧ openin (T f) Vbig"
          by (simp add: Vbigprops Vprops Vrestrict)
        moreover have fcstar: "f ∈ C* X" using fprops by simp
        ultimately have "U ∈ open_sets_induced_by_func f (topspace X) (T f)"
          using open_sets_induced_by_func_def[of f "topspace X" euclideanreal] T_def
          by auto
        hence "U ∈ open_sets_induced_by_func (cstar_id X f) (topspace X) (T f) ∧ f ∈ C* X"
          using fcstar cstar_id_def[of X] by auto
        hence "U ∈ weak_generators (topspace X) (cstar_id X) T (C* X)"
          using fcstar unfolding weak_generators_def by auto
      }
      thus ?thesis by auto
    qed
    ultimately show ?thesis by auto
  qed
  thus ?thesis by (simp add: T_def T'_def weak_topology_def cstar_id_def)
qed


subsection ‹
 A topology is a weak topology if it admits a continuous function set that separates
 points from closed sets
 ›

definition funcset_separates_points :: "'a topology ==> ('b ==> 'a ==> 'c) ==> 'b set ==> bool"
  where "funcset_separates_points X F I
            = (∀ x ∈ topspace X . ∀ y ∈ topspace X . x ≠ y ⟶ (∃ i ∈ I . F i x ≠ F i y))"

definition funcset_separates_points_from_closed_sets ::
    "'a topology ==> ('b ==> 'a ==> 'c) ==> ('b ==> 'c topology) ==> 'b set ==> bool"
  where "funcset_separates_points_from_closed_sets X F T I
            = (∀ x . ∀ A . closedin X A ∧ x ∈ (topspace X - A)
                        ⟶ (∃ i ∈ I . F i x ∉ (T i) closure_of (F i ` A)))"

lemma funcset_separates_points_from_closed_sets_imp_weak:
  assumes "funcset_separates_points_from_closed_sets X F T I"
and       "∀ i ∈ I . continuous_map X (T i) (F i)"
and       "W = weak_topology (topspace X) F T I"
and       "funcset_types (topspace X) F T I"
  shows   "X = W"
proof -
  { fix U assume Uhyp: "openin X U"
    { fix x assume xhyp: "x ∈ U"
      define A where "A = (topspace X) - U"
      have xinX: "x ∈ topspace X" using Uhyp xhyp openin_subset by auto
      moreover have Aprops: "closedin X A ∧ x ∉ A" using Uhyp xhyp A_def by auto
      ultimately obtain i where iprops: "i ∈ I ∧ F i x ∉ (T i) closure_of (F i ` A)"
        using assms(1) funcset_separates_points_from_closed_sets_def[of X F T I] by auto
  
      define V where "V = topspace (T i) - (T i) closure_of (F i ` A)"
      define R where "R = { p ∈ (topspace X) . F i p ∈ V }"
        have Vopen: "openin (T i) V ∧ F i x ∈ V" using iprops xinX V_def
        by (metis DiffI Int_iff assms(2) closedin_closure_of continuous_map_preimage_topspace 
                  openin_diff openin_topspace vimage_eq)
      hence "x ∈ R" using R_def assms(2) xinX by simp
      moreover have "R ⊆ U" 
      proof -
        have "F i ` R ⊆ V" using R_def by auto
        hence "F i ` R ∩ (T i) closure_of (F i ` A) = {}" using V_def by auto
        moreover have "F i ` A ⊆ (T i) closure_of (F i ` A)"
          by (metis Aprops assms(2) closure_of_eq continuous_map_image_closure_subset iprops) 
        ultimately have "F i ` R ∩ (F i `A) = {}" by auto
        hence "R ∩ A = {}" by auto
        thus ?thesis using A_def R_def by auto
      qed
      moreover have "openin W R" 
      proof -
        have "R = inverse' (F i) (topspace X) V" 
          by (simp add: R_def inverse'_def)
        hence "R ∈ open_sets_induced_by_func (F i) (topspace X) (T i)"
          using open_sets_induced_by_func_def[of "F i" "topspace X" "T i"] Vopen
                assms(2) continuous_map_funspace iprops by fastforce
        hence "R ∈ weak_generators (topspace X) F T I"
          using weak_generators_def[of "topspace X" F T I] iprops by auto
        thus ?thesis using generators_are_open[of "weak_generators (topspace X) F T I"]
          opens_eq_generated_topology[of "weak_generators (topspace X) F T I" R] assms(3)
          by (simp add: topology_generated_by_Basis weak_topology_def)
      qed
      ultimately have "x ∈ R ∧ R ⊆ U ∧ openin W R" by auto
      hence "∃ R . x ∈ R ∧ R ⊆ U ∧ openin W R" by auto
    }
    hence "∀ x . x ∈ U ⟶ (∃ R . x ∈ R ∧ R ⊆ U ∧ openin W R)"
      by auto
    hence "openin W U" by (meson openin_subopen)
  }
  hence XimpW: "∀ U . openin X U ⟶ openin W U" by auto

  moreover have "∀ U . openin W U ⟶ openin X U"
  proof -
    have "topspace X = topspace W" 
      using assms(3) assms(4) weak_topology_topspace[of W "topspace X" F T I]
      by (metis XimpW openin_topspace openin_topspace_empty subtopology_eq_discrete_topology_empty)
    thus ?thesis
      using assms(3) assms(4) assms(2) weak_topology_is_weakest[of W "topspace X" F T I X] 
      by blast
  qed
  ultimately show ?thesis by (meson topology_eq)
qed


text ‹
 The canonical functions on a product space: evaluation and projection
 ›

definition evaluation_map :: "'a topology ==> ('b ==> 'a ==> 'c) ==> 'b set ==> 'a ==> 'b ==> 'c"
  where "evaluation_map X F I = (λ x ∈ topspace X . (λ i ∈ I . F i x))"

definition product_projection :: "('a ==> 'b topology) ==> 'a set ==> 'a ==> ('a ==> 'b) ==> 'b"
  where "product_projection T I = (λ i ∈ I . (λ p ∈ topspace (product_topology T I) . p i))"

lemma product_projection:
  shows "∀ i ∈ I . ∀ p ∈ topspace (product_topology T I) . product_projection T I i p = p i"
  using product_projection_def[of T I] by simp

(* evaluation and projection are complementary *)
lemma evaluation_then_projection:
assumes "∀ i ∈ I . F i ∈ topspace X → topspace (T i)"
  shows "∀ i ∈ I . ∀ x ∈ topspace X . ((product_projection T I i) o (evaluation_map X F I)) x = F i x" 
proof -
  { fix i assume iprops: "i ∈ I"
    { fix x assume xprops: "x ∈ topspace X"
      have Fix: "(λ i ∈ I . F i x) ∈ topspace (product_topology T I)" using xprops assms(1) by auto
      have "((product_projection T I i) o (evaluation_map X F I)) x
                = (product_projection T I i) ((λ x ∈ topspace X . (λ i ∈ I . F i x)) x)"
        unfolding evaluation_map_def by auto
      moreover have "… = (product_projection T I i) (λ i ∈ I . F i x)" using xprops by simp
      moreover have "… = (λ p ∈ topspace (product_topology T I) . p i) (λ i ∈ I . F i x)"
        unfolding product_projection_def using iprops by auto
      moreover have "… = F i x" using Fix iprops by simp
      ultimately have "((product_projection T I i) o (evaluation_map X F I)) x = F i x" by auto
    }
    hence "∀ x ∈ topspace X . ((product_projection T I i) o (evaluation_map X F I)) x = F i x" 
      by auto
  }
  thus ?thesis by auto
qed


subsection ‹
 A product topology is the weak topology induced by its projections if the projections
 separate points from closed sets.
 ›

lemma projections_continuous:
  assumes "P = product_topology T I"
and       "F = (λ i ∈ I . product_projection T I i)"
shows     "∀i∈I. continuous_map P (T i) (F i)" 
    using assms(1) assms(2) product_projection_def[of T I]
    by fastforce

lemma product_topology_eq_weak_topology:
  assumes "P = product_topology T I"
and       "F = (λ i ∈ I . product_projection T I i)"
and       "W = weak_topology (topspace P) F T I"
and       "funcset_types (topspace P) F T I"
and       "funcset_separates_points_from_closed_sets P F T I"
shows     "P = W"
using assms product_projection_def[of T I] projections_continuous
      funcset_separates_points_from_closed_sets_imp_weak[of P F T I W]
    by simp


text ‹
 Reducing the domain and minimising the range of continuous functions,
 and related results concerning weak topologies.
 ›

lemma continuous_map_reduced:
  assumes "continuous_map X Y f"
  shows   "continuous_map (subtopology X S) (subtopology Y (f`S)) (restrict f S)"
  using assms continuous_map_from_subtopology continuous_map_in_subtopology by fastforce

lemma inj_on_imp:
  assumes "inj_on f S"
  shows "∀ y . (y ∈ f ` S) ⟷ (∃ x ∈ S . y = f x)"
by (simp add: image_iff)

lemma injection_on_intersection:
  assumes "inj_on f S"
and       "B ≠ {}"
and       "∀ b ∈ B . b ⊆ S"
  shows   "f ` (∩B) = ∩{ f ` b | b . b ∈ B }"
(is "?lhs = ?rhs")
proof -
  have "?lhs ⊆ ?rhs" by auto
  moreover have "?rhs ⊆ ?lhs"
  proof -
    { fix y assume rhs: "y ∈ ?rhs"
      then obtain b where bprops: "y ∈ f ` b ∧ b ∈ B" 
        by (smt (verit, del_insts) Inter_iff assms(2) ex_in_conv mem_Collect_eq)
      then obtain x where xprops: "x ∈ b ∧ b ∈ B ∧ y = f x" by auto

      (* since y is in all b's ... *)
      have  "∀ b ∈ B . y ∈ f ` b" using rhs by auto
      hence "∀ b ∈ B . f x ∈ f ` b" using xprops by auto
      hence "∀ b ∈ B . x ∈ b" using assms(1)
        by (meson assms(3) in_mono inj_on_image_mem_iff xprops)
      hence "x ∈ ∩B" by auto
      hence "y ∈ ?lhs" using xprops by auto
    }
    thus ?thesis by auto
  qed
  ultimately show ?thesis by auto
qed


subsection ‹
 Evaluation is an embedding for weak topologies
 ›

lemma evaluation_is_embedding:
  assumes "X = weak_topology (topspace X) F T I"
and       "P = product_topology T I"
and       "funcset_types (topspace X) F T I"
and       "funcset_separates_points X F I"
shows     "embedding_map X P (evaluation_map X F I)"
proof -
  define ev   where "ev = evaluation_map X F I"
  define proj where "proj = product_projection T I"
  define R    where "R = ev ` topspace X"
  define Rtop where "Rtop = subtopology P R"

(* ev is injective *)
  have injective: "inj_on ev (topspace X)"
  proof -
    have sigs: "∀ i ∈ I . F i ∈ (topspace X) → (topspace (T i))"
      using assms(3) funcset_types_def[of "topspace X" F T I]
      by blast

    { fix x y assume xyprops: "x ∈ topspace X ∧ y ∈ topspace X"
      { assume hyp: "x ≠ y"
        then obtain i where iprops: "i ∈ I ∧ F i x ≠ F i y"
          using assms(4) funcset_separates_points_def[of X F I] hyp xyprops
          by blast
        hence "(proj i) (ev x) ≠ (proj i) (ev y)"
          using evaluation_then_projection[of I F X T] proj_def ev_def
          by (simp add: sigs xyprops)          
        hence "ev x ≠ ev y" by auto
      }
      hence "ev x = ev y ⟶ x = y" by auto
    }
    thus ?thesis using inj_on_def by blast
  qed
(* ev is continuous *)
  moreover have ev_cts: "continuous_map X Rtop ev"
  proof -
    have main: "∀ i ∈ I . ∀ x ∈ topspace X . (proj i o ev) x = F i x" 
      using proj_def ev_def product_projection_def[of T I] evaluation_then_projection[of I F X T]
            evaluation_map_def[of X F I]
      by (metis assms(1) assms(3) continuous_map_funspace weak_generators_continuous)
    moreover have "∀ i ∈ I . continuous_map X (T i) (F i)" 
      using weak_generators_continuous[of X "topspace X" F T I] assms by auto
    moreover have "∀ i ∈ I . ∀ x ∈ topspace X . F i x = ev x i"
      using product_projection_def[of T I] main ev_def
      by (simp add: evaluation_map_def[of X F I])
    moreover have "ev ` topspace X ⊆ extensional I"
      using ev_def extensional_def assms evaluation_map_def[of X F I]
      by fastforce
    ultimately have "continuous_map X P ev" 
      using assms proj_def ev_def Rtop_def continuous_map_componentwise[of X T I ev]
            continuous_map_eq by fastforce
    thus ?thesis
      using Rtop_def R_def continuous_map_in_subtopology by blast
  qed
(* ev is open *)
  moreover have "open_map X Rtop ev"
  proof -
    have open_map_on_gens: "∀ U ∈ weak_generators (topspace X) F T I . openin Rtop (ev ` U)"
    proof -
      { define Rs where "Rs = (λ i ∈ I . (F i ` topspace X))"
        define Rtops where "Rtops = (λ i ∈ I . subtopology (T i) (Rs i))"

        fix U assume "U ∈ weak_generators (topspace X) F T I"
        then obtain i where iprops: "i ∈ I ∧ U ∈ open_sets_induced_by_func (F i) (topspace X) (T i)"
          using assms weak_generators_def[of "topspace X" F T I] by auto
        then obtain V 
          where Vprops: "openin (T i) V ∧ U = inverse' (F i) (topspace X) V"
          using open_sets_induced_by_func_def[of "F i" "topspace X" "T i"]
          by blast
        hence Uprops: "openin (T i) V ∧ U = { x ∈ topspace X . F i x ∈ V }"
          using inverse'_def[of "F i" "topspace X" V] by auto
        moreover have "∀ x ∈ topspace X . F i x = ((proj i) o ev) x"
          using evaluation_then_projection[of I F X T] assms(3) 
                funcset_types_def[of "topspace X" F T I] iprops
                proj_def ev_def
          by auto
        hence "U = { x ∈ topspace X . ((proj i) o ev) x ∈ V }" using Uprops by auto
        hence "ev ` U = { y ∈ R . (proj i) y ∈ V }" using R_def by auto
        moreover have "{ y ∈ R . (proj i) y ∈ V } = R ∩ ((proj i) -` V )"
          by auto
        moreover have "continuous_map P (T i) (proj i)" 
          using continuous_map_product_projection[of i I T] iprops proj_def
                product_projection_def[of T I] assms(2)  by auto
        ultimately have summary: "openin (T i) V ∧ continuous_map P (T i) (proj i)
                        ∧ (ev ` U) = R ∩ ((proj i) -` V )"  by auto
        hence "∀U. openin (T i) U ⟶ openin P {x ∈ topspace P. proj i x ∈ U}"
          using continuous_map_def[of P "T i" "proj i"] by auto
        hence "openin P ((proj i -` V) ∩ topspace P)"
          using summary by blast
        moreover have "R ⊆ topspace P" 
          using R_def ev_def evaluation_map_def[of X F I] assms(3) 
                funcset_types_def[of "topspace X" F T I]
          by (metis Rtop_def ev_cts continuous_map_image_subset_topspace 
              continuous_map_into_fulltopology)
        ultimately have "openin Rtop ((proj i -` V) ∩ R)"
          using Rtop_def
          by (metis inf.absorb_iff2 inf_assoc openin_subtopology)
        hence "openin Rtop (ev ` U)" using summary 
          by (simp add: inf_commute)
      }
      thus ?thesis by auto
    qed

    have open_map_on_basics: "∀ U ∈ weak_base (topspace X) F T I . openin Rtop (ev ` U)"
    proof -
      have Ugens: "∪ (weak_generators (topspace X) F T I) = topspace X"
        using assms(1) weak_generators_topspace by blast

      { fix U assume bprops: "U ∈ weak_base (topspace X) F T I"
        hence "U ∈ finite_intersections_of (weak_generators (topspace X) F T I)"
          by (simp add: base_generated_by_def weak_base_def)
        then obtain b where bprops: "b ⊆ weak_generators (topspace X) F T I ∧ finite' b ∧ U = ∩b"
          unfolding finite_intersections_of_def
          by auto
        hence "finite' b ∧ (∀ g ∈ b . openin Rtop (ev ` g))" using open_map_on_gens by auto
        hence "openin Rtop (∩ { (ev ` g) | g . g ∈ b })" by auto
        hence "openin Rtop (ev ` ∩b)" 
          using injection_on_intersection[of ev "topspace X" b] bprops 
          by (metis (no_types, lifting) Ugens Union_upper in_mono injective)
        hence "openin Rtop (ev ` U)" using bprops by metis
      }
      thus ?thesis by auto
    qed
    hence open_map_on_opens: "∀ U ∈ weak_opens (topspace X) F T I . openin Rtop (ev ` U)"
      by (smt (verit, ccfv_SIG) image_iff image_mono openin_subopen weak_opens_nhood_base 
          weak_topology_alt)
    thus ?thesis 
      using opens_eq_generated_topology[of "weak_generators (topspace X) F T I"] assms(1)
      unfolding weak_topology_def using open_map_def[of X Rtop]
      by (simp add: weak_opens_def)
  qed
(* so ev is a homeomorphism X \<longleftrightarrow> Rtop *)
  ultimately have "homeomorphic_map X Rtop ev"
    by (metis R_def Rtop_def bijective_open_imp_homeomorphic_map continuous_map_image_subset_topspace 
        continuous_map_into_fulltopology topspace_subtopology_subset)
  thus ?thesis using embedding_map_def[of X P ev] ev_def R_def Rtop_def
    by auto
qed
(* end of proof that ev is an embedding *)


section ‹
 Compactification
 ›

subsection ‹ Definition ›

lemma embedding_map_id: 
  assumes "S ⊆ topspace X"
  shows   "embedding_map (subtopology X S) X id" 
  using assms embedding_map_def topspace_subtopology_subset 
  by fastforce

(* X is densely embedded in compactification K via a known evaluation *)
definition compactification_via :: "('a ==> 'b) ==> 'a topology ==> 'b topology ==> bool"
  where "compactification_via f X K ≡ compact_space K ∧ dense_embedding X K f"

(* X is densely embedded in compactification K via an unknown evaluation *)
definition compactification :: "'a topology ==> 'b topology ==> bool"
  where "compactification X K = (∃ f . compactification_via f X K)"

lemma compactification_compactification_via:
  assumes "compactification_via f X K"
  shows   "compactification X K"
  using assms unfolding compactification_def by fastforce



subsection ‹
 Example: The Alexandroff compactification of a non-compact locally-compact Hausdorff space
 ›

lemma Alexandroff_is_compactification_via_Some: 
  assumes "¬ compact_space X ∧ Hausdorff_space X ∧ locally_compact_space X"
  shows "compactification_via Some X (Alexandroff_compactification X)"
  using assms compact_space_Alexandroff_compactification
              embedding_map_Some
              Alexandroff_compactification_dense
              compactification_via_def
  by (metis dense_in_def)


subsection ‹
 Example: The closure of a subset of a compact space
 ›

lemma compact_closure_is_compactification:
  assumes "compact_space K"
and       "S ⊆ topspace K"
shows     "compactification_via id (subtopology K S) (subtopology K (K closure_of S))"
proof -
  define big where "big = subtopology K (K closure_of S)"
  define small where "small = subtopology K S"
  have "dense_in big (id ` topspace small) (topspace big)"
    by (metis dense_in_def big_def small_def assms(2) closedin_topspace closure_of_minimal 
              closure_of_subset closure_of_subtopology_open id_def image_id inf.orderE 
              openin_imp_subset openin_subtopology_refl topspace_subtopology_subset)
  moreover have "embedding_map small big id"
    by (metis assms(2) big_def closure_of_subset_Int embedding_map_in_subtopology id_apply 
              embedding_map_id image_id small_def topspace_subtopology)
  ultimately have "dense_embedding small big id" by blast
  moreover have "compact_space big"
    by (simp add: big_def assms(1) closedin_compact_space compact_space_subtopology)
  ultimately show ?thesis 
    unfolding compactification_via_def using small_def big_def by blast
qed


subsection ‹
 Example: A compact space is a compactification of itself
 ›

lemma compactification_of_compact:
  assumes "compact_space K"
  shows   "compactification_via id K K"
  using compact_closure_is_compactification[of K "topspace K"]
  by (simp add: assms)


subsection ‹
 Example: A closed non-trivial real interval is a compactification of its interior
 ›

lemma closed_interval_interior:
  shows "{a::real <..< b} = interior {a..b}"
  by auto

lemma open_interval_closure:
  shows "(a < (b::real)) ⟶ {a .. b} = closure {a <..< b}" 
    using closure_greaterThanLessThan[of a b] by simp

lemma closed_interval_compactification:
  assumes "(a::real) < b"
and       "open_interval = subtopology euclideanreal {a<..<b}"
and       "closed_interval = subtopology euclideanreal {a..b}"
  shows "compactification open_interval closed_interval"
proof -
  have "compact_space closed_interval" using assms(3)
    using compact_space_subtopology compactin_euclidean_iff by blast
  moreover have "Hausdorff_space closed_interval"
    by (simp add: Hausdorff_space_subtopology assms(3))
  moreover have "{a<..<b} ⊆ topspace closed_interval"
    by (simp add: assms(3) greaterThanLessThan_subseteq_atLeastAtMost_iff)
  ultimately have "compactification_via id open_interval closed_interval"
    using compact_closure_is_compactification[of closed_interval "{a<..<b}"]
          open_interval_closure[of a b]
    by (metis assms closedin_self closedin_subtopology_refl closure_of_subtopology 
              euclidean_closure_of subtopology_subtopology subtopology_topspace 
              topspace_subtopology_subset)
  thus ?thesis using
          compactification_compactification_via[of id open_interval closed_interval]
    by auto
qed


section ‹ The Stone-{\v C}ech compactification of a Tychonov space ›


(* smallest closed interval containing the range of a bounded function *)
lemma compact_range':
  assumes "f ∈ C* X"
  shows   "compact (range' X f)"
proof -
  obtain m M where mM: "∀ y ∈ topspace X . f y ∈ {m..M}" using assms by auto
  hence "f ` topspace X ⊆ {m..M}" by auto
  hence "range' X f ⊆ euclideanreal closure_of {m..M}" 
    unfolding range'_def by (meson closure_of_mono)
  moreover have "compact {m..M}" by auto
  ultimately show ?thesis
    by (metis closed_Int_compact closed_atLeastAtMost closed_closedin closedin_closure_of 
              closure_of_closedin inf.order_iff range'_def)
qed

lemma c_range_nonempty:
  assumes "f ∈ C(X)"
and       "topspace X ≠ {}"
shows   "range' X f ≠ {}"
proof -
  have "f ` topspace X ≠ {}" using assms by blast
  thus ?thesis unfolding range'_def by simp
qed

lemma cstar_range_nonempty:
  assumes "f ∈ C* X"
and       "topspace X ≠ {}"
shows     "range' X f ≠ {}"
  using assms c_range_nonempty[of f X]
  by auto

(* C*(X) separates points from closed subsets in a tych_space *)
lemma cstar_separates_tych_space:
  assumes "tych_space X"
  shows "funcset_separates_points_from_closed_sets X (cstar_id X) (λf ∈ C* X. euclideanreal) (C* X)
         ∧ funcset_separates_points X (cstar_id X) (C* X)"
proof -
  { fix x S assume "closedin X S ∧ x ∈ topspace X - S"
    then obtain f 
      where fprops: "continuous_map X (top_of_set {0..(1::real)}) f ∧ f x = 0 ∧ f ` S ⊆ {1}"
      using assms completely_regular_space_def[of X] 
      by presburger
    hence "f ∈ C X" 
      using continuous_map_into_fulltopology[of X euclideanreal "{0..(1::real)}" f]
      by auto
    moreover have "fbounded f X"
      by (meson atLeastAtMost_iff continuous_map_upper_lower_semicontinuous_le_gen fprops)
    ultimately have f_in_cstar: "f ∈ (C* X)" by auto

    moreover have f_separates: "f x ∉ (euclideanreal closure_of (f ` S))"
    proof -
      have "closedin euclideanreal (f ` S)"
        by (metis closed_closedin closed_empty closed_singleton fprops subset_singletonD)
      moreover have "f x ∉ f ` S" using fprops by auto
      thus ?thesis using calculation by auto
    qed
    ultimately have "∃ f ∈ C* X . f x ∉ euclideanreal closure_of (f ` S)" by auto
  }
  hence rtp1: "funcset_separates_points_from_closed_sets X (cstar_id X) (λf ∈ C* X. euclideanreal) (C* X)"
    using cstar_id_def[of X] unfolding funcset_separates_points_from_closed_sets_def by auto

  moreover have "funcset_separates_points X (cstar_id X) (C* X)" 
  proof -
    { fix x y assume "{x,y} ⊆ topspace X ∧ x ≠ y"
      hence "closedin X {y} ∧ x ∈ topspace X - {y}" 
        using assms by (simp add: t1_space_closedin_finite)
      hence "∃f ∈ C* X . cstar_id X f x ∉ (λf∈ C* X . euclideanreal) f closure_of cstar_id X f ` {y}" 
        using funcset_separates_points_from_closed_sets_def[of X "cstar_id X" "λ f ∈ C* X . euclideanreal" "C* X"]
              rtp1 by presburger
      hence "∃ f ∈ C* X . f x ≠ f y"  
        using cstar_id_def[of X] t1_space_closedin_finite[of euclideanreal] by auto
    }
    thus ?thesis using cstar_id_def[of X] unfolding funcset_separates_points_def by auto
  qed
  ultimately show ?thesis by auto
qed


text ‹
 The product topology induced by $C^*(X)$ on a Tychonov space.
 ›

(* scT identifies the compact component of product_topology associated with each f in C*(X) *)
definition scT :: "'a topology ==> ('a ==> real) ==> real topology"
  where "scT X = (λ f ∈ C* X . subtopology euclideanreal (range' X f))"

(* sometimes we want the whole of euclideanreal, not just the range' *)
definition scT_full :: "'a topology ==> ('a ==> real) ==> real topology"
  where "scT_full X = (λ f ∈ C* X . euclideanreal)"

(* the product_topology cube containing \<beta>X *)
definition scProduct :: "'a topology ==> (('a ==> real) ==> real) topology"
  where "scProduct X = product_topology (scT X) (C* X)"

(* the projection operator for scProduct *)
definition scProject :: "'a topology ==> ('a ==> real) ==> (('a ==> real) ==> real) ==> real"
  where "scProject X = product_projection (scT X) (C* X)"

(* the evaluation operator for scProduct (called scEmbed, as we'll see below that it's an embedding *)
definition scEmbed :: "'a topology ==> 'a ==> ('a ==> real) ==> real"
  where "scEmbed X = evaluation_map X (cstar_id X) (C* X)"

lemma scT_images_compact_Hausdorff:
  shows "∀ f ∈ C* X . compact_Hausdorff (scT X f)"
proof -
  have T: "∀ f ∈ C* X . scT X f = subtopology euclideanreal (range' X f)"
    unfolding scT_def by simp
  thus ?thesis using range'_def[of X f]
    by (simp add: Hausdorff_space_subtopology compact_range' compact_space_subtopology)
qed

lemma scT_images_bounded:
  shows "∀ f ∈ C* X . bounded (topspace (scT X f))"
  using scT_images_compact_Hausdorff[of X] scT_def[of X]
  by (simp add: compact_imp_bounded compact_range')

lemma scProduct_compact_Hausdorff:
  shows "compact_Hausdorff (scProduct X)"
  unfolding scProduct_def using scT_images_compact_Hausdorff[of X]
  using compact_space_product_topology 
  by (metis (no_types, lifting) compact_Hausdorff_imp_regular_space regular_space_product_topology 
            regular_t0_eq_Hausdorff_space t0_space_product_topology)


text ‹
 The Stone-{\v C}ech compactification of a Tychonov space and its extension properties
 ›

lemma tych_space_weak:
  assumes "tych_space X"
shows     "X = weak_topology (topspace X) (cstar_id X) (scT X) (C* X)"
proof (cases "topspace X = {}")
  case True 
  then show ?thesis 
    using weak_topology_on_empty[of "weak_topology (topspace X) (cstar_id X) (scT X) (C* X)"]
          topology_eq by fastforce
next
  case False 
  define W where "W = weak_topology (topspace X) (cstar_id X) (scT X) (C* X)"
    
  hence "topspace W = topspace X"
    using cstar_types_restricted[of X] scT_def[of X] W_def cstar_nonempty[of X]
          weak_topology_topspace[of W "topspace X" "cstar_id X" "scT X" "C* X"]
    by auto
  moreover have "∀f. continuous_map X euclideanreal f ∧ fbounded f X ⟶
        continuous_map X (top_of_set (closure (f ` topspace X))) f"
    using closure_subset continuous_map_into_subtopology image_subset_iff by fastforce
  ultimately have  "openin X U" if "openin W U" for U
    using cstar_types_restricted[of X] scT_def[of X] cstar_id_def[of X] weak_topology_is_weakest [OF W_def] that
    by (simp add: range'_def)

  moreover have "openin W U" if U: "openin X U" for U
  proof -
    have "∃ V . x ∈ V ∧ V ⊆ U ∧ openin W V" if x: "x ∈ U" for x
    proof -
      have x_in_X: "x ∈ topspace X" 
        using openin_subset U x by fastforce

      define S where "S = topspace X - U"
      hence props': "x ∈ topspace X - S ∧ closedin X S" 
        using U openin_closedin_eq x  by fastforce
      then obtain f where fprops: "continuous_map X (top_of_set {0..1::real}) f ∧ f x = 0 ∧ f ` S ⊆ {1}" 
        using assms(1) completely_regular_space_def[of X]
        by meson
      then obtain ffull 
        where ffullprops: "(ffull ∈ C X) ∧ ffull x = (0::real) ∧ ffull ` S ⊆ {1}"
        using continuous_map_into_fulltopology 
        by (metis mem_Collect_eq)

      define F where "F = fbound ffull 0 1"
      hence Fcstar: "F ∈ C* X" using ffullprops fbound_cstar[of ffull X 0 1] by auto
      hence Ftype: "F ∈ topspace X → topspace euclideanreal"
        unfolding continuous_map_def by auto

      define I where "I = {(-1) <..< 1::real}"
      hence Iprops: "openin euclideanreal I" 
        by (simp add: openin_delete)

      define V where "V = inverse' F (topspace X) I"

      have crprops: "F x = 0 ∧ F ` S ⊆ {1}"
        using ffullprops F_def 
        unfolding fbound_def fmid_def fmin_def fmax_def min_def max_def
        by auto
      hence "V ⊆ U" 
        by (auto simp: S_def I_def inverse'_def V_def)
      moreover have "x ∈ V" 
        using crprops I_def x_in_X unfolding inverse'_def V_def by auto  
      moreover have "openin W V" (* sledgehammer needs step-by-step guidance *)
      proof -
        have "V ∈ open_sets_induced_by_func F (topspace X) euclideanreal"
          unfolding open_sets_induced_by_func_def using Ftype V_def Iprops
          by blast
        moreover have "open_sets_induced_by_func F (topspace X) euclideanreal ⊆
                         weak_generators (topspace X) (cstar_id X) (scT_full X) (C* X)"
          using weak_generators_def[of "topspace X" "(cstar_id X)" "scT_full X" "C* X"] 
            scT_full_def[of X] cstar_id_def[of X] Fcstar 
          by (smt (verit, ccfv_SIG) Sup_upper mem_Collect_eq restrict_apply')
        ultimately have "V ∈ weak_generators (topspace X) (cstar_id X) (scT_full X) (C* X)"
          by auto
        hence "openin (topology_generated_by (weak_generators (topspace X) (cstar_id X) (scT_full X) (C* X))) V"
          using generators_are_open[of "weak_generators (topspace X) (cstar_id X) (scT_full X) (C* X)"]
            topology_generated_by_Basis by blast
        thus ?thesis 
          using W_def weak_restricted_topology_eq_weak[of X]
          unfolding scT_def scT_full_def weak_topology_def
          by simp
      qed
      ultimately show ?thesis by auto
    qed
    thus ?thesis by (meson openin_subopen)
  qed
  ultimately have "∀ U . openin X U ⟷ openin W U" by auto
  hence "X = W" by (simp add: topology_eq)
  thus ?thesis using W_def by simp
qed


subsection ‹
 Definition of $\beta{X}$
 ›

definition scEmbeddedCopy :: "'a topology ==> (('a ==> real) ==> real) set"
  where "scEmbeddedCopy X = scEmbed X ` topspace X"

definition scCompactification :: "'a topology ==> (('a ==> real) ==> real) topology" (‹β _›)
  where "scCompactification X
            = subtopology (scProduct X) ((scProduct X) closure_of (scEmbeddedCopy X))"

lemma sc_topspace:
  shows "topspace (β X) = (scProduct X) closure_of (scEmbeddedCopy X)"
  using scCompactification_def[of X] closure_of_subset_topspace by force

lemma scProject': 
  shows "∀ f ∈ C* X . ∀ p ∈ topspace (β X) . scProject X f p = p f"
proof -
  have "topspace (β X) ⊆ topspace (scProduct X)" unfolding scCompactification_def by auto
  thus ?thesis 
    unfolding scProject_def product_projection_def scProduct_def
    by auto
qed
    
        
text ‹
 Evaluation densely embeds Tychonov $X$ in $\beta{X}$
 ›

lemma dense_embedding_scEmbed:
  assumes "tych_space X"
  shows   "dense_embedding X (β X) (scEmbed X)"
proof -
  define W where "W = weak_topology (topspace X) (cstar_id X) (λf ∈ C* X. euclideanreal) (C* X)"
  hence "X = W" using assms tych_space_weak[of X]
    by (metis (mono_tags, lifting) scT_def weak_restricted_topology_eq_weak)

  hence Xweak: "X = weak_topology (topspace X) (cstar_id X) (scT X) (C* X)"
    using scT_def[of X] W_def cstar_id_def[of X]
          weak_restricted_topology_eq_weak[where X ="X"] by auto
  moreover have "scProduct X = product_topology (scT X) (C* X)" using scProduct_def[of X] by auto
  moreover have "funcset_types (topspace X) (cstar_id X) (scT X) (C* X)"
    unfolding scT_def using cstar_types_restricted[of X] by auto
  moreover have "funcset_separates_points X (cstar_id X) (C* X)"
    using cstar_separates_tych_space[of X] assms(1) by auto
  moreover have "(C* X) ≠ {}" using cstar_nonempty by auto
  ultimately have "embedding_map X (scProduct X) (scEmbed X)"
    using evaluation_is_embedding[of X "cstar_id X" "scT X" "C* X" "scProduct X"]
    unfolding scProduct_def scEmbed_def
    by auto
  hence embeds: "embedding_map X (β X) (scEmbed X)"
    unfolding scCompactification_def 
    by (metis closure_of_subset embedding_map_in_subtopology scEmbeddedCopy_def subtopology_topspace)
  moreover have "dense_in (β X) (scEmbed X ` topspace X) (topspace (β X))"
    unfolding dense_in_def using scCompactification_def[of X] scEmbeddedCopy_def[of X]
    by (metis Int_absorb1 closure_of_subset closure_of_subset_topspace closure_of_subtopology 
              embedding_map_in_subtopology embeds set_eq_subset subtopology_topspace 
              topspace_subtopology_subset)
  ultimately show ?thesis by auto
qed


subsection ‹
 $\beta{X}$ is a compactification of $X$
 ›

lemma scCompactification_compact_Hausdorff:
  assumes "tych_space X"
  shows   "compact_Hausdorff (β X)"
  using scCompactification_def[of X] scProduct_compact_Hausdorff[of X]
  by (simp add: Hausdorff_space_subtopology closedin_compact_space compact_space_subtopology)

lemma scCompactification_is_compactification_via_scEmbed:
  assumes "tych_space X"
  shows "compactification_via (scEmbed X) X (β X)"
  using compactification_via_def[of "scEmbed X" X "β X"]
        scCompactification_compact_Hausdorff[of X]
        dense_embedding_scEmbed[of X] assms 
  by auto

lemma scCompactification_is_compactification:
  assumes "tych_space X"
  shows   "compactification X (β X)"
  using assms compactification_compactification_via
              scCompactification_is_compactification_via_scEmbed
  by blast

lemma scEvaluation_range: 
  assumes "x ∈ topspace X"
and       "tych_space X"
shows     "(λ f ∈ C* X . f x) ∈ topspace (product_topology (scT X) C* X)"
proof -
  have "funcset_types (topspace X) (cstar_id X) (λf∈ C* X . top_of_set (range' X f)) C* X"
    using cstar_types_restricted[of X] by auto
  hence "∀f∈ C* X . f ∈ topspace X → topspace (scT X f)"
    unfolding funcset_types_def scT_def cstar_id_def[of X] by auto
  thus ?thesis using topspace_product_topology[of "scT X" "C* X"] assms(1) by auto
qed

lemma scEmbed_then_project:
  assumes "f ∈ C* X"
and       "x ∈ topspace X"
and       "tych_space X"
shows     "scProject X f (scEmbed X x) = f x"
proof -
  have fequiv: "∀ y ∈ topspace X . (λ g ∈ C* X . (cstar_id X) g y) = (λ g ∈ C* X . g y)" 
  proof -
    { fix y assume yprops: "y ∈ topspace X"
      hence "∀ g ∈ C* X . (cstar_id X) g y = g y" unfolding cstar_id_def by auto
      hence "(λ g ∈ C* X . (cstar_id X) g y) = (λ g ∈ C* X . g y)" 
        by (meson restrict_ext)
    }
    thus ?thesis by auto
  qed
  
  have "scProject X f (scEmbed X x) = scProject X f (evaluation_map X (cstar_id X) (C* X) x)"
    unfolding scEmbed_def by auto
  also have "… = scProject X f (λg∈ C* X . g x)"
    unfolding evaluation_map_def using assms(2) fequiv by auto
  also have "… = (λg∈ C* X. λp∈topspace (product_topology (scT X) (C* X)). p g) f (λg∈ C* X . g x)"
    unfolding  product_projection_def scProject_def by auto
  also have "… = (λp∈topspace (product_topology (scT X) (C* X)). p f) (λg∈ C* X . g x)"
    using assms(1) by auto 
  also have "… = f x" using scEvaluation_range[of x X] assms by auto
  ultimately show ?thesis by auto
qed


subsection ‹
 Evaluation is a $C^*$-embedding of $X$ into $\beta{X}$
 ›

definition scExtend :: "'a topology ==> ('a ==> real) ==> (('a ==> real) ==> real) ==> real"
  where "scExtend X = (λ f ∈ C* X . restrict (scProject X f) (topspace (β X)))"

(* (scExtend X) extends functions in C*(X) to functions on topspace (\<beta> X) *)
proposition scExtend_extends:
  assumes "tych_space X"
  shows   "∀ f ∈ C* X . ∀ x ∈ topspace X . f x = (scExtend X f) (scEmbed X x)"
proof -
  { fix f assume fprops: "f ∈ C* X"
    have "∀ x ∈ topspace X . (scProject X f) (scEmbed X x) = (scExtend X f) (scEmbed X x) "
    proof - 
      { fix x assume xprops: "x ∈ topspace X"
        define p where pprops: "p = scEmbed X x"

        hence "scExtend X f p = (restrict (scProject X f) (topspace β X)) p" 
          using xprops fprops unfolding scExtend_def by auto
        moreover have "p ∈ topspace β X"
          using assms(1) pprops dense_embedding_scEmbed[of X]
                scCompactification_def[of X] scEmbeddedCopy_def[of X]
          by (metis (no_types, lifting) embedding_map_in_subtopology image_eqI
                    in_mono subtopology_topspace xprops)
        ultimately have "scExtend X f p = scProject X f p" 
          using pprops scEmbeddedCopy_def[of X] scEmbed_def[of X] evaluation_map_def by auto 
      }
      thus ?thesis by auto
    qed
    hence "∀ x ∈ topspace X . f x = (scExtend X f) (scEmbed X x)"  
      using scEmbed_then_project[of f X] assms(1) fprops by auto
  }
  thus ?thesis by auto
qed

lemma scExtend_extends_cstar:
  assumes "tych_space X"   
  shows   "∀ f ∈ C* X . (∀ x ∈ topspace X . f x = (scExtend X f) (scEmbed X x)) ∧ scExtend X f ∈ C* (β X)"
proof -
  define e where "e = scExtend X"
  { fix f assume fprops: "f ∈ C* X"
    hence  "continuous_map (scProduct X) (scT X f) (scProject X f)"
      using scProduct_def[of X] scProject_def[of X] 
            projections_continuous[of "scProduct X" "scT X" "C* X" "scProject X"]
            product_projection_def[of "scT X" "C* X"] 
      by (metis (no_types, lifting) restrict_extensional extensional_restrict)
    hence "continuous_map (β X) (scT X f) (scProject X f)"
      by (simp add: continuous_map_from_subtopology scCompactification_def)
    hence c_embedded_f: "continuous_map (β X) (scT X f) (scExtend X f)"
      using scExtend_def[of X] fprops by force
    moreover have fbounded_f:"fbounded (scExtend X f) (β X)"
    proof -
      obtain m M where "f ` topspace X ⊆ {m..M}" using fprops by force
      hence extend_on_embedded: "e f ` (scEmbeddedCopy X) ⊆ {m..M}"
        using scExtend_extends[of X] e_def
        by (smt (verit, ccfv_SIG) fprops assms(1) image_cong image_image scEmbeddedCopy_def)
      hence "e f ` (topspace (β X)) ⊆ {m..M}"
      proof -
        { fix p assume pprops: "p ∈ e f ` (topspace (β X))"
          then obtain v where vprops: "v ∈ topspace (β X) ∧ p = e f v" by auto
          { fix U assume Uprops: "openin (scT X f) U ∧ p ∈ U"
            define V where "V = inverse' (e f) (topspace (β X)) U"
            hence "openin (β X) V"
              using c_embedded_f Uprops e_def unfolding continuous_map_def inverse'_def
              by auto
            moreover have "topspace (β X) = (β X) closure_of scEmbeddedCopy X"
              using scCompactification_def[of X] closure_of_subset_topspace[of "β X" "scEmbeddedCopy X"]  
                    dense_embedding_scEmbed[of X] scEmbeddedCopy_def[of X]
              by (metis assms closure_of_subtopology_open embedding_map_in_subtopology 
                        subtopology_topspace topspace_subtopology)
            moreover have "v ∈ V ∧ v ∈ topspace (β X)" 
              using vprops V_def Uprops unfolding inverse'_def by auto
            ultimately obtain x where xprops: "x ∈ scEmbeddedCopy X ∧ x ∈ V"
              using in_closure_of[of v "β X" "scEmbeddedCopy X"]
              by presburger
            define w where "w = e f x"
            hence "w ∈ {m..M}" using extend_on_embedded xprops by blast
            moreover have "w ∈ U" using w_def xprops vprops V_def
              by (simp add: inverse'_alt)
            ultimately have "∃ w. w ∈ U ∩ {m..M}" by auto
          }
          hence "∀ U . openin (scT X f) U ∧ p ∈ U ⟶ (∃ w. w ∈ U ∩ {m..M})" by auto
          moreover have "p ∈ topspace (scT X f)" 
            by (metis e_def Int_iff vprops c_embedded_f continuous_map_preimage_topspace vimageE)
          ultimately have "p ∈ (scT X f) closure_of {m..M}"
            using in_closure_of[of p "scT X f" "{m..M}"]
            by auto
          hence "p ∈ euclideanreal closure_of {m..M}"
            using scT_def[of X] range'_def[of X f] 
            by (metis (no_types, lifting) closure_of_subtopology_subset fprops restrict_apply' subsetD)
          hence "p ∈ {m..M}" by auto
        }
        thus ?thesis by auto
      qed
      thus ?thesis by (metis e_def atLeastAtMost_iff image_subset_iff)
    qed
    ultimately have "scExtend X f ∈ C* (β X)" 
      using scT_def[of X] continuous_map_into_fulltopology fprops by auto
  }
  hence "∀ f ∈ C* X . scExtend X f ∈ C* (β X)" by auto
  thus ?thesis using assms scExtend_extends by blast
qed

lemma cstar_embedding_scEmbed:
  assumes "tych_space X"
  shows   "cstar_embedding X (β X) (scEmbed X)"
  using assms scExtend_extends_cstar[of X] dense_embedding_scEmbed[of X] 
  by meson


text ‹
 A compact Hausdorff space is its own Stone-Cech compactification
 ›

lemma scCompactification_of_compact_Hausdorff:
assumes "compact_Hausdorff X"
shows   "homeomorphic_map X (β X) (scEmbed X)"
proof -
  have dense: "dense_embedding X (β X) (scEmbed X)"
    by (simp add: assms compact_Hausdorff_imp_tych dense_embedding_scEmbed)
  moreover have closed: "closed_map X (β X) (scEmbed X)"
    by (meson T1_Spaces.continuous_imp_closed_map assms compact_Hausdorff_imp_tych 
              continuous_map_in_subtopology embedding_map_def dense
              homeomorphic_eq_everything_map scCompactification_compact_Hausdorff)
  moreover have "open_map X (β X) (scEmbed X)"
    by (metis closed closure_of_subset_eq dense_in_def embedding_imp_closed_map_eq 
              embedding_map_def homeomorphic_imp_open_map local.dense subtopology_superset)
  thus ?thesis
    by (metis closed closure_of_subset_eq dense_in_def embedding_imp_closed_map_eq 
              embedding_map_def local.dense subtopology_superset)
qed


subsection ‹
 The Stone-{\v C}ech Extension Property:
 Any continuous map from $X$ to a compact Hausdorff space $K$ extends uniquely to a continuous map
 from $\beta{X}$ to $K$.
 ›

(* a simple, but key, lemma *)
proposition gof_cstar:
  assumes "compact_Hausdorff K"
and       "continuous_map X K f"
shows     "∀ g ∈ C* K . (g o f) ∈ C* X"
proof -
  have tych_K: "tych_space K" 
    using  assms(1) compact_Hausdorff_imp_tych by auto

  { fix g assume gprops: "g ∈ C* K"
    have "continuous_map K (scT K g) g"
      using closure_subset gprops by (fastforce simp: continuous_map_in_subtopology scT_def range'_def)
    hence cts_scT: "continuous_map X (scT K g) (g o f)" 
      using assms by (simp add: continuous_map_compose)
    hence gofprops: "(g o f) ∈ (C X)"
      using scT_def[of K] range'_def[of K] 
      by (metis (mono_tags, lifting) continuous_map_in_subtopology gprops mem_Collect_eq restrict_apply')
    moreover have "fbounded (g o f) X"
    proof -
      have "compact (g ` topspace K)" using assms(1) gprops 
        using compact_space_def compactin_euclidean_iff image_compactin by blast
      hence "bounded (g ` topspace K)" 
        by (simp add: compact_imp_bounded)
      moreover have "(g o f) ` topspace X ⊆ g ` topspace K" 
        by (metis assms(2) continuous_map_image_subset_topspace image_comp image_mono)
      ultimately have "bounded ((g o f) ` topspace X)"
        by (metis bounded_subset)
      thus ?thesis using bounded_range_iff_fbounded[of "g o f" X] gofprops by auto
    qed
    ultimately have "(g o f) ∈ C* X" by auto
  }
  thus ?thesis by auto
qed

proposition scEmbed_range:
  assumes "tych_space X"
and       "x ∈ topspace X"
shows     "scEmbed X x ∈ topspace (β X)"
  using assms(1) assms(2) dense_embedding_scEmbed embedding_map_in_subtopology by fastforce

proposition scEmbed_range':
  assumes "tych_space X"
and       "x ∈ topspace X"
shows     "scEmbed X x ∈ topspace (scProduct X)"
  using assms(1) assms(2) scEmbed_range[of X] 
  by (simp add: scCompactification_def)

proposition scProjection:
  shows "∀ f ∈ C* X. ∀ p ∈ topspace (scProduct X) . scProject X f p = p f"
  using scProject_def[of X] scProduct_def[of X] product_projection[of "C* X" "scT X"]
  by simp

proposition scProjections_continuous:
  shows "∀ f ∈ C* X . continuous_map (scProduct X) (scT X f) (scProject X f)"
proof -
  have "∀ f ∈ C* X . continuous_map (scProduct X) (scT X f) (scProject X f)"
    using scProduct_def[of X] scProject_def[of X] 
    by (metis (mono_tags, lifting) projections_continuous restrict_apply')
  thus ?thesis using scCompactification_def[of X] by simp
qed

proposition continuous_embedding_inverse:
  assumes "embedding_map X Y e"
  shows "∃ e' . continuous_map (subtopology Y (e ` topspace X)) X e' ∧ (∀ x ∈ topspace X . e' (e x) = x)"
  by (meson assms embedding_map_def homeomorphic_map_maps homeomorphic_maps_def)


(* The Stone-Cech Extension Property - Proof adapted from Willard 19.5 *)
(* Every continuous map from X to K extends uniquely to \<beta> X *)

lemma scExtension_exists:
  assumes "tych_space X"
and       "compact_Hausdorff K"
shows     "∀ f ∈ cts[X,K] . ∃ F ∈ cts[β X, K] . (∀ x ∈ topspace X . F (scEmbed X x) = f x)"
proof-
  { fix f assume fprops: "f ∈ cts[X,K]"

    (* start with some basic facts that are already known to be useful in other proofs  *)
    have tych_K: "tych_space K" using assms(2) compact_Hausdorff_imp_tych[of K] by simp
  
    define Xspace where "Xspace = topspace (scProduct X)"
    define Kspace where "Kspace = topspace (scProduct K)" 
    (* Now define a map H : scProduct X \<Rightarrow> scProduct K *)
    define H where "H = (λ p ∈ Xspace . λ g ∈ C* K . scProject X (g o f) p)"

    have H_of_scEmbed: "∀ x ∈ topspace X . H (scEmbed X x) = scEmbed K (f x)"
    proof -
      { fix x assume xprops: "x ∈ topspace X"
        hence "H (scEmbed X x) = (λ p ∈ Xspace . λ g ∈ C* K . scProject X (g o f) p) (scEmbed X x)" 
          using H_def by auto
        moreover have "(scEmbed X x) ∈ Xspace" 
          using Xspace_def assms(1) scEmbed_range'[of X x] xprops by auto
        ultimately have "H (scEmbed X x) = (λ g ∈ C* K . scProject X (g o f) (scEmbed X x)) "
          by auto
        also have "… = (λ g ∈ C* K . (g o f) x)" 
          using assms(2) gof_cstar[of K X f] xprops fprops assms(1)
                scEmbed_then_project[where x="x" and X="X"]
          by (metis (no_types, lifting) mem_Collect_eq restrict_ext)
        also have "… = (λ g ∈ C* K . g (f x))" by auto
        finally have "H (scEmbed X x) = scEmbed K (f x)" 
          using scEmbed_def[of K] cstar_id_def[of K] evaluation_map_def[of K "cstar_id K" "C* K"]
          by (smt (verit) continuous_map_image_subset_topspace fprops xprops image_subset_iff 
                  mem_Collect_eq restrict_apply' restrict_ext xprops)
      }
      thus ?thesis by auto
    qed
    hence H_on_embedded: "H ` scEmbeddedCopy X ⊆ scEmbeddedCopy K"
    proof -
      { fix p assume "p ∈ H ` scEmbeddedCopy X"
        then obtain q where qprops: "q ∈ scEmbeddedCopy X ∧ p = H q" by auto
        then obtain x where xprops: "x ∈ topspace X ∧ q = scEmbed X x" 
          using scEmbeddedCopy_def[of X] by auto
        hence "p = scEmbed K (f x)" using qprops H_of_scEmbed by auto
        hence "p ∈ scEmbeddedCopy K" 
          using scEmbeddedCopy_def[of K] xprops qprops fprops 
          by (metis continuous_map_image_subset_topspace image_eqI in_mono mem_Collect_eq)
      }
      thus ?thesis by auto
    qed
      (* We'll be using:
      continuous_map_coordinatewise_then_product[of "C* K" "scProduct X" "scT K" "H"]:
          \<forall> g \<in> C* K .  continuous_map (scProduct X) (scT K g) (\<lambda>x. H x g)) \<Longrightarrow>
                        continuous_map (scProduct X) (product_topology (scT K) (C* K)) H
       *)
    (* Show that each projection of H is continuous *)
    have components_cts: "∀ g ∈ C* K . continuous_map (scProduct X) (scT K g) (λx ∈ Xspace . H x g)"
    proof -
      { fix g assume gprops: "g ∈ C* K"
        (* range described using X *)
        have "continuous_map (scProduct X) (scT X (g o f)) ( λ x ∈ Xspace . H x g)" 
        proof -
          have "∀f∈ C* X . continuous_map (scProduct X) (scT X f) (scProject X f)"
            using scProjections_continuous[of X] by simp
          hence "continuous_map (scProduct X) (scT X (g o f)) (scProject X (g o f))"
            using assms(2) fprops gprops gof_cstar[of K X f] by auto
          moreover have "∀x ∈ Xspace. H x g = (scProject X (g o f)) x"
            using gprops  H_def Xspace_def
            by auto
          ultimately show ?thesis
            using Xspace_def continuous_map_eq by fastforce
        qed
        (* need to convert to range using K *)
        moreover have "scT X (g o f) = subtopology (scT K g) (range' X (g o f))"
        proof -
          have "(g o f) ` topspace X ⊆ g ` topspace K" 
              using gprops fprops unfolding continuous_map_def by auto
          hence "range' X (g o f) ⊆ range' K g" 
            unfolding range'_def by (meson closure_of_mono)
          hence "top_of_set (range' X (g o f))
                          = subtopology (top_of_set (range' K g)) (range' X (g o f))"
            by (simp add: inf.absorb_iff2 subtopology_subtopology)
          hence "scT X (g o f) = subtopology (scT K g) (range' X (g o f))"
            using scT_def[of X] scT_def[of K] gprops assms(2) gof_cstar[of K X f] fprops by auto
          thus ?thesis by auto
        qed
        ultimately have "continuous_map (scProduct X) (scT K g) ( λ x ∈ Xspace . H x g)"
          using continuous_map_in_subtopology by auto
      }
      thus ?thesis by auto
    qed
    (* and hence H is continuous *)
    hence Hcts: "continuous_map (scProduct X) (scProduct K) H"
      using continuous_map_coordinatewise_then_product[of "C* K" "scProduct X" "scT K" "H"]
            scProduct_def[of X] scProduct_def[of K] H_def Xspace_def
      by (smt (verit, del_insts) continuous_map_eq restrict_apply)
    (* the image of \<beta>X under H is inside scEmbeddedCopy K  *)
    have H_on_beta: "H ` topspace (β X) ⊆ scEmbeddedCopy K"
    proof -
      have "H ` scEmbeddedCopy X ⊆ scEmbeddedCopy K" using H_on_embedded by auto
      hence "H ` topspace (β X) ⊆ scProduct K closure_of scEmbeddedCopy K"
        using scCompactification_def[of X] Hcts closure_of_mono 
             continuous_map_eq_image_closure_subset by fastforce
      thus ?thesis using scEmbeddedCopy_def
        by (metis assms(2) closure_of_subset_topspace homeomorphic_imp_surjective_map 
                  scCompactification_def scCompactification_of_compact_Hausdorff topspace_subtopology_subset)
    qed
    (* now obtain an inverse for scEmbed K *)
    have embeds: "dense_embedding K (β K) (scEmbed K)" using dense_embedding_scEmbed[of K] tych_K by auto
    have closed: "closedin (scProduct K) (scEmbeddedCopy K)"
      using assms(2) scEmbeddedCopy_def[of X] scCompactification_def[of K]      
            scCompactification_compact_Hausdorff[of K] 
      by (metis closure_of_eq closure_of_subset_topspace closure_of_topspace dense_in_def embeds 
                homeomorphic_map_closure_of scCompactification_of_compact_Hausdorff scEmbeddedCopy_def 
                topspace_subtopology_subset)
    hence onto: "scEmbeddedCopy K = topspace (β K)" 
      using scCompactification_def[of K]
      by (metis closure_of_closedin closure_of_subset_topspace topspace_subtopology_subset)
    then obtain e' 
      where e'props: "continuous_map (β K) K e'
                  ∧ (∀ x ∈ topspace K . e' (scEmbed K x) = x)"
         by (metis continuous_embedding_inverse embeds scEmbeddedCopy_def subtopology_topspace)
    (* ... and use it to define F. Then verify its properties *)
    define F where "F = e' o (λ p ∈ topspace (β X) . restrict H (topspace β X) p)"
    (* F is continuous *)
    have Fcts: "F ∈ cts[ β X, K ]"
    proof -
      have "(λ p ∈ topspace (β X) . restrict H (topspace β X) p) ∈ cts[β X, scProduct K]" 
        using Hcts Xspace_def continuous_map_from_subtopology scCompactification_def
        by (metis closedin_subset closedin_topspace mem_Collect_eq restrict_continuous_map)
      moreover have "H ∈ (topspace β X) → topspace (β K)"
        using Xspace_def H_on_beta Xspace_def scCompactification_def[of K] onto by blast
      ultimately have "(λ p ∈ topspace (β X) . restrict H (topspace β X) p) ∈ cts[β X, β K]"
        using scCompactification_def[of K] by (simp add: Pi_iff continuous_map_into_subtopology)
      moreover have "e' ∈ cts[ β K, K ]" using e'props by simp
      ultimately show ?thesis
        using F_def continuous_map_compose[of "β X" "β K" "(λ p ∈ topspace (β X) . restrict H (topspace β X) p)"]
        by auto
    qed
    (* F extends f *)
    moreover have Fextends: "∀ x ∈ topspace X . (F o scEmbed X) x = f x"
    proof -
      { fix x assume xprops: "x ∈ topspace X"
        have "(F o scEmbed X) x = F (scEmbed X x)" by auto
        moreover have "scEmbed X x ∈ topspace (β X)" 
          using assms(1) scEmbed_range[of X x] xprops by auto
        ultimately have "(F o scEmbed X) x
              = (e' o (λ p ∈ topspace (β X) . restrict H (topspace β X) p)) (scEmbed X x)" 
          using F_def by simp
        also have "… = (e' o (λ p ∈ topspace (β X) . H p)) (scEmbed X x)" by auto
        finally have step1: "(F o scEmbed X) x = e' ((λ p ∈ topspace (β X) . H p) (scEmbed X x))" by auto
        have "(λ p ∈ topspace (β X) . H p) (scEmbed X x) = H (scEmbed X x)"
          using scEmbed_range[of X x] assms(1) xprops by auto
        also have "… = scEmbed K (f x)" using H_of_scEmbed  xprops by auto
        finally have step2: "(λ p ∈ topspace (β X) . H p) (scEmbed X x) = scEmbed K (f x)"
          by auto        
        have "(F o scEmbed X) x = e' ((λ p ∈ topspace (β X) . H p) (scEmbed X x))"
          using step1 by simp
        also have "… = e' (scEmbed K (f x))" using step2 by auto
        finally have "(F o scEmbed X) x = f x" 
          using e'props tych_K scEmbed_range[of K "f x"] xprops fprops
          by (metis continuous_map_image_subset_topspace image_subset_iff mem_Collect_eq)
      }
      thus ?thesis by auto
    qed
    (* So F is the extension we want *)
    ultimately have "F ∈ cts[β X, K] ∧ (∀ x ∈ topspace X . F (scEmbed X x) = f x)"
      by auto
    hence "∃ F ∈ cts[β X, K] . (∀ x ∈ topspace X . F (scEmbed X x) = f x)" by auto
  }
  thus ?thesis by auto
qed

lemma scExtension_unique:
  assumes "F ∈ cts[β X, K] ∧ (∀ x ∈ topspace X . F (scEmbed X x) = f x)"
and       "compact_Hausdorff K"
shows     "(∀ G . G ∈ cts[β X, K] ∧ (∀ x ∈ topspace X . G (scEmbed X x) = f x)
                      ⟶ (∀ p ∈ topspace (β X) . F p = G p))"
proof -
  { fix G assume Gprops: "G ∈ cts[β X, K] ∧ (∀ x ∈ topspace X . G (scEmbed X x) = f x)"
    have "∀ p ∈ scEmbeddedCopy X . F p = G p"         
    proof -
      { fix p assume pprops: "p ∈ scEmbeddedCopy X"
        then obtain x where xprops: "x ∈ topspace X ∧ p = scEmbed X x"
          using scEmbeddedCopy_def[of X] by auto
        hence "F p = G p" using assms Gprops by auto
      }
      thus ?thesis by auto
    qed
    moreover have "dense_in (β X) (scEmbeddedCopy X) (topspace (β X))"
        by (metis closure_of_subset_topspace dense_in_closure dense_in_def scCompactification_def 
                  topspace_subtopology_subset)
    moreover have "(cts_on β X to_shared Hausdorff_space) {F,G}"
    proof -
      have "Hausdorff_space K" using assms(2) by auto
      moreover have "∀ g ∈ {F,G} . g ∈ cts[β X, K]"
        using assms Gprops by auto
      ultimately have "∃ K . Hausdorff_space K ∧ {F,G} ⊆ cts[β X,K]" by auto
      thus ?thesis by auto
    qed
    ultimately have "(∀ p ∈ topspace (β X) . F p = G p)"
      using continuous_maps_on_dense_subset[of F G "β X" "scEmbeddedCopy X"]
      by auto
  }
  thus ?thesis by auto
qed

lemma scExtension_property:
  assumes "tych_space X"
and       "compact_Hausdorff K"
shows     "∀ f ∈ cts[X,K] . ∃! F ∈ cts_E[β X, K] . (∀ x ∈ topspace X . F (scEmbed X x) = f x)"
proof -
  { fix f assume fprops: "f ∈ cts[X,K]"
    define P where "P = (λg . g ∈ cts_E[β X, K] ∧ (∀ x ∈ topspace X . g (scEmbed X x) = f x))"
    then obtain F where Fprops: "F ∈ cts[β X, K] ∧ (∀ x ∈ topspace X . F (scEmbed X x) = f x)"
      using scExtension_exists[of X K] assms fprops by auto 
    define F' where "F' = restrict F (topspace β X)"
    (* show that F' satisfies P *)
    have "F ∈ (topspace β X) → topspace K" using Fprops continuous_map_def[of "β X" K F] by auto
    hence F'ext: "F' ∈ (topspace β X) →_E topspace K" 
      using F'_def restrict_def[of F "topspace β X"] extensional_def[of "topspace β X"]
      by auto
    moreover have F'cts: "F' ∈ cts[ β X, K ]" 
    proof -
      have "F' ∈ (topspace β X) → topspace K" using F'ext by auto
      moreover have "∀ U . {x ∈ topspace β X. F x ∈ U} = {x ∈ topspace β X. F' x ∈ U}"
        using F'_def by auto
      ultimately show ?thesis using Fprops unfolding continuous_map_def by auto
    qed
    ultimately have "F' ∈ cts_E[ β X, K ]" by auto
    moreover have F'embed: "(∀ x ∈ topspace X . F' (scEmbed X x) = f x)"
    proof -
      have "∀ x ∈ topspace X . scEmbed X x ∈ topspace β X"
        using assms(1) scEmbed_range[of X] by blast
      thus ?thesis using F'_def Fprops by fastforce
    qed
    ultimately have "P F'" using P_def by auto
    (* now show that nothing else satisfies P *)
    moreover have "∀ G . P G ⟶ G = F'"
    proof - 
      { fix G assume Gprops: "P G"
        { fix p
          have "F' p = G p"
          proof (cases "p ∈ topspace β X")
            case True
            hence "F' ∈ cts[ β X, K] ∧ (∀x∈topspace X. F' (scEmbed X x) = f x)"
              using F'cts F'embed by auto
            moreover have "G ∈ cts[ β X, K] ∧ (∀x∈topspace X. G (scEmbed X x) = f x)"
              using Gprops P_def by auto
            ultimately show ?thesis
              using assms(2) scExtension_unique[of F' X K f] "True" by blast
          next
            case False
            hence "F' p = undefined" using F'_def by auto
            moreover have "G p = undefined" 
              using Gprops P_def extensional_def[of "topspace β X"] "False" by auto
            ultimately show ?thesis by auto
          qed
        }
        hence "∀ p . F' p = G p" by auto
      }
      thus ?thesis by auto
    qed
    ultimately have "∃! F' . P F'" by blast
    hence "∃! F ∈ cts_E[β X, K] . (∀ x ∈ topspace X . F (scEmbed X x) = f x)"
      using P_def by auto
  }
  thus ?thesis by auto
qed
(* Concludes the proof of the Stone-Cech Extension Property *)       

end