src/HOL/Analysis/Function_Topology.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69517 dc20f278e8f3 child 69566 c41954ee87cf permissions -rw-r--r--
capitalize proper names in lemma names
     1 (*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr with additions from LCP

     2     License: BSD

     3 *)

     4

     5 theory Function_Topology

     6 imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure

     7 begin

     8

     9

    10 section%important \<open>Product Topology\<close>

    11

    12 text \<open>We want to define the product topology.

    13

    14 The product topology on a product of topological spaces is generated by

    15 the sets which are products of open sets along finitely many coordinates, and the whole

    16 space along the other coordinates. This is the coarsest topology for which the projection

    17 to each factor is continuous.

    18

    19 To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type

    20 'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from 'i to 'a such that the $i$-th

    21 coordinate belongs to $X\;i$ for all $i \in I$.

    22

    23 Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.

    24 This means that type classes can not be used to define such a product if one wants to take the

    25 product of different topological spaces (as the type 'a can only be given one structure of

    26 topological space using type classes). On the other hand, one can define different topologies (as

    27 introduced in \verb+thy+) on one type, and these topologies do not need to

    28 share the same maximal open set. Hence, one can form a product of topologies in this sense, and

    29 this works well. The big caveat is that it does not interact well with the main body of

    30 topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps

    31 is not defined in this setting.

    32

    33 As the product of different topological spaces is very important in several areas of

    34 mathematics (for instance adeles), I introduce below the product topology in terms of topologies,

    35 and reformulate afterwards the consequences in terms of type classes (which are of course very

    36 handy for applications).

    37

    38 Given this limitation, it looks to me that it would be very beneficial to revamp the theory

    39 of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving

    40 type classes as consequences of more general statements in terms of topologies (but I am

    41 probably too naive here).

    42

    43 Here is an example of a reformulation using topologies. Let

    44 \begin{verbatim}

    45 continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-U \<inter> topspace(T1)))

    46                                       \<and> (f(topspace T1) \<subseteq> (topspace T2)))

    47 \end{verbatim}

    48 be the natural continuity definition of a map from the topology $T1$ to the topology $T2$. Then

    49 the current \verb+continuous_on+ (with type classes) can be redefined as

    50 \begin{verbatim}

    51 continuous_on s f = continuous_on_topo (subtopology euclidean s) (topology euclidean) f

    52 \end{verbatim}

    53

    54 In fact, I need \verb+continuous_on_topo+ to express the continuity of the projection on subfactors

    55 for the product topology, in Lemma~\verb+continuous_on_restrict_product_topology+, and I show

    56 the above equivalence in Lemma~\verb+continuous_on_continuous_on_topo+.

    57

    58 I only develop the basics of the product topology in this theory. The most important missing piece

    59 is Tychonov theorem, stating that a product of compact spaces is always compact for the product

    60 topology, even when the product is not finite (or even countable).

    61

    62 I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.

    63 \<close>

    64

    65 subsection%important \<open>Topology without type classes\<close>

    66

    67 subsubsection%important \<open>The topology generated by some (open) subsets\<close>

    68

    69 text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,

    70 as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,

    71 and is never a problem in proofs, so I prefer to write it down explicitly.

    72

    73 We do not require UNIV to be an open set, as this will not be the case in applications. (We are

    74 thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)\<close>

    75

    76 inductive generate_topology_on for S where

    77 Empty: "generate_topology_on S {}"

    78 |Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"

    79 | UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"

    80 | Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"

    81

    82 lemma%unimportant istopology_generate_topology_on:

    83   "istopology (generate_topology_on S)"

    84 unfolding istopology_def by (auto intro: generate_topology_on.intros)

    85

    86 text \<open>The basic property of the topology generated by a set $S$ is that it is the

    87 smallest topology containing all the elements of $S$:\<close>

    88

    89 lemma%unimportant generate_topology_on_coarsest:

    90   assumes "istopology T"

    91           "\<And>s. s \<in> S \<Longrightarrow> T s"

    92           "generate_topology_on S s0"

    93   shows "T s0"

    94 using assms(3) apply (induct rule: generate_topology_on.induct)

    95 using assms(1) assms(2) unfolding istopology_def by auto

    96

    97 abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"

    98   where "topology_generated_by S \<equiv> topology (generate_topology_on S)"

    99

   100 lemma%unimportant openin_topology_generated_by_iff:

   101   "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"

   102   using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp

   103

   104 lemma%unimportant openin_topology_generated_by:

   105   "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"

   106 using openin_topology_generated_by_iff by auto

   107

   108 lemma%important topology_generated_by_topspace:

   109   "topspace (topology_generated_by S) = (\<Union>S)"

   110 proof%unimportant

   111   {

   112     fix s assume "openin (topology_generated_by S) s"

   113     then have "generate_topology_on S s" by (rule openin_topology_generated_by)

   114     then have "s \<subseteq> (\<Union>S)" by (induct, auto)

   115   }

   116   then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"

   117     unfolding topspace_def by auto

   118 next

   119   have "generate_topology_on S (\<Union>S)"

   120     using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp

   121   then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"

   122     unfolding topspace_def using openin_topology_generated_by_iff by auto

   123 qed

   124

   125 lemma%important topology_generated_by_Basis:

   126   "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"

   127 by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)

   128

   129 lemma generate_topology_on_Inter:

   130   "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"

   131   by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)

   132

   133 subsection\<open>Topology bases and sub-bases\<close>

   134

   135 lemma istopology_base_alt:

   136    "istopology (arbitrary union_of P) \<longleftrightarrow>

   137     (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T

   138            \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"

   139   by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)

   140

   141 lemma istopology_base_eq:

   142    "istopology (arbitrary union_of P) \<longleftrightarrow>

   143     (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"

   144   by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)

   145

   146 lemma istopology_base:

   147    "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"

   148   by (simp add: arbitrary_def istopology_base_eq union_of_inc)

   149

   150 lemma openin_topology_base_unique:

   151    "openin X = arbitrary union_of P \<longleftrightarrow>

   152         (\<forall>V. P V \<longrightarrow> openin X V) \<and> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V. P V \<and> x \<in> V \<and> V \<subseteq> U))"

   153    (is "?lhs = ?rhs")

   154 proof

   155   assume ?lhs

   156   then show ?rhs

   157     by (auto simp: union_of_def arbitrary_def)

   158 next

   159   assume R: ?rhs

   160   then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S

   161     using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce

   162   from R show ?lhs

   163     by (fastforce simp add: union_of_def arbitrary_def intro: *)

   164 qed

   165

   166 lemma topology_base_unique:

   167    "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;

   168      \<And>U x. \<lbrakk>openin X U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. P B \<and> x \<in> B \<and> B \<subseteq> U\<rbrakk>

   169     \<Longrightarrow> topology(arbitrary union_of P) = X"

   170   by (metis openin_topology_base_unique openin_inverse [of X])

   171

   172 lemma topology_bases_eq_aux:

   173    "\<lbrakk>(arbitrary union_of P) S;

   174      \<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U\<rbrakk>

   175         \<Longrightarrow> (arbitrary union_of Q) S"

   176   by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)

   177

   178 lemma topology_bases_eq:

   179    "\<lbrakk>\<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U;

   180     \<And>V x. \<lbrakk>Q V; x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> V\<rbrakk>

   181         \<Longrightarrow> topology (arbitrary union_of P) =

   182             topology (arbitrary union_of Q)"

   183   by (fastforce intro:  arg_cong [where f=topology]  elim: topology_bases_eq_aux)

   184

   185 lemma istopology_subbase:

   186    "istopology (arbitrary union_of (finite intersection_of P relative_to S))"

   187   by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)

   188

   189 lemma openin_subbase:

   190   "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S

   191    \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"

   192   by (simp add: istopology_subbase topology_inverse')

   193

   194 lemma topspace_subbase [simp]:

   195    "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")

   196 proof

   197   show "?lhs \<subseteq> U"

   198     by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)

   199   show "U \<subseteq> ?lhs"

   200     by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase

   201               openin_subset relative_to_inc subset_UNIV topology_inverse')

   202 qed

   203

   204 lemma minimal_topology_subbase:

   205    "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;

   206      openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>

   207     \<Longrightarrow> openin X S"

   208   apply (simp add: istopology_subbase topology_inverse)

   209   apply (simp add: union_of_def intersection_of_def relative_to_def)

   210   apply (blast intro: openin_Int_Inter)

   211   done

   212

   213 lemma istopology_subbase_UNIV:

   214    "istopology (arbitrary union_of (finite intersection_of P))"

   215   by (simp add: istopology_base finite_intersection_of_Int)

   216

   217

   218 lemma generate_topology_on_eq:

   219   "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")

   220 proof (intro ext iffI)

   221   fix A

   222   assume "?lhs A"

   223   then show "?rhs A"

   224   proof induction

   225     case (Int a b)

   226     then show ?case

   227       by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)

   228   next

   229     case (UN K)

   230     then show ?case

   231       by (simp add: arbitrary_union_of_Union)

   232   next

   233     case (Basis s)

   234     then show ?case

   235       by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)

   236   qed auto

   237 next

   238   fix A

   239   assume "?rhs A"

   240   then obtain \<U> where \<U>: "\<And>T. T \<in> \<U> \<Longrightarrow> \<exists>\<F>. finite' \<F> \<and> \<F> \<subseteq> S \<and> \<Inter>\<F> = T" and eq: "A = \<Union>\<U>"

   241     unfolding union_of_def intersection_of_def by auto

   242   show "?lhs A"

   243     unfolding eq

   244   proof (rule generate_topology_on.UN)

   245     fix T

   246     assume "T \<in> \<U>"

   247     with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"

   248       by blast

   249     have "generate_topology_on S (\<Inter>\<F>)"

   250     proof (rule generate_topology_on_Inter)

   251       show "finite \<F>" "\<F> \<noteq> {}"

   252         by (auto simp: \<open>finite' \<F>\<close>)

   253       show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"

   254         by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)

   255     qed

   256     then show "generate_topology_on S T"

   257       using \<open>\<Inter>\<F> = T\<close> by blast

   258   qed

   259 qed

   260

   261 subsubsection%important \<open>Continuity\<close>

   262

   263 text \<open>We will need to deal with continuous maps in terms of topologies and not in terms

   264 of type classes, as defined below.\<close>

   265

   266 definition%important continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"

   267   where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-U \<inter> topspace(T1)))

   268                                       \<and> (f(topspace T1) \<subseteq> (topspace T2)))"

   269

   270 lemma%important continuous_on_continuous_on_topo:

   271   "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"

   272 unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def

   273 topspace_euclidean_subtopology open_openin topspace_euclidean by fast

   274

   275 lemma%unimportant continuous_on_topo_UNIV:

   276   "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"

   277 using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto

   278

   279 lemma%important continuous_on_topo_open [intro]:

   280   "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-U \<inter> topspace(T1))"

   281 unfolding%unimportant continuous_on_topo_def by auto

   282

   283 lemma%unimportant continuous_on_topo_topspace [intro]:

   284   "continuous_on_topo T1 T2 f \<Longrightarrow> f(topspace T1) \<subseteq> (topspace T2)"

   285 unfolding continuous_on_topo_def by auto

   286

   287 lemma%important continuous_on_generated_topo_iff:

   288   "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>

   289       ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-U \<inter> topspace(T1))) \<and> (f(topspace T1) \<subseteq> (\<Union> S)))"

   290 unfolding continuous_on_topo_def topology_generated_by_topspace

   291 proof%unimportant (auto simp add: topology_generated_by_Basis)

   292   assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f - U \<inter> topspace T1)"

   293   fix U assume "openin (topology_generated_by S) U"

   294   then have "generate_topology_on S U" by (rule openin_topology_generated_by)

   295   then show "openin T1 (f - U \<inter> topspace T1)"

   296   proof (induct)

   297     fix a b

   298     assume H: "openin T1 (f - a \<inter> topspace T1)" "openin T1 (f - b \<inter> topspace T1)"

   299     have "f - (a \<inter> b) \<inter> topspace T1 = (f-a \<inter> topspace T1) \<inter> (f-b \<inter> topspace T1)"

   300       by auto

   301     then show "openin T1 (f - (a \<inter> b) \<inter> topspace T1)" using H by auto

   302   next

   303     fix K

   304     assume H: "openin T1 (f - k \<inter> topspace T1)" if "k\<in> K" for k

   305     define L where "L = {f - k \<inter> topspace T1|k. k \<in> K}"

   306     have *: "openin T1 l" if "l \<in>L" for l using that H unfolding L_def by auto

   307     have "openin T1 (\<Union>L)" using openin_Union[OF *] by simp

   308     moreover have "(\<Union>L) = (f - \<Union>K \<inter> topspace T1)" unfolding L_def by auto

   309     ultimately show "openin T1 (f - \<Union>K \<inter> topspace T1)" by simp

   310   qed (auto simp add: H)

   311 qed

   312

   313 lemma%important continuous_on_generated_topo:

   314   assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-U \<inter> topspace(T1))"

   315           "f(topspace T1) \<subseteq> (\<Union> S)"

   316   shows "continuous_on_topo T1 (topology_generated_by S) f"

   317 using%unimportant assms continuous_on_generated_topo_iff by blast

   318

   319 lemma%important continuous_on_topo_compose:

   320   assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"

   321   shows "continuous_on_topo T1 T3 (g o f)"

   322 using%unimportant assms unfolding continuous_on_topo_def

   323 proof%unimportant (auto)

   324   fix U :: "'c set"

   325   assume H: "openin T3 U"

   326   have "openin T1 (f - (g - U \<inter> topspace T2) \<inter> topspace T1)"

   327     using H assms by blast

   328   moreover have "f - (g - U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) - U \<inter> topspace T1"

   329     using H assms continuous_on_topo_topspace by fastforce

   330   ultimately show "openin T1 ((g \<circ> f) - U \<inter> topspace T1)"

   331     by simp

   332 qed (blast)

   333

   334 lemma%unimportant continuous_on_topo_preimage_topspace [intro]:

   335   assumes "continuous_on_topo T1 T2 f"

   336   shows "f-(topspace T2) \<inter> topspace T1 = topspace T1"

   337 using assms unfolding continuous_on_topo_def by auto

   338

   339

   340 subsubsection%important \<open>Pullback topology\<close>

   341

   342 text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is

   343 a special case of this notion, pulling back by the identity. We introduce the general notion as

   344 we will need it to define the strong operator topology on the space of continuous linear operators,

   345 by pulling back the product topology on the space of all functions.\<close>

   346

   347 text \<open>\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on

   348 the set $A$.\<close>

   349

   350 definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"

   351   where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-U \<inter> A)"

   352

   353 lemma%important istopology_pullback_topology:

   354   "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-U \<inter> A)"

   355 unfolding%unimportant istopology_def proof (auto)

   356   fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f - U \<inter> A"

   357   then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-(U S) \<inter> A"

   358     by (rule bchoice)

   359   then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-(U S) \<inter> A"

   360     by blast

   361   define V where "V = (\<Union>S\<in>K. U S)"

   362   have "openin T V" "\<Union>K = f - V \<inter> A" unfolding V_def using U by auto

   363   then show "\<exists>V. openin T V \<and> \<Union>K = f - V \<inter> A" by auto

   364 qed

   365

   366 lemma%unimportant openin_pullback_topology:

   367   "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-U \<inter> A)"

   368 unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto

   369

   370 lemma%unimportant topspace_pullback_topology:

   371   "topspace (pullback_topology A f T) = f-(topspace T) \<inter> A"

   372 by (auto simp add: topspace_def openin_pullback_topology)

   373

   374 lemma%important continuous_on_topo_pullback [intro]:

   375   assumes "continuous_on_topo T1 T2 g"

   376   shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"

   377 unfolding continuous_on_topo_def

   378 proof%unimportant (auto)

   379   fix U::"'b set" assume "openin T2 U"

   380   then have "openin T1 (g-U \<inter> topspace T1)"

   381     using assms unfolding continuous_on_topo_def by auto

   382   have "(g o f)-U \<inter> topspace (pullback_topology A f T1) = (g o f)-U \<inter> A \<inter> f-(topspace T1)"

   383     unfolding topspace_pullback_topology by auto

   384   also have "... = f-(g-U \<inter> topspace T1) \<inter> A "

   385     by auto

   386   also have "openin (pullback_topology A f T1) (...)"

   387     unfolding openin_pullback_topology using \<open>openin T1 (g-U \<inter> topspace T1)\<close> by auto

   388   finally show "openin (pullback_topology A f T1) ((g \<circ> f) - U \<inter> topspace (pullback_topology A f T1))"

   389     by auto

   390 next

   391   fix x assume "x \<in> topspace (pullback_topology A f T1)"

   392   then have "f x \<in> topspace T1"

   393     unfolding topspace_pullback_topology by auto

   394   then show "g (f x) \<in> topspace T2"

   395     using assms unfolding continuous_on_topo_def by auto

   396 qed

   397

   398 lemma%important continuous_on_topo_pullback' [intro]:

   399   assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-A"

   400   shows "continuous_on_topo T1 (pullback_topology A f T2) g"

   401 unfolding continuous_on_topo_def

   402 proof%unimportant (auto)

   403   fix U assume "openin (pullback_topology A f T2) U"

   404   then have "\<exists>V. openin T2 V \<and> U = f-V \<inter> A"

   405     unfolding openin_pullback_topology by auto

   406   then obtain V where "openin T2 V" "U = f-V \<inter> A"

   407     by blast

   408   then have "g - U \<inter> topspace T1 = g-(f-V \<inter> A) \<inter> topspace T1"

   409     by blast

   410   also have "... = (f o g)-V \<inter> (g-A \<inter> topspace T1)"

   411     by auto

   412   also have "... = (f o g)-V \<inter> topspace T1"

   413     using assms(2) by auto

   414   also have "openin T1 (...)"

   415     using assms(1) \<open>openin T2 V\<close> by auto

   416   finally show "openin T1 (g - U \<inter> topspace T1)" by simp

   417 next

   418   fix x assume "x \<in> topspace T1"

   419   have "(f o g) x \<in> topspace T2"

   420     using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto

   421   then have "g x \<in> f-(topspace T2)"

   422     unfolding comp_def by blast

   423   moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast

   424   ultimately show "g x \<in> topspace (pullback_topology A f T2)"

   425     unfolding topspace_pullback_topology by blast

   426 qed

   427

   428

   429 subsection%important \<open>The product topology\<close>

   430

   431 text \<open>We can now define the product topology, as generated by

   432 the sets which are products of open sets along finitely many coordinates, and the whole

   433 space along the other coordinates. Equivalently, it is generated by sets which are one open

   434 set along one single coordinate, and the whole space along other coordinates. In fact, this is only

   435 equivalent for nonempty products, but for the empty product the first formulation is better

   436 (the second one gives an empty product space, while an empty product should have exactly one

   437 point, equal to \verb+undefined+ along all coordinates.

   438

   439 So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.

   440 \<close>

   441

   442 definition%important product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"

   443   where "product_topology T I =

   444     topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"

   445

   446 text \<open>The total set of the product topology is the product of the total sets

   447 along each coordinate.\<close>

   448

   449 proposition product_topology:

   450   "product_topology X I =

   451    topology

   452     (arbitrary union_of

   453        ((finite intersection_of

   454         (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))

   455         relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"

   456   (is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")

   457 proof -

   458   let ?\<Omega> = "(\<lambda>F. \<exists>Y. F = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)})"

   459   have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A

   460   proof -

   461     have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"

   462       if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>

   463     proof -

   464       have "\<forall>U \<in> \<U>. \<exists>Y. U = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}"

   465         using \<U> by auto

   466       then obtain Y where Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = Pi\<^sub>E I (Y U) \<and> (\<forall>i. openin (X i) (Y U i)) \<and> finite {i. (Y U) i \<noteq> topspace (X i)}"

   467         by metis

   468       obtain U where "U \<in> \<U>"

   469         using \<open>\<U> \<noteq> {}\<close> by blast

   470       let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i})  {i \<in> I. Y U i \<noteq> topspace (X i)}"

   471       show ?thesis

   472       proof (intro conjI exI)

   473         show "finite (\<Union>U\<in>\<U>. ?F U)"

   474           using Y \<open>finite' \<U>\<close> by auto

   475         show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"

   476         proof

   477           have *: "f \<in> U"

   478             if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"

   479               and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U

   480           proof -

   481             have "Pi\<^sub>E I (Y U) = U"

   482               using Y \<open>U \<in> \<U>\<close> by blast

   483             then show "f \<in> U"

   484               using that unfolding PiE_def Pi_def by blast

   485           qed

   486           show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"

   487             by (auto simp: PiE_iff *)

   488           show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"

   489             using Y openin_subset \<open>finite' \<U>\<close> by fastforce

   490         qed

   491       qed (use Y openin_subset in \<open>blast+\<close>)

   492     qed

   493     have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"

   494       if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>

   495     proof (cases "\<U>={}")

   496       case True

   497       then show ?thesis

   498         apply (rule_tac x="{?TOP}" in exI, simp)

   499         apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)

   500         apply force

   501         done

   502     next

   503       case False

   504       then obtain U where "U \<in> \<U>"

   505         by blast

   506       have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"

   507         using \<U> by auto

   508       then obtain J Y where

   509         Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = {f. f (J U) \<in> Y U} \<and> J U \<in> I \<and> openin (X (J U)) (Y U)"

   510         by metis

   511       let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"

   512       show ?thesis

   513       proof (intro conjI exI)

   514         show "finite (?G  \<U>)" "?G  \<U> \<noteq> {}"

   515           using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+

   516         have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"

   517           using Y by force

   518         show "?G  \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"

   519           apply clarsimp

   520           apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)

   521           apply (auto simp: *)

   522           done

   523       next

   524         show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"

   525         proof

   526           have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"

   527             apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)

   528             using Y \<open>U \<in> \<U>\<close> openin_subset by blast+

   529           then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"

   530             using \<open>U \<in> \<U>\<close>

   531             by fastforce

   532           moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"

   533             using PiE_mem Y by fastforce

   534           ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"

   535             by auto

   536         qed (use Y in fastforce)

   537       qed

   538     qed

   539     show ?thesis

   540       unfolding relative_to_def intersection_of_def

   541       by (safe; blast dest!: 1 2)

   542   qed

   543   show ?thesis

   544     unfolding product_topology_def generate_topology_on_eq

   545     apply (rule arg_cong [where f = topology])

   546     apply (rule arg_cong [where f = "(union_of)arbitrary"])

   547     apply (force simp: *)

   548     done

   549 qed

   550

   551 lemma%important topspace_product_topology:

   552   "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"

   553 proof%unimportant

   554   show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"

   555     unfolding product_topology_def topology_generated_by_topspace

   556     unfolding topspace_def by auto

   557   have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"

   558     using openin_topspace not_finite_existsD by auto

   559   then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"

   560     unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)

   561 qed

   562

   563 lemma%unimportant product_topology_basis:

   564   assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"

   565   shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"

   566   unfolding product_topology_def

   567   by (rule topology_generated_by_Basis) (use assms in auto)

   568

   569 lemma%important product_topology_open_contains_basis:

   570   assumes "openin (product_topology T I) U" "x \<in> U"

   571   shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"

   572 proof%unimportant -

   573   have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"

   574     using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto

   575   then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"

   576   proof induction

   577     case (Int U V x)

   578     then obtain XU XV where H:

   579       "x \<in> Pi\<^sub>E I XU" "(\<forall>i. openin (T i) (XU i))" "finite {i. XU i \<noteq> topspace (T i)}" "Pi\<^sub>E I XU \<subseteq> U"

   580       "x \<in> Pi\<^sub>E I XV" "(\<forall>i. openin (T i) (XV i))" "finite {i. XV i \<noteq> topspace (T i)}" "Pi\<^sub>E I XV \<subseteq> V"

   581       by auto meson

   582     define X where "X = (\<lambda>i. XU i \<inter> XV i)"

   583     have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"

   584       unfolding X_def by (auto simp add: PiE_iff)

   585     then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto

   586     moreover have "\<forall>i. openin (T i) (X i)"

   587       unfolding X_def using H by auto

   588     moreover have "finite {i. X i \<noteq> topspace (T i)}"

   589       apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])

   590       unfolding X_def using H by auto

   591     moreover have "x \<in> Pi\<^sub>E I X"

   592       unfolding X_def using H by auto

   593     ultimately show ?case

   594       by auto

   595   next

   596     case (UN K x)

   597     then obtain k where "k \<in> K" "x \<in> k" by auto

   598     with UN have "\<exists>X. x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"

   599       by simp

   600     then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"

   601       by blast

   602     then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"

   603       using \<open>k \<in> K\<close> by auto

   604     then show ?case

   605       by auto

   606   qed auto

   607   then show ?thesis using \<open>x \<in> U\<close> by auto

   608 qed

   609

   610

   611 lemma openin_product_topology:

   612    "openin (product_topology X I) =

   613     arbitrary union_of

   614           ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))

   615            relative_to topspace (product_topology X I))"

   616   apply (subst product_topology)

   617   apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])

   618   done

   619

   620 lemma subtopology_PiE:

   621   "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"

   622 proof -

   623   let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"

   624   let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"

   625   have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =

   626         finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"

   627     by (rule finite_intersection_of_relative_to)

   628   also have "\<dots> = finite intersection_of

   629                       ((\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)

   630                        relative_to ?X \<inter> Pi\<^sub>E I S)

   631                    relative_to ?X \<inter> Pi\<^sub>E I S"

   632     apply (rule arg_cong2 [where f = "(relative_to)"])

   633      apply (rule arg_cong [where f = "(intersection_of)finite"])

   634      apply (rule ext)

   635      apply (auto simp: relative_to_def intersection_of_def)

   636     done

   637   finally

   638   have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =

   639         finite intersection_of

   640           (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)

   641           relative_to ?X \<inter> Pi\<^sub>E I S"

   642     by (metis finite_intersection_of_relative_to)

   643   then show ?thesis

   644   unfolding topology_eq

   645   apply clarify

   646   apply (simp add: openin_product_topology flip: openin_relative_to)

   647   apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)

   648   done

   649 qed

   650

   651

   652 lemma product_topology_base_alt:

   653    "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))

   654     relative_to topspace(product_topology X I) =

   655     (\<lambda>F. (\<exists>U. F =  Pi\<^sub>E I U \<and> finite {i \<in> I. U i \<noteq> topspace(X i)} \<and> (\<forall>i \<in> I. openin (X i) (U i))))"

   656    (is "?lhs = ?rhs")

   657 proof -

   658   have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"

   659     unfolding all_relative_to all_intersection_of topspace_product_topology

   660   proof clarify

   661     fix \<F>

   662     assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"

   663     then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U \<and>

   664           finite {i \<in> I. U i \<noteq> topspace (X i)} \<and> (\<forall>i\<in>I. openin (X i) (U i))"

   665     proof (induction)

   666       case (insert F \<F>)

   667       then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"

   668         and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"

   669         and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"

   670         by auto

   671       obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"

   672         using insert by auto

   673       let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"

   674       show ?case

   675       proof (intro exI conjI)

   676         show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"

   677         using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce

   678       next

   679         show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"

   680           by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto

   681       next

   682         show "\<forall>i\<in>I. openin (X i) (?U i)"

   683           by (simp add: \<open>openin (X i) V\<close> ope openin_Int)

   684       qed

   685     qed (auto intro: dest: not_finite_existsD)

   686   qed

   687   moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"

   688   proof clarify

   689     fix U :: "'a \<Rightarrow> 'b set"

   690     assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"

   691     let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"

   692     show "?lhs (Pi\<^sub>E I U)"

   693       unfolding relative_to_def topspace_product_topology

   694     proof (intro exI conjI)

   695       show "(finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)) ?U"

   696         using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto

   697       show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"

   698         using ope openin_subset by fastforce

   699     qed

   700   qed

   701   ultimately show ?thesis

   702     by meson

   703 qed

   704

   705

   706 lemma topspace_product_topology_alt:

   707    "topspace (product_topology Y I) = {f \<in> extensional I. \<forall>k \<in> I. f k \<in> topspace(Y k)}"

   708   by (force simp: product_topology PiE_def)

   709

   710 lemma openin_product_topology_alt:

   711   "openin (product_topology X I) S \<longleftrightarrow>

   712     (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>

   713                  (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"

   714   apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto)

   715   apply (drule bspec; blast)

   716   done

   717

   718

   719 text \<open>The basic property of the product topology is the continuity of projections:\<close>

   720

   721 lemma%unimportant continuous_on_topo_product_coordinates [simp]:

   722   assumes "i \<in> I"

   723   shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"

   724 proof -

   725   {

   726     fix U assume "openin (T i) U"

   727     define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"

   728     then have *: "(\<lambda>x. x i) - U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)) = (\<Pi>\<^sub>E j\<in>I. X j)"

   729       unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]

   730       by (auto simp add: PiE_iff, auto, metis subsetCE)

   731     have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"

   732       unfolding X_def using \<open>openin (T i) U\<close> by auto

   733     have "openin (product_topology T I) ((\<lambda>x. x i) - U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"

   734       unfolding product_topology_def

   735       apply (rule topology_generated_by_Basis)

   736       apply (subst *)

   737       using ** by auto

   738   }

   739   then show ?thesis unfolding continuous_on_topo_def

   740     by (auto simp add: assms topspace_product_topology PiE_iff)

   741 qed

   742

   743 lemma%important continuous_on_topo_coordinatewise_then_product [intro]:

   744   assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"

   745           "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"

   746   shows "continuous_on_topo T1 (product_topology T I) f"

   747 unfolding product_topology_def

   748 proof%unimportant (rule continuous_on_generated_topo)

   749   fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"

   750   then obtain X where H: "U = Pi\<^sub>E I X" "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"

   751     by blast

   752   define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"

   753   have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto

   754   have "(\<lambda>x. f x i)-(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i

   755     using that assms(1) by (simp add: continuous_on_topo_preimage_topspace)

   756   then have *: "(\<lambda>x. f x i)-(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i

   757     using that unfolding J_def by auto

   758   have "f-U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-(X i) \<inter> topspace T1) \<inter> (topspace T1)"

   759     by (subst H(1), auto simp add: PiE_iff assms)

   760   also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-(X i) \<inter> topspace T1) \<inter> (topspace T1)"

   761     using * \<open>J \<subseteq> I\<close> by auto

   762   also have "openin T1 (...)"

   763     apply (rule openin_INT)

   764     apply (simp add: \<open>finite J\<close>)

   765     using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto

   766   ultimately show "openin T1 (f-U \<inter> topspace T1)" by simp

   767 next

   768   show "f topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"

   769     apply (subst topology_generated_by_topspace[symmetric])

   770     apply (subst product_topology_def[symmetric])

   771     apply (simp only: topspace_product_topology)

   772     apply (auto simp add: PiE_iff)

   773     using assms unfolding continuous_on_topo_def by auto

   774 qed

   775

   776 lemma%unimportant continuous_on_topo_product_then_coordinatewise [intro]:

   777   assumes "continuous_on_topo T1 (product_topology T I) f"

   778   shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"

   779         "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"

   780 proof -

   781   fix i assume "i \<in> I"

   782   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto

   783   also have "continuous_on_topo T1 (T i) (...)"

   784     apply (rule continuous_on_topo_compose[of _ "product_topology T I"])

   785     using assms \<open>i \<in> I\<close> by auto

   786   ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"

   787     by simp

   788 next

   789   fix i x assume "i \<notin> I" "x \<in> topspace T1"

   790   have "f x \<in> topspace (product_topology T I)"

   791     using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto

   792   then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"

   793     using topspace_product_topology by metis

   794   then show "f x i = undefined"

   795     using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)

   796 qed

   797

   798 lemma%unimportant continuous_on_restrict:

   799   assumes "J \<subseteq> I"

   800   shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"

   801 proof (rule continuous_on_topo_coordinatewise_then_product)

   802   fix i assume "i \<in> J"

   803   then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto

   804   then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"

   805     using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto

   806 next

   807   fix i assume "i \<notin> J"

   808   then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"

   809     unfolding restrict_def by auto

   810 qed

   811

   812

   813 subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>

   814

   815 instantiation "fun" :: (type, topological_space) topological_space

   816 begin

   817

   818 definition%important open_fun_def:

   819   "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"

   820

   821 instance proof%unimportant

   822   have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"

   823     unfolding topspace_product_topology topspace_euclidean by auto

   824   then show "open (UNIV::('a \<Rightarrow> 'b) set)"

   825     unfolding open_fun_def by (metis openin_topspace)

   826 qed (auto simp add: open_fun_def)

   827

   828 end

   829

   830 lemma%unimportant euclidean_product_topology:

   831   "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"

   832 by (metis open_openin topology_eq open_fun_def)

   833

   834 lemma%important product_topology_basis':

   835   fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"

   836   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"

   837   shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"

   838 proof%unimportant -

   839   define J where "J = xI"

   840   define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"

   841   define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"

   842   have *: "open (X i)" for i

   843     unfolding X_def V_def using assms by auto

   844   have **: "finite {i. X i \<noteq> UNIV}"

   845     unfolding X_def V_def J_def using assms(1) by auto

   846   have "open (Pi\<^sub>E UNIV X)"

   847     unfolding open_fun_def apply (rule product_topology_basis)

   848     using * ** unfolding open_openin topspace_euclidean by auto

   849   moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"

   850     apply (auto simp add: PiE_iff) unfolding X_def V_def J_def

   851     proof (auto)

   852       fix f :: "'a \<Rightarrow> 'b" and i :: 'i

   853       assume a1: "i \<in> I"

   854       assume a2: "\<forall>i. f i \<in> (if i \<in> xI then if i \<in> xI then \<Inter>{U ia |ia. ia \<in> I \<and> x ia = i} else UNIV else UNIV)"

   855       have f3: "x i \<in> xI"

   856         using a1 by blast

   857       have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"

   858         using a1 by blast

   859       then show "f (x i) \<in> U i"

   860         using f3 a2 by (meson Inter_iff)

   861     qed

   862   ultimately show ?thesis by simp

   863 qed

   864

   865 text \<open>The results proved in the general situation of products of possibly different

   866 spaces have their counterparts in this simpler setting.\<close>

   867

   868 lemma%unimportant continuous_on_product_coordinates [simp]:

   869   "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"

   870 unfolding continuous_on_topo_UNIV euclidean_product_topology

   871 by (rule continuous_on_topo_product_coordinates, simp)

   872

   873 lemma%unimportant continuous_on_coordinatewise_then_product [intro, continuous_intros]:

   874   assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"

   875   shows "continuous_on UNIV f"

   876 using assms unfolding continuous_on_topo_UNIV euclidean_product_topology

   877 by (rule continuous_on_topo_coordinatewise_then_product, simp)

   878

   879 lemma%unimportant continuous_on_product_then_coordinatewise:

   880   assumes "continuous_on UNIV f"

   881   shows "continuous_on UNIV (\<lambda>x. f x i)"

   882 using assms unfolding continuous_on_topo_UNIV euclidean_product_topology

   883 by (rule continuous_on_topo_product_then_coordinatewise(1), simp)

   884

   885 lemma%unimportant continuous_on_product_coordinatewise_iff:

   886   "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"

   887 by (auto intro: continuous_on_product_then_coordinatewise)

   888

   889 subsubsection%important \<open>Topological countability for product spaces\<close>

   890

   891 text \<open>The next two lemmas are useful to prove first or second countability

   892 of product spaces, but they have more to do with countability and could

   893 be put in the corresponding theory.\<close>

   894

   895 lemma%unimportant countable_nat_product_event_const:

   896   fixes F::"'a set" and a::'a

   897   assumes "a \<in> F" "countable F"

   898   shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"

   899 proof -

   900   have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}

   901                   \<subseteq> (\<Union>N. {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)})"

   902     using infinite_nat_iff_unbounded_le by fastforce

   903   have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat

   904   proof (induction N)

   905     case 0

   906     have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"

   907       using \<open>a \<in> F\<close> by auto

   908     then show ?case by auto

   909   next

   910     case (Suc N)

   911     define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"

   912       where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"

   913     have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>Suc N. x i = a)} \<subseteq> f({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"

   914     proof (auto)

   915       fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"

   916       define y where "y = (\<lambda>i. if i = N then a else x i)"

   917       have "f (y, x N) = x"

   918         unfolding f_def y_def by auto

   919       moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"

   920         unfolding y_def using H \<open>a \<in> F\<close> by auto

   921       ultimately show "x \<in> f({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"

   922         by (metis (no_types, lifting) image_eqI)

   923     qed

   924     moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"

   925       using Suc.IH assms(2) by auto

   926     ultimately show ?case

   927       by (meson countable_image countable_subset)

   928   qed

   929   then show ?thesis using countable_subset[OF *] by auto

   930 qed

   931

   932 lemma%unimportant countable_product_event_const:

   933   fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b

   934   assumes "\<And>i. countable (F i)"

   935   shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"

   936 proof -

   937   define G where "G = (\<Union>i. F i) \<union> {b}"

   938   have "countable G" unfolding G_def using assms by auto

   939   have "b \<in> G" unfolding G_def by auto

   940   define pi where "pi = (\<lambda>(x::(nat \<Rightarrow> 'b)). (\<lambda> i::'a. x ((to_nat::('a \<Rightarrow> nat)) i)))"

   941   have "{f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}

   942         \<subseteq> pi{g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"

   943   proof (auto)

   944     fix f assume H: "\<forall>i. f i \<in> F i" "finite {i. f i \<noteq> b}"

   945     define I where "I = {i. f i \<noteq> b}"

   946     define g where "g = (\<lambda>j. if j \<in> to_natI then f (from_nat j) else b)"

   947     have "{j. g j \<noteq> b} \<subseteq> to_natI" unfolding g_def by auto

   948     then have "finite {j. g j \<noteq> b}"

   949       unfolding I_def using H(2) using finite_surj by blast

   950     moreover have "g j \<in> G" for j

   951       unfolding g_def G_def using H by auto

   952     ultimately have "g \<in> {g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"

   953       by auto

   954     moreover have "f = pi g"

   955       unfolding pi_def g_def I_def using H by fastforce

   956     ultimately show "f \<in> pi{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"

   957       by auto

   958   qed

   959   then show ?thesis

   960     using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]

   961     by (meson countable_image countable_subset)

   962 qed

   963

   964 instance "fun" :: (countable, first_countable_topology) first_countable_topology

   965 proof%unimportant

   966   fix x::"'a \<Rightarrow> 'b"

   967   have "\<exists>A::('b \<Rightarrow> nat \<Rightarrow> 'b set). \<forall>x. (\<forall>i. x \<in> A x i \<and> open (A x i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A x i \<subseteq> S))"

   968     apply (rule choice) using first_countable_basis by auto

   969   then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"

   970                                                   "\<And>x i. open (A x i)"

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

   972     by metis

   973   text \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>

   974   define B where "B = (\<lambda>i. (A (x i))UNIV \<union> {UNIV})"

   975   have "countable (B i)" for i unfolding B_def by auto

   976

   977   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"

   978   have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"

   979     unfolding K_def B_def by auto

   980   then have "K \<noteq> {}" by auto

   981   have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"

   982     apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto

   983   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X){X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"

   984     unfolding K_def by auto

   985   ultimately have "countable K" by auto

   986   have "x \<in> k" if "k \<in> K" for k

   987     using that unfolding K_def B_def apply auto using A(1) by auto

   988   have "open k" if "k \<in> K" for k

   989     using that unfolding open_fun_def K_def B_def apply (auto)

   990     apply (rule product_topology_basis)

   991     unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))

   992

   993   have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U

   994   proof -

   995     have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"

   996       using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto

   997     with product_topology_open_contains_basis[OF this]

   998     have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"

   999       unfolding topspace_euclidean open_openin by simp

  1000     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"

  1001                            "\<And>i. open (X i)"

  1002                            "finite {i. X i \<noteq> UNIV}"

  1003                            "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"

  1004       by auto

  1005     define I where "I = {i. X i \<noteq> UNIV}"

  1006     define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B i \<and> y \<subseteq> X i) else UNIV)"

  1007     have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i

  1008       unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)

  1009     have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i

  1010       apply (cases "i \<in> I")

  1011       unfolding Y_def using * that apply (auto)

  1012       apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)

  1013       unfolding B_def apply simp

  1014       unfolding I_def apply auto

  1015       done

  1016     have "{i. Y i \<noteq> UNIV} \<subseteq> I"

  1017       unfolding Y_def by auto

  1018     then have ***: "finite {i. Y i \<noteq> UNIV}"

  1019       unfolding I_def using H(3) rev_finite_subset by blast

  1020     have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"

  1021       using ** *** by auto

  1022     then have "Pi\<^sub>E UNIV Y \<in> K"

  1023       unfolding K_def by auto

  1024

  1025     have "Y i \<subseteq> X i" for i

  1026       apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto

  1027     then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto

  1028     then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto

  1029     then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto

  1030   qed

  1031

  1032   show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"

  1033     apply (rule first_countableI[of K])

  1034     using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto

  1035 qed

  1036

  1037 lemma%important product_topology_countable_basis:

  1038   shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).

  1039           topological_basis K \<and> countable K \<and>

  1040           (\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"

  1041 proof%unimportant -

  1042   obtain B::"'b set set" where B: "countable B \<and> topological_basis B"

  1043     using ex_countable_basis by auto

  1044   then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)

  1045   define B2 where "B2 = B \<union> {UNIV}"

  1046   have "countable B2"

  1047     unfolding B2_def using B by auto

  1048   have "open U" if "U \<in> B2" for U

  1049     using that unfolding B2_def using B topological_basis_open by auto

  1050

  1051   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"

  1052   have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"

  1053     unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto

  1054

  1055   have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"

  1056     apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto

  1057   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X){X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"

  1058     unfolding K_def by auto

  1059   ultimately have ii: "countable K" by auto

  1060

  1061   have iii: "topological_basis K"

  1062   proof (rule topological_basisI)

  1063     fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"

  1064     then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"

  1065       unfolding open_fun_def by auto

  1066     with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]

  1067     have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"

  1068       unfolding topspace_euclidean open_openin by simp

  1069     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"

  1070                            "\<And>i. open (X i)"

  1071                            "finite {i. X i \<noteq> UNIV}"

  1072                            "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"

  1073       by auto

  1074     then have "x i \<in> X i" for i by auto

  1075     define I where "I = {i. X i \<noteq> UNIV}"

  1076     define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y) else UNIV)"

  1077     have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i

  1078       unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)

  1079     have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i

  1080       using someI_ex[OF *]

  1081       apply (cases "i \<in> I")

  1082       unfolding Y_def using * apply (auto)

  1083       unfolding B2_def I_def by auto

  1084     have "{i. Y i \<noteq> UNIV} \<subseteq> I"

  1085       unfolding Y_def by auto

  1086     then have ***: "finite {i. Y i \<noteq> UNIV}"

  1087       unfolding I_def using H(3) rev_finite_subset by blast

  1088     have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"

  1089       using ** *** by auto

  1090     then have "Pi\<^sub>E UNIV Y \<in> K"

  1091       unfolding K_def by auto

  1092

  1093     have "Y i \<subseteq> X i" for i

  1094       apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto

  1095     then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto

  1096     then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto

  1097

  1098     have "x \<in> Pi\<^sub>E UNIV Y"

  1099       using ** by auto

  1100

  1101     show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"

  1102       using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto

  1103   next

  1104     fix U assume "U \<in> K"

  1105     show "open U"

  1106       using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)

  1107       apply (rule product_topology_basis)

  1108       using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV unfolding topspace_euclidean open_openin[symmetric]

  1109       by auto

  1110   qed

  1111

  1112   show ?thesis using i ii iii by auto

  1113 qed

  1114

  1115 instance "fun" :: (countable, second_countable_topology) second_countable_topology

  1116   apply standard

  1117   using product_topology_countable_basis topological_basis_imp_subbasis by auto

  1118

  1119

  1120 subsection%important \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)

  1121

  1122 text \<open>Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous

  1123 operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology

  1124 (the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).

  1125

  1126 However, there is another topology on this space, the strong operator topology, where $T_n$ tends to

  1127 $T$ iff, for all $x$ in 'a, then $T_n x$ tends to $T x$. This is precisely the product topology

  1128 where the target space is endowed with the norm topology. It is especially useful when 'b is the set

  1129 of real numbers, since then this topology is compact.

  1130

  1131 We can not implement it using type classes as there is already a topology, but at least we

  1132 can define it as a topology.

  1133

  1134 Note that there is yet another (common and useful) topology on operator spaces, the weak operator

  1135 topology, defined analogously using the product topology, but where the target space is given the

  1136 weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the

  1137 canonical embedding of a space into its bidual. We do not define it there, although it could also be

  1138 defined analogously.

  1139 \<close>

  1140

  1141 definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"

  1142 where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"

  1143

  1144 lemma%unimportant strong_operator_topology_topspace:

  1145   "topspace strong_operator_topology = UNIV"

  1146 unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto

  1147

  1148 lemma%important strong_operator_topology_basis:

  1149   fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"

  1150   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"

  1151   shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"

  1152 proof%unimportant -

  1153   have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"

  1154     by (rule product_topology_basis'[OF assms])

  1155   moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}

  1156                 = blinfun_apply-{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"

  1157     by auto

  1158   ultimately show ?thesis

  1159     unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto

  1160 qed

  1161

  1162 lemma%important strong_operator_topology_continuous_evaluation:

  1163   "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"

  1164 proof%unimportant -

  1165   have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"

  1166     unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)

  1167     using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce

  1168   then show ?thesis unfolding comp_def by simp

  1169 qed

  1170

  1171 lemma%unimportant continuous_on_strong_operator_topo_iff_coordinatewise:

  1172   "continuous_on_topo T strong_operator_topology f

  1173     \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"

  1174 proof (auto)

  1175   fix x::"'b"

  1176   assume "continuous_on_topo T strong_operator_topology f"

  1177   with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]

  1178   have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"

  1179     by simp

  1180   then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"

  1181     unfolding comp_def by auto

  1182 next

  1183   assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"

  1184   have "continuous_on_topo T euclidean (blinfun_apply o f)"

  1185     unfolding euclidean_product_topology

  1186     apply (rule continuous_on_topo_coordinatewise_then_product, auto)

  1187     using * unfolding comp_def by auto

  1188   show "continuous_on_topo T strong_operator_topology f"

  1189     unfolding strong_operator_topology_def

  1190     apply (rule continuous_on_topo_pullback')

  1191     by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)

  1192 qed

  1193

  1194 lemma%important strong_operator_topology_weaker_than_euclidean:

  1195   "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"

  1196 by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise,

  1197     auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)

  1198

  1199

  1200 subsection%important \<open>Metrics on product spaces\<close>

  1201

  1202

  1203 text \<open>In general, the product topology is not metrizable, unless the index set is countable.

  1204 When the index set is countable, essentially any (convergent) combination of the metrics on the

  1205 factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,

  1206 for instance.

  1207

  1208 What is not completely trivial is that the distance thus defined induces the same topology

  1209 as the product topology. This is what we have to prove to show that we have an instance

  1210 of \verb+metric_space+.

  1211

  1212 The proofs below would work verbatim for general countable products of metric spaces. However,

  1213 since distances are only implemented in terms of type classes, we only develop the theory

  1214 for countable products of the same space.\<close>

  1215

  1216 instantiation "fun" :: (countable, metric_space) metric_space

  1217 begin

  1218

  1219 definition%important dist_fun_def:

  1220   "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"

  1221

  1222 definition%important uniformity_fun_def:

  1223   "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"

  1224

  1225 text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the

  1226 instance: once it is proved, they become trivial consequences of the general theory of metric

  1227 spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how

  1228 to do this.\<close>

  1229

  1230 lemma%important dist_fun_le_dist_first_terms:

  1231   "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"

  1232 proof%unimportant -

  1233   have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)

  1234           = (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"

  1235     by (rule suminf_cong, simp add: power_add)

  1236   also have "... = (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)"

  1237     apply (rule suminf_mult)

  1238     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)

  1239   also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"

  1240     apply (simp, rule suminf_le, simp)

  1241     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)

  1242   also have "... = (1/2)^(Suc N) * 2"

  1243     using suminf_geometric[of "1/2"] by auto

  1244   also have "... = (1/2)^N"

  1245     by auto

  1246   finally have *: "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) \<le> (1/2)^N"

  1247     by simp

  1248

  1249   define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"

  1250   have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"

  1251     unfolding M_def by (rule Max_ge, auto)

  1252   then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)

  1253   have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n

  1254     unfolding M_def apply (rule Max_ge) using that by auto

  1255   then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n

  1256     using that by force

  1257   have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>

  1258       (\<Sum>n< Suc N. M * (1 / 2) ^ n)"

  1259     by (rule sum_mono, simp add: i)

  1260   also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"

  1261     by (rule sum_distrib_left[symmetric])

  1262   also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"

  1263     by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)

  1264   also have "... = M * 2"

  1265     using suminf_geometric[of "1/2"] by auto

  1266   finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"

  1267     by simp

  1268

  1269   have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"

  1270     unfolding dist_fun_def by simp

  1271   also have "... = (\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)

  1272                   + (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"

  1273     apply (rule suminf_split_initial_segment)

  1274     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)

  1275   also have "... \<le> 2 * M + (1/2)^N"

  1276     using * ** by auto

  1277   finally show ?thesis unfolding M_def by simp

  1278 qed

  1279

  1280 lemma%unimportant open_fun_contains_ball_aux:

  1281   assumes "open (U::(('a \<Rightarrow> 'b) set))"

  1282           "x \<in> U"

  1283   shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"

  1284 proof -

  1285   have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"

  1286     using open_fun_def assms by auto

  1287   obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"

  1288                     "\<And>i. openin euclidean (X i)"

  1289                     "finite {i. X i \<noteq> topspace euclidean}"

  1290                     "x \<in> Pi\<^sub>E UNIV X"

  1291     using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto

  1292   define I where "I = {i. X i \<noteq> topspace euclidean}"

  1293   have "finite I" unfolding I_def using H(3) by auto

  1294   {

  1295     fix i

  1296     have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto

  1297     then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"

  1298       using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast

  1299     then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast

  1300     define f where "f = min e (1/2)"

  1301     have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto

  1302     moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto

  1303     ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto

  1304   } note * = this

  1305   have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"

  1306     by (rule choice, auto simp add: *)

  1307   then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"

  1308     by blast

  1309   define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"

  1310   have "m > 0" if "I\<noteq>{}"

  1311     unfolding m_def Min_gr_iff using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto

  1312   moreover have "{y. dist x y < m} \<subseteq> U"

  1313   proof (auto)

  1314     fix y assume "dist x y < m"

  1315     have "y i \<in> X i" if "i \<in> I" for i

  1316     proof -

  1317       have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"

  1318         by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)

  1319       define n where "n = to_nat i"

  1320       have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"

  1321         using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto

  1322       then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"

  1323         using \<open>n = to_nat i\<close> by auto

  1324       also have "... \<le> (1/2)^(to_nat i) * e i"

  1325         unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto

  1326       ultimately have "min (dist (x i) (y i)) 1 < e i"

  1327         by (auto simp add: divide_simps)

  1328       then have "dist (x i) (y i) < e i"

  1329         using \<open>e i < 1\<close> by auto

  1330       then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto

  1331     qed

  1332     then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)

  1333     then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto

  1334   qed

  1335   ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto

  1336

  1337   have "U = UNIV" if "I = {}"

  1338     using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)

  1339   then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast

  1340   then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast

  1341 qed

  1342

  1343 lemma%unimportant ball_fun_contains_open_aux:

  1344   fixes x::"('a \<Rightarrow> 'b)" and e::real

  1345   assumes "e>0"

  1346   shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"

  1347 proof -

  1348   have "\<exists>N::nat. 2^N > 8/e"

  1349     by (simp add: real_arch_pow)

  1350   then obtain N::nat where "2^N > 8/e" by auto

  1351   define f where "f = e/4"

  1352   have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto

  1353   define X::"('a \<Rightarrow> 'b set)" where "X = (\<lambda>i. if (\<exists>n\<le>N. i = from_nat n) then {z. dist (x i) z < f} else UNIV)"

  1354   have "{i. X i \<noteq> UNIV} \<subseteq> from_nat{0..N}"

  1355     unfolding X_def by auto

  1356   then have "finite {i. X i \<noteq> topspace euclidean}"

  1357     unfolding topspace_euclidean using finite_surj by blast

  1358   have "\<And>i. open (X i)"

  1359     unfolding X_def using metric_space_class.open_ball open_UNIV by auto

  1360   then have "\<And>i. openin euclidean (X i)"

  1361     using open_openin by auto

  1362   define U where "U = Pi\<^sub>E UNIV X"

  1363   have "open U"

  1364     unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)

  1365     unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>

  1366     by auto

  1367   moreover have "x \<in> U"

  1368     unfolding U_def X_def by (auto simp add: PiE_iff)

  1369   moreover have "dist x y < e" if "y \<in> U" for y

  1370   proof -

  1371     have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n

  1372       using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)

  1373       unfolding X_def using that by (metis less_imp_le mem_Collect_eq)

  1374     have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"

  1375       apply (rule Max.boundedI) using * by auto

  1376

  1377     have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"

  1378       by (rule dist_fun_le_dist_first_terms)

  1379     also have "... \<le> 2 * f + e / 8"

  1380       apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps divide_simps)

  1381     also have "... \<le> e/2 + e/8"

  1382       unfolding f_def by auto

  1383     also have "... < e"

  1384       by auto

  1385     finally show "dist x y < e" by simp

  1386   qed

  1387   ultimately show ?thesis by auto

  1388 qed

  1389

  1390 lemma%unimportant fun_open_ball_aux:

  1391   fixes U::"('a \<Rightarrow> 'b) set"

  1392   shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"

  1393 proof (auto)

  1394   assume "open U"

  1395   fix x assume "x \<in> U"

  1396   then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"

  1397     using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto

  1398 next

  1399   assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"

  1400   define K where "K = {V. open V \<and> V \<subseteq> U}"

  1401   {

  1402     fix x assume "x \<in> U"

  1403     then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast

  1404     then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"

  1405       using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto

  1406     have "V \<in> K"

  1407       unfolding K_def using e(2) V(1) V(3) by auto

  1408     then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto

  1409   }

  1410   then have "(\<Union>K) = U"

  1411     unfolding K_def by auto

  1412   moreover have "open (\<Union>K)"

  1413     unfolding K_def by auto

  1414   ultimately show "open U" by simp

  1415 qed

  1416

  1417 instance proof

  1418   fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"

  1419   proof

  1420     assume "x = y"

  1421     then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto

  1422   next

  1423     assume "dist x y = 0"

  1424     have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"

  1425       by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)

  1426     have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n

  1427       using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)

  1428     then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n

  1429       by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff

  1430                 zero_eq_1_divide_iff zero_neq_numeral)

  1431     then have "x (from_nat n) = y (from_nat n)" for n

  1432       by auto

  1433     then have "x i = y i" for i

  1434       by (metis from_nat_to_nat)

  1435     then show "x = y"

  1436       by auto

  1437   qed

  1438 next

  1439   text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing

  1440         with infinite series, hence we should justify the convergence at each step. In this

  1441         respect, the following simplification rule is extremely handy.\<close>

  1442   have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"

  1443     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)

  1444   fix x y z::"'a \<Rightarrow> 'b"

  1445   {

  1446     fix n

  1447     have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>

  1448             dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"

  1449       by (simp add: dist_triangle2)

  1450     have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"

  1451       using zero_le_dist by blast

  1452     moreover

  1453     {

  1454       assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"

  1455       then have "1 \<le> min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"

  1456         by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)

  1457     }

  1458     ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>

  1459             min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"

  1460       using * by linarith

  1461   } note ineq = this

  1462   have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"

  1463     unfolding dist_fun_def by simp

  1464   also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1

  1465                         + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"

  1466     apply (rule suminf_le)

  1467     using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left

  1468       le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)

  1469     by (auto simp add: summable_add)

  1470   also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)

  1471                   + (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"

  1472     by (rule suminf_add[symmetric], auto)

  1473   also have "... = dist x z + dist y z"

  1474     unfolding dist_fun_def by simp

  1475   finally show "dist x y \<le> dist x z + dist y z"

  1476     by simp

  1477 next

  1478   text\<open>Finally, we show that the topology generated by the distance and the product

  1479         topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,

  1480         except that the condition to prove is expressed with filters. To deal with this,

  1481         we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in

  1482         \verb+Real_Vector_Spaces.thy+\<close>

  1483   fix U::"('a \<Rightarrow> 'b) set"

  1484   have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P

  1485   unfolding uniformity_fun_def apply (subst eventually_INF_base)

  1486     by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])

  1487   then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"

  1488     unfolding fun_open_ball_aux by simp

  1489 qed (simp add: uniformity_fun_def)

  1490

  1491 end

  1492

  1493 text \<open>Nice properties of spaces are preserved under countable products. In addition

  1494 to first countability, second countability and metrizability, as we have seen above,

  1495 completeness is also preserved, and therefore being Polish.\<close>

  1496

  1497 instance "fun" :: (countable, complete_space) complete_space

  1498 proof

  1499   fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"

  1500   have "Cauchy (\<lambda>n. u n i)" for i

  1501   unfolding cauchy_def proof (intro impI allI)

  1502     fix e assume "e>(0::real)"

  1503     obtain k where "i = from_nat k"

  1504       using from_nat_to_nat[of i] by metis

  1505     have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto

  1506     then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"

  1507       using \<open>Cauchy u\<close> unfolding cauchy_def by blast

  1508     then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"

  1509       by blast

  1510     have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"

  1511     proof (auto)

  1512       fix m n::nat assume "m \<ge> N" "n \<ge> N"

  1513       have "(1/2)^k * min (dist (u m i) (u n i)) 1

  1514               = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"

  1515         using \<open>i = from_nat k\<close> by auto

  1516       also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"

  1517         apply (rule sum_le_suminf)

  1518         by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)

  1519       also have "... = dist (u m) (u n)"

  1520         unfolding dist_fun_def by auto

  1521       also have "... < (1/2)^k * min e 1"

  1522         using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto

  1523       finally have "min (dist (u m i) (u n i)) 1 < min e 1"

  1524         by (auto simp add: algebra_simps divide_simps)

  1525       then show "dist (u m i) (u n i) < e" by auto

  1526     qed

  1527     then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"

  1528       by blast

  1529   qed

  1530   then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i

  1531     using Cauchy_convergent convergent_def by auto

  1532   then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"

  1533     using choice by force

  1534   then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast

  1535   have "u \<longlonglongrightarrow> x"

  1536   proof (rule metric_LIMSEQ_I)

  1537     fix e assume [simp]: "e>(0::real)"

  1538     have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i

  1539       by (rule metric_LIMSEQ_D, auto simp add: *)

  1540     have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"

  1541       apply (rule choice) using i by auto

  1542     then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"

  1543       by blast

  1544

  1545     have "\<exists>N::nat. 2^N > 4/e"

  1546       by (simp add: real_arch_pow)

  1547     then obtain N::nat where "2^N > 4/e" by auto

  1548     define L where "L = Max {K (from_nat n)|n. n \<le> N}"

  1549     have "dist (u k) x < e" if "k \<ge> L" for k

  1550     proof -

  1551       have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n

  1552       proof -

  1553         have "K (from_nat n) \<le> L"

  1554           unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto

  1555         then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto

  1556         then show ?thesis using K less_imp_le by auto

  1557       qed

  1558       have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"

  1559         apply (rule Max.boundedI) using * by auto

  1560       have "dist (u k) x \<le> 2 * Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} + (1/2)^N"

  1561         using dist_fun_le_dist_first_terms by auto

  1562       also have "... \<le> 2 * e/4 + e/4"

  1563         apply (rule add_mono)

  1564         using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps divide_simps)

  1565       also have "... < e" by auto

  1566       finally show ?thesis by simp

  1567     qed

  1568     then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast

  1569   qed

  1570   then show "convergent u" using convergent_def by blast

  1571 qed

  1572

  1573 instance "fun" :: (countable, polish_space) polish_space

  1574 by standard

  1575

  1576

  1577

  1578

  1579 subsection%important \<open>Measurability\<close> (*FIX ME mv *)

  1580

  1581 text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,

  1582 generated by open sets in the product, and the product sigma algebra, countably generated by

  1583 products of measurable sets along finitely many coordinates. The second one is defined and studied

  1584 in \verb+Finite_Product_Measure.thy+.

  1585

  1586 These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),

  1587 but there is a fundamental difference: open sets are generated by arbitrary unions, not only

  1588 countable ones, so typically many open sets will not be measurable with respect to the product sigma

  1589 algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide

  1590 only when everything is countable (i.e., the product is countable, and the borel sigma algebra in

  1591 the factor is countably generated).

  1592

  1593 In this paragraph, we develop basic measurability properties for the borel sigma algebra, and

  1594 compare it with the product sigma algebra as explained above.

  1595 \<close>

  1596

  1597 lemma%unimportant measurable_product_coordinates [measurable (raw)]:

  1598   "(\<lambda>x. x i) \<in> measurable borel borel"

  1599 by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])

  1600

  1601 lemma%unimportant measurable_product_then_coordinatewise:

  1602   fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"

  1603   assumes [measurable]: "f \<in> borel_measurable M"

  1604   shows "(\<lambda>x. f x i) \<in> borel_measurable M"

  1605 proof -

  1606   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"

  1607     unfolding comp_def by auto

  1608   then show ?thesis by simp

  1609 qed

  1610

  1611 text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation

  1612 of the product sigma algebra that is more similar to the one we used above for the product

  1613 topology.\<close>

  1614

  1615 lemma%important sets_PiM_finite:

  1616   "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))

  1617         {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"

  1618 proof%unimportant

  1619   have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"

  1620   proof (auto)

  1621     fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"

  1622     then have *: "X i \<in> sets (M i)" for i by simp

  1623     define J where "J = {i \<in> I. X i \<noteq> space (M i)}"

  1624     have "finite J" "J \<subseteq> I" unfolding J_def using H by auto

  1625     define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"

  1626     have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"

  1627       unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto

  1628     moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"

  1629       unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]

  1630       by (auto simp add: PiE_iff, blast)

  1631     ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp

  1632   qed

  1633   then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}

  1634               \<subseteq> sets (Pi\<^sub>M I M)"

  1635     by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)

  1636

  1637   have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>

  1638                 (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"

  1639     if "i \<in> I" "A \<in> sets (M i)" for i A

  1640   proof -

  1641     define X where "X = (\<lambda>j. if j = i then A else space (M j))"

  1642     have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"

  1643       unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>

  1644       by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)

  1645     moreover have "X j \<in> sets (M j)" for j

  1646       unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto

  1647     moreover have "finite {j. X j \<noteq> space (M j)}"

  1648       unfolding X_def by simp

  1649     ultimately show ?thesis by auto

  1650   qed

  1651   show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"

  1652     unfolding sets_PiM_single

  1653     apply (rule sigma_sets_mono')

  1654     apply (auto simp add: PiE_iff *)

  1655     done

  1656 qed

  1657

  1658 lemma%important sets_PiM_subset_borel:

  1659   "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"

  1660 proof%unimportant -

  1661   have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"

  1662   proof -

  1663     define I where "I = {i. X i \<noteq> UNIV}"

  1664     have "finite I" unfolding I_def using that by simp

  1665     have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-(X i) \<inter> space borel) \<inter> space borel"

  1666       unfolding I_def by auto

  1667     also have "... \<in> sets borel"

  1668       using that \<open>finite I\<close> by measurable

  1669     finally show ?thesis by simp

  1670   qed

  1671   then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"

  1672     by auto

  1673   then show ?thesis unfolding sets_PiM_finite space_borel

  1674     by (simp add: * sets.sigma_sets_subset')

  1675 qed

  1676

  1677 lemma%important sets_PiM_equal_borel:

  1678   "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"

  1679 proof%unimportant

  1680   obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"

  1681             "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"

  1682     using product_topology_countable_basis by fast

  1683   have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k

  1684   proof -

  1685     obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"

  1686       using K(3)[OF \<open>k \<in> K\<close>] by blast

  1687     show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto

  1688   qed

  1689   have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"

  1690   proof -

  1691     obtain B where "B \<subseteq> K" "U = (\<Union>B)"

  1692       using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)

  1693     have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast

  1694     moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k

  1695       using \<open>B \<subseteq> K\<close> * that by auto

  1696     ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto

  1697   qed

  1698   have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"

  1699     apply (rule sets.sigma_sets_subset') using ** by auto

  1700   then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"

  1701     unfolding borel_def by auto

  1702 qed (simp add: sets_PiM_subset_borel)

  1703

  1704 lemma%important measurable_coordinatewise_then_product:

  1705   fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"

  1706   assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"

  1707   shows "f \<in> borel_measurable M"

  1708 proof%unimportant -

  1709   have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"

  1710     by (rule measurable_PiM_single', auto simp add: assms)

  1711   then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast

  1712 qed

  1713

  1714 end