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
lp15@69030
     1
(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr with additions from LCP
hoelzl@64289
     2
    License: BSD
hoelzl@64289
     3
*)
hoelzl@64289
     4
hoelzl@64289
     5
theory Function_Topology
lp15@69030
     6
imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure 
hoelzl@64289
     7
begin
hoelzl@64289
     8
hoelzl@64289
     9
nipkow@69517
    10
section%important \<open>Product Topology\<close>
hoelzl@64289
    11
wenzelm@64911
    12
text \<open>We want to define the product topology.
hoelzl@64289
    13
hoelzl@64289
    14
The product topology on a product of topological spaces is generated by
hoelzl@64289
    15
the sets which are products of open sets along finitely many coordinates, and the whole
hoelzl@64289
    16
space along the other coordinates. This is the coarsest topology for which the projection
hoelzl@64289
    17
to each factor is continuous.
hoelzl@64289
    18
hoelzl@64289
    19
To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
wenzelm@64910
    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
hoelzl@64289
    21
coordinate belongs to $X\;i$ for all $i \in I$.
hoelzl@64289
    22
hoelzl@64289
    23
Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
hoelzl@64289
    24
This means that type classes can not be used to define such a product if one wants to take the
hoelzl@64289
    25
product of different topological spaces (as the type 'a can only be given one structure of
hoelzl@64289
    26
topological space using type classes). On the other hand, one can define different topologies (as
lp15@66827
    27
introduced in \verb+thy+) on one type, and these topologies do not need to
hoelzl@64289
    28
share the same maximal open set. Hence, one can form a product of topologies in this sense, and
hoelzl@64289
    29
this works well. The big caveat is that it does not interact well with the main body of
hoelzl@64289
    30
topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
hoelzl@64289
    31
is not defined in this setting.
hoelzl@64289
    32
hoelzl@64289
    33
As the product of different topological spaces is very important in several areas of
hoelzl@64289
    34
mathematics (for instance adeles), I introduce below the product topology in terms of topologies,
hoelzl@64289
    35
and reformulate afterwards the consequences in terms of type classes (which are of course very
hoelzl@64289
    36
handy for applications).
hoelzl@64289
    37
hoelzl@64289
    38
Given this limitation, it looks to me that it would be very beneficial to revamp the theory
hoelzl@64289
    39
of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving
hoelzl@64289
    40
type classes as consequences of more general statements in terms of topologies (but I am
hoelzl@64289
    41
probably too naive here).
hoelzl@64289
    42
hoelzl@64289
    43
Here is an example of a reformulation using topologies. Let
hoelzl@64289
    44
\begin{verbatim}
hoelzl@64289
    45
continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
hoelzl@64289
    46
                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))
hoelzl@64289
    47
\end{verbatim}
hoelzl@64289
    48
be the natural continuity definition of a map from the topology $T1$ to the topology $T2$. Then
hoelzl@64289
    49
the current \verb+continuous_on+ (with type classes) can be redefined as
hoelzl@64289
    50
\begin{verbatim}
hoelzl@64289
    51
continuous_on s f = continuous_on_topo (subtopology euclidean s) (topology euclidean) f
hoelzl@64289
    52
\end{verbatim}
hoelzl@64289
    53
hoelzl@64289
    54
In fact, I need \verb+continuous_on_topo+ to express the continuity of the projection on subfactors
hoelzl@64289
    55
for the product topology, in Lemma~\verb+continuous_on_restrict_product_topology+, and I show
hoelzl@64289
    56
the above equivalence in Lemma~\verb+continuous_on_continuous_on_topo+.
hoelzl@64289
    57
hoelzl@64289
    58
I only develop the basics of the product topology in this theory. The most important missing piece
hoelzl@64289
    59
is Tychonov theorem, stating that a product of compact spaces is always compact for the product
hoelzl@64289
    60
topology, even when the product is not finite (or even countable).
hoelzl@64289
    61
hoelzl@64289
    62
I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
wenzelm@64911
    63
\<close>
hoelzl@64289
    64
ak2110@68833
    65
subsection%important \<open>Topology without type classes\<close>
hoelzl@64289
    66
ak2110@68833
    67
subsubsection%important \<open>The topology generated by some (open) subsets\<close>
hoelzl@64289
    68
wenzelm@64911
    69
text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
hoelzl@64289
    70
as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
hoelzl@64289
    71
and is never a problem in proofs, so I prefer to write it down explicitly.
hoelzl@64289
    72
hoelzl@64289
    73
We do not require UNIV to be an open set, as this will not be the case in applications. (We are
wenzelm@64911
    74
thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)\<close>
hoelzl@64289
    75
hoelzl@64289
    76
inductive generate_topology_on for S where
hoelzl@64289
    77
Empty: "generate_topology_on S {}"
hoelzl@64289
    78
|Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
hoelzl@64289
    79
| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
hoelzl@64289
    80
| Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
hoelzl@64289
    81
ak2110@68833
    82
lemma%unimportant istopology_generate_topology_on:
hoelzl@64289
    83
  "istopology (generate_topology_on S)"
hoelzl@64289
    84
unfolding istopology_def by (auto intro: generate_topology_on.intros)
hoelzl@64289
    85
wenzelm@64911
    86
text \<open>The basic property of the topology generated by a set $S$ is that it is the
wenzelm@64911
    87
smallest topology containing all the elements of $S$:\<close>
hoelzl@64289
    88
ak2110@68833
    89
lemma%unimportant generate_topology_on_coarsest:
hoelzl@64289
    90
  assumes "istopology T"
hoelzl@64289
    91
          "\<And>s. s \<in> S \<Longrightarrow> T s"
hoelzl@64289
    92
          "generate_topology_on S s0"
hoelzl@64289
    93
  shows "T s0"
hoelzl@64289
    94
using assms(3) apply (induct rule: generate_topology_on.induct)
hoelzl@64289
    95
using assms(1) assms(2) unfolding istopology_def by auto
hoelzl@64289
    96
lp15@69030
    97
abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
lp15@69030
    98
  where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
hoelzl@64289
    99
ak2110@68833
   100
lemma%unimportant openin_topology_generated_by_iff:
hoelzl@64289
   101
  "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
lp15@69030
   102
  using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
hoelzl@64289
   103
ak2110@68833
   104
lemma%unimportant openin_topology_generated_by:
hoelzl@64289
   105
  "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
hoelzl@64289
   106
using openin_topology_generated_by_iff by auto
hoelzl@64289
   107
ak2110@68833
   108
lemma%important topology_generated_by_topspace:
hoelzl@64289
   109
  "topspace (topology_generated_by S) = (\<Union>S)"
ak2110@68833
   110
proof%unimportant
hoelzl@64289
   111
  {
hoelzl@64289
   112
    fix s assume "openin (topology_generated_by S) s"
hoelzl@64289
   113
    then have "generate_topology_on S s" by (rule openin_topology_generated_by)
hoelzl@64289
   114
    then have "s \<subseteq> (\<Union>S)" by (induct, auto)
hoelzl@64289
   115
  }
hoelzl@64289
   116
  then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"
hoelzl@64289
   117
    unfolding topspace_def by auto
hoelzl@64289
   118
next
hoelzl@64289
   119
  have "generate_topology_on S (\<Union>S)"
hoelzl@64289
   120
    using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
hoelzl@64289
   121
  then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
hoelzl@64289
   122
    unfolding topspace_def using openin_topology_generated_by_iff by auto
hoelzl@64289
   123
qed
hoelzl@64289
   124
ak2110@68833
   125
lemma%important topology_generated_by_Basis:
hoelzl@64289
   126
  "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
ak2110@68833
   127
by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
hoelzl@64289
   128
lp15@69030
   129
lemma generate_topology_on_Inter:
lp15@69030
   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>)"
lp15@69030
   131
  by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)
lp15@69030
   132
lp15@69030
   133
subsection\<open>Topology bases and sub-bases\<close>
lp15@69030
   134
lp15@69030
   135
lemma istopology_base_alt:
lp15@69030
   136
   "istopology (arbitrary union_of P) \<longleftrightarrow>
lp15@69030
   137
    (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
lp15@69030
   138
           \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
lp15@69030
   139
  by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)
lp15@69030
   140
lp15@69030
   141
lemma istopology_base_eq:
lp15@69030
   142
   "istopology (arbitrary union_of P) \<longleftrightarrow>
lp15@69030
   143
    (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
lp15@69030
   144
  by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)
lp15@69030
   145
lp15@69030
   146
lemma istopology_base:
lp15@69030
   147
   "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"
lp15@69030
   148
  by (simp add: arbitrary_def istopology_base_eq union_of_inc)
lp15@69030
   149
lp15@69030
   150
lemma openin_topology_base_unique:
lp15@69030
   151
   "openin X = arbitrary union_of P \<longleftrightarrow>
lp15@69030
   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))"
lp15@69030
   153
   (is "?lhs = ?rhs")
lp15@69030
   154
proof
lp15@69030
   155
  assume ?lhs
lp15@69030
   156
  then show ?rhs
lp15@69030
   157
    by (auto simp: union_of_def arbitrary_def)
lp15@69030
   158
next
lp15@69030
   159
  assume R: ?rhs
lp15@69030
   160
  then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S
lp15@69030
   161
    using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce
lp15@69030
   162
  from R show ?lhs
lp15@69030
   163
    by (fastforce simp add: union_of_def arbitrary_def intro: *)
lp15@69030
   164
qed
lp15@69030
   165
lp15@69030
   166
lemma topology_base_unique:
lp15@69030
   167
   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
lp15@69030
   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>
lp15@69030
   169
    \<Longrightarrow> topology(arbitrary union_of P) = X"
lp15@69030
   170
  by (metis openin_topology_base_unique openin_inverse [of X])
lp15@69030
   171
lp15@69030
   172
lemma topology_bases_eq_aux:
lp15@69030
   173
   "\<lbrakk>(arbitrary union_of P) S;
lp15@69030
   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>
lp15@69030
   175
        \<Longrightarrow> (arbitrary union_of Q) S"
lp15@69030
   176
  by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)
lp15@69030
   177
lp15@69030
   178
lemma topology_bases_eq:
lp15@69030
   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;
lp15@69030
   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>
lp15@69030
   181
        \<Longrightarrow> topology (arbitrary union_of P) =
lp15@69030
   182
            topology (arbitrary union_of Q)"
lp15@69030
   183
  by (fastforce intro:  arg_cong [where f=topology]  elim: topology_bases_eq_aux)
lp15@69030
   184
lp15@69030
   185
lemma istopology_subbase:
lp15@69030
   186
   "istopology (arbitrary union_of (finite intersection_of P relative_to S))"
lp15@69030
   187
  by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)
lp15@69030
   188
lp15@69030
   189
lemma openin_subbase:
lp15@69030
   190
  "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S
lp15@69030
   191
   \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"
lp15@69030
   192
  by (simp add: istopology_subbase topology_inverse')
lp15@69030
   193
lp15@69030
   194
lemma topspace_subbase [simp]:
lp15@69030
   195
   "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")
lp15@69030
   196
proof
lp15@69030
   197
  show "?lhs \<subseteq> U"
lp15@69030
   198
    by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)
lp15@69030
   199
  show "U \<subseteq> ?lhs"
lp15@69030
   200
    by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase 
lp15@69030
   201
              openin_subset relative_to_inc subset_UNIV topology_inverse')
lp15@69030
   202
qed
lp15@69030
   203
lp15@69030
   204
lemma minimal_topology_subbase:
lp15@69030
   205
   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;
lp15@69030
   206
     openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>
lp15@69030
   207
    \<Longrightarrow> openin X S"
lp15@69030
   208
  apply (simp add: istopology_subbase topology_inverse)
lp15@69030
   209
  apply (simp add: union_of_def intersection_of_def relative_to_def)
lp15@69030
   210
  apply (blast intro: openin_Int_Inter)
lp15@69030
   211
  done
lp15@69030
   212
lp15@69030
   213
lemma istopology_subbase_UNIV:
lp15@69030
   214
   "istopology (arbitrary union_of (finite intersection_of P))"
lp15@69030
   215
  by (simp add: istopology_base finite_intersection_of_Int)
lp15@69030
   216
lp15@69030
   217
lp15@69030
   218
lemma generate_topology_on_eq:
lp15@69030
   219
  "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")
lp15@69030
   220
proof (intro ext iffI)
lp15@69030
   221
  fix A
lp15@69030
   222
  assume "?lhs A"
lp15@69030
   223
  then show "?rhs A"
lp15@69030
   224
  proof induction
lp15@69030
   225
    case (Int a b)
lp15@69030
   226
    then show ?case
lp15@69030
   227
      by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)
lp15@69030
   228
  next
lp15@69030
   229
    case (UN K)
lp15@69030
   230
    then show ?case
lp15@69030
   231
      by (simp add: arbitrary_union_of_Union)
lp15@69030
   232
  next
lp15@69030
   233
    case (Basis s)
lp15@69030
   234
    then show ?case
lp15@69030
   235
      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
lp15@69030
   236
  qed auto
lp15@69030
   237
next
lp15@69030
   238
  fix A
lp15@69030
   239
  assume "?rhs A"
lp15@69030
   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>"
lp15@69030
   241
    unfolding union_of_def intersection_of_def by auto
lp15@69030
   242
  show "?lhs A"
lp15@69030
   243
    unfolding eq
lp15@69030
   244
  proof (rule generate_topology_on.UN)
lp15@69030
   245
    fix T
lp15@69030
   246
    assume "T \<in> \<U>"
lp15@69030
   247
    with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"
lp15@69030
   248
      by blast
lp15@69030
   249
    have "generate_topology_on S (\<Inter>\<F>)"
lp15@69030
   250
    proof (rule generate_topology_on_Inter)
lp15@69030
   251
      show "finite \<F>" "\<F> \<noteq> {}"
lp15@69030
   252
        by (auto simp: \<open>finite' \<F>\<close>)
lp15@69030
   253
      show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"
lp15@69030
   254
        by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)
lp15@69030
   255
    qed
lp15@69030
   256
    then show "generate_topology_on S T"
lp15@69030
   257
      using \<open>\<Inter>\<F> = T\<close> by blast
lp15@69030
   258
  qed
lp15@69030
   259
qed
lp15@69030
   260
ak2110@68833
   261
subsubsection%important \<open>Continuity\<close>
hoelzl@64289
   262
wenzelm@64911
   263
text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
wenzelm@64911
   264
of type classes, as defined below.\<close>
hoelzl@64289
   265
ak2110@68833
   266
definition%important continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
hoelzl@64289
   267
  where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
hoelzl@64289
   268
                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
hoelzl@64289
   269
ak2110@68833
   270
lemma%important continuous_on_continuous_on_topo:
hoelzl@64289
   271
  "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
ak2110@68833
   272
unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
hoelzl@64289
   273
topspace_euclidean_subtopology open_openin topspace_euclidean by fast
hoelzl@64289
   274
ak2110@68833
   275
lemma%unimportant continuous_on_topo_UNIV:
hoelzl@64289
   276
  "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
hoelzl@64289
   277
using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
hoelzl@64289
   278
ak2110@68833
   279
lemma%important continuous_on_topo_open [intro]:
hoelzl@64289
   280
  "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
ak2110@68833
   281
unfolding%unimportant continuous_on_topo_def by auto
hoelzl@64289
   282
ak2110@68833
   283
lemma%unimportant continuous_on_topo_topspace [intro]:
hoelzl@64289
   284
  "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
hoelzl@64289
   285
unfolding continuous_on_topo_def by auto
hoelzl@64289
   286
ak2110@68833
   287
lemma%important continuous_on_generated_topo_iff:
hoelzl@64289
   288
  "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
hoelzl@64289
   289
      ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
hoelzl@64289
   290
unfolding continuous_on_topo_def topology_generated_by_topspace
ak2110@68833
   291
proof%unimportant (auto simp add: topology_generated_by_Basis)
hoelzl@64289
   292
  assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
hoelzl@64289
   293
  fix U assume "openin (topology_generated_by S) U"
hoelzl@64289
   294
  then have "generate_topology_on S U" by (rule openin_topology_generated_by)
hoelzl@64289
   295
  then show "openin T1 (f -` U \<inter> topspace T1)"
hoelzl@64289
   296
  proof (induct)
hoelzl@64289
   297
    fix a b
hoelzl@64289
   298
    assume H: "openin T1 (f -` a \<inter> topspace T1)" "openin T1 (f -` b \<inter> topspace T1)"
hoelzl@64289
   299
    have "f -` (a \<inter> b) \<inter> topspace T1 = (f-`a \<inter> topspace T1) \<inter> (f-`b \<inter> topspace T1)"
hoelzl@64289
   300
      by auto
hoelzl@64289
   301
    then show "openin T1 (f -` (a \<inter> b) \<inter> topspace T1)" using H by auto
hoelzl@64289
   302
  next
hoelzl@64289
   303
    fix K
hoelzl@64289
   304
    assume H: "openin T1 (f -` k \<inter> topspace T1)" if "k\<in> K" for k
hoelzl@64289
   305
    define L where "L = {f -` k \<inter> topspace T1|k. k \<in> K}"
hoelzl@64289
   306
    have *: "openin T1 l" if "l \<in>L" for l using that H unfolding L_def by auto
hoelzl@64289
   307
    have "openin T1 (\<Union>L)" using openin_Union[OF *] by simp
hoelzl@64289
   308
    moreover have "(\<Union>L) = (f -` \<Union>K \<inter> topspace T1)" unfolding L_def by auto
hoelzl@64289
   309
    ultimately show "openin T1 (f -` \<Union>K \<inter> topspace T1)" by simp
hoelzl@64289
   310
  qed (auto simp add: H)
hoelzl@64289
   311
qed
hoelzl@64289
   312
ak2110@68833
   313
lemma%important continuous_on_generated_topo:
hoelzl@64289
   314
  assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
hoelzl@64289
   315
          "f`(topspace T1) \<subseteq> (\<Union> S)"
hoelzl@64289
   316
  shows "continuous_on_topo T1 (topology_generated_by S) f"
ak2110@68833
   317
using%unimportant assms continuous_on_generated_topo_iff by blast
hoelzl@64289
   318
ak2110@68833
   319
lemma%important continuous_on_topo_compose:
hoelzl@64289
   320
  assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
hoelzl@64289
   321
  shows "continuous_on_topo T1 T3 (g o f)"
ak2110@68833
   322
using%unimportant assms unfolding continuous_on_topo_def
ak2110@68833
   323
proof%unimportant (auto)
hoelzl@64289
   324
  fix U :: "'c set"
hoelzl@64289
   325
  assume H: "openin T3 U"
hoelzl@64289
   326
  have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
hoelzl@64289
   327
    using H assms by blast
hoelzl@64289
   328
  moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
hoelzl@64289
   329
    using H assms continuous_on_topo_topspace by fastforce
hoelzl@64289
   330
  ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
hoelzl@64289
   331
    by simp
hoelzl@64289
   332
qed (blast)
hoelzl@64289
   333
ak2110@68833
   334
lemma%unimportant continuous_on_topo_preimage_topspace [intro]:
hoelzl@64289
   335
  assumes "continuous_on_topo T1 T2 f"
hoelzl@64289
   336
  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
hoelzl@64289
   337
using assms unfolding continuous_on_topo_def by auto
hoelzl@64289
   338
hoelzl@64289
   339
ak2110@68833
   340
subsubsection%important \<open>Pullback topology\<close>
hoelzl@64289
   341
wenzelm@64911
   342
text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
hoelzl@64289
   343
a special case of this notion, pulling back by the identity. We introduce the general notion as
hoelzl@64289
   344
we will need it to define the strong operator topology on the space of continuous linear operators,
wenzelm@64911
   345
by pulling back the product topology on the space of all functions.\<close>
hoelzl@64289
   346
wenzelm@64911
   347
text \<open>\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
wenzelm@64911
   348
the set $A$.\<close>
hoelzl@64289
   349
ak2110@68833
   350
definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
hoelzl@64289
   351
  where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
hoelzl@64289
   352
ak2110@68833
   353
lemma%important istopology_pullback_topology:
hoelzl@64289
   354
  "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
ak2110@68833
   355
unfolding%unimportant istopology_def proof (auto)
hoelzl@64289
   356
  fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
hoelzl@64289
   357
  then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
hoelzl@64289
   358
    by (rule bchoice)
hoelzl@64289
   359
  then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
hoelzl@64289
   360
    by blast
hoelzl@64289
   361
  define V where "V = (\<Union>S\<in>K. U S)"
hoelzl@64289
   362
  have "openin T V" "\<Union>K = f -` V \<inter> A" unfolding V_def using U by auto
hoelzl@64289
   363
  then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
hoelzl@64289
   364
qed
hoelzl@64289
   365
ak2110@68833
   366
lemma%unimportant openin_pullback_topology:
hoelzl@64289
   367
  "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
hoelzl@64289
   368
unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto
hoelzl@64289
   369
ak2110@68833
   370
lemma%unimportant topspace_pullback_topology:
hoelzl@64289
   371
  "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
hoelzl@64289
   372
by (auto simp add: topspace_def openin_pullback_topology)
hoelzl@64289
   373
ak2110@68833
   374
lemma%important continuous_on_topo_pullback [intro]:
hoelzl@64289
   375
  assumes "continuous_on_topo T1 T2 g"
hoelzl@64289
   376
  shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
hoelzl@64289
   377
unfolding continuous_on_topo_def
ak2110@68833
   378
proof%unimportant (auto)
hoelzl@64289
   379
  fix U::"'b set" assume "openin T2 U"
hoelzl@64289
   380
  then have "openin T1 (g-`U \<inter> topspace T1)"
hoelzl@64289
   381
    using assms unfolding continuous_on_topo_def by auto
hoelzl@64289
   382
  have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
hoelzl@64289
   383
    unfolding topspace_pullback_topology by auto
hoelzl@64289
   384
  also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
hoelzl@64289
   385
    by auto
hoelzl@64289
   386
  also have "openin (pullback_topology A f T1) (...)"
wenzelm@64911
   387
    unfolding openin_pullback_topology using \<open>openin T1 (g-`U \<inter> topspace T1)\<close> by auto
hoelzl@64289
   388
  finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
hoelzl@64289
   389
    by auto
hoelzl@64289
   390
next
hoelzl@64289
   391
  fix x assume "x \<in> topspace (pullback_topology A f T1)"
hoelzl@64289
   392
  then have "f x \<in> topspace T1"
hoelzl@64289
   393
    unfolding topspace_pullback_topology by auto
hoelzl@64289
   394
  then show "g (f x) \<in> topspace T2"
hoelzl@64289
   395
    using assms unfolding continuous_on_topo_def by auto
hoelzl@64289
   396
qed
hoelzl@64289
   397
ak2110@68833
   398
lemma%important continuous_on_topo_pullback' [intro]:
hoelzl@64289
   399
  assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
hoelzl@64289
   400
  shows "continuous_on_topo T1 (pullback_topology A f T2) g"
hoelzl@64289
   401
unfolding continuous_on_topo_def
ak2110@68833
   402
proof%unimportant (auto)
hoelzl@64289
   403
  fix U assume "openin (pullback_topology A f T2) U"
hoelzl@64289
   404
  then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
hoelzl@64289
   405
    unfolding openin_pullback_topology by auto
hoelzl@64289
   406
  then obtain V where "openin T2 V" "U = f-`V \<inter> A"
hoelzl@64289
   407
    by blast
hoelzl@64289
   408
  then have "g -` U \<inter> topspace T1 = g-`(f-`V \<inter> A) \<inter> topspace T1"
hoelzl@64289
   409
    by blast
hoelzl@64289
   410
  also have "... = (f o g)-`V \<inter> (g-`A \<inter> topspace T1)"
hoelzl@64289
   411
    by auto
hoelzl@64289
   412
  also have "... = (f o g)-`V \<inter> topspace T1"
hoelzl@64289
   413
    using assms(2) by auto
hoelzl@64289
   414
  also have "openin T1 (...)"
wenzelm@64911
   415
    using assms(1) \<open>openin T2 V\<close> by auto
hoelzl@64289
   416
  finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
hoelzl@64289
   417
next
hoelzl@64289
   418
  fix x assume "x \<in> topspace T1"
hoelzl@64289
   419
  have "(f o g) x \<in> topspace T2"
wenzelm@64911
   420
    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
hoelzl@64289
   421
  then have "g x \<in> f-`(topspace T2)"
hoelzl@64289
   422
    unfolding comp_def by blast
wenzelm@64911
   423
  moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
hoelzl@64289
   424
  ultimately show "g x \<in> topspace (pullback_topology A f T2)"
hoelzl@64289
   425
    unfolding topspace_pullback_topology by blast
hoelzl@64289
   426
qed
hoelzl@64289
   427
hoelzl@64289
   428
ak2110@68833
   429
subsection%important \<open>The product topology\<close>
hoelzl@64289
   430
wenzelm@64911
   431
text \<open>We can now define the product topology, as generated by
hoelzl@64289
   432
the sets which are products of open sets along finitely many coordinates, and the whole
hoelzl@64289
   433
space along the other coordinates. Equivalently, it is generated by sets which are one open
hoelzl@64289
   434
set along one single coordinate, and the whole space along other coordinates. In fact, this is only
hoelzl@64289
   435
equivalent for nonempty products, but for the empty product the first formulation is better
hoelzl@64289
   436
(the second one gives an empty product space, while an empty product should have exactly one
hoelzl@64289
   437
point, equal to \verb+undefined+ along all coordinates.
hoelzl@64289
   438
hoelzl@64289
   439
So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
wenzelm@64911
   440
\<close>
hoelzl@64289
   441
ak2110@68833
   442
definition%important product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
hoelzl@64289
   443
  where "product_topology T I =
hoelzl@64289
   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)}}"
hoelzl@64289
   445
wenzelm@64911
   446
text \<open>The total set of the product topology is the product of the total sets
wenzelm@64911
   447
along each coordinate.\<close>
hoelzl@64289
   448
lp15@69030
   449
proposition product_topology:
lp15@69030
   450
  "product_topology X I =
lp15@69030
   451
   topology
lp15@69030
   452
    (arbitrary union_of
lp15@69030
   453
       ((finite intersection_of
lp15@69030
   454
        (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
lp15@69030
   455
        relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"
lp15@69030
   456
  (is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")
lp15@69030
   457
proof -
lp15@69030
   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)})"
lp15@69030
   459
  have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A
lp15@69030
   460
  proof -
lp15@69030
   461
    have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"
lp15@69030
   462
      if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>
lp15@69030
   463
    proof -
lp15@69030
   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)}"
lp15@69030
   465
        using \<U> by auto
lp15@69030
   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)}"
lp15@69030
   467
        by metis
lp15@69030
   468
      obtain U where "U \<in> \<U>"
lp15@69030
   469
        using \<open>\<U> \<noteq> {}\<close> by blast
lp15@69030
   470
      let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i}) ` {i \<in> I. Y U i \<noteq> topspace (X i)}"
lp15@69030
   471
      show ?thesis
lp15@69030
   472
      proof (intro conjI exI)
lp15@69030
   473
        show "finite (\<Union>U\<in>\<U>. ?F U)"
lp15@69030
   474
          using Y \<open>finite' \<U>\<close> by auto
lp15@69030
   475
        show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"
lp15@69030
   476
        proof
lp15@69030
   477
          have *: "f \<in> U"
lp15@69030
   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"
lp15@69030
   479
              and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
lp15@69030
   480
          proof -
lp15@69030
   481
            have "Pi\<^sub>E I (Y U) = U"
lp15@69030
   482
              using Y \<open>U \<in> \<U>\<close> by blast
lp15@69030
   483
            then show "f \<in> U"
lp15@69030
   484
              using that unfolding PiE_def Pi_def by blast
lp15@69030
   485
          qed
lp15@69030
   486
          show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
lp15@69030
   487
            by (auto simp: PiE_iff *)
lp15@69030
   488
          show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
lp15@69030
   489
            using Y openin_subset \<open>finite' \<U>\<close> by fastforce
lp15@69030
   490
        qed
lp15@69030
   491
      qed (use Y openin_subset in \<open>blast+\<close>)
lp15@69030
   492
    qed
lp15@69030
   493
    have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"
lp15@69030
   494
      if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>
lp15@69030
   495
    proof (cases "\<U>={}")
lp15@69030
   496
      case True
lp15@69030
   497
      then show ?thesis
lp15@69030
   498
        apply (rule_tac x="{?TOP}" in exI, simp)
lp15@69030
   499
        apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)
lp15@69030
   500
        apply force
lp15@69030
   501
        done
lp15@69030
   502
    next
lp15@69030
   503
      case False
lp15@69030
   504
      then obtain U where "U \<in> \<U>"
lp15@69030
   505
        by blast
lp15@69030
   506
      have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"
lp15@69030
   507
        using \<U> by auto
lp15@69030
   508
      then obtain J Y where
lp15@69030
   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)"
lp15@69030
   510
        by metis
lp15@69030
   511
      let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"
lp15@69030
   512
      show ?thesis
lp15@69030
   513
      proof (intro conjI exI)
lp15@69030
   514
        show "finite (?G ` \<U>)" "?G ` \<U> \<noteq> {}"
lp15@69030
   515
          using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+
lp15@69030
   516
        have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"
lp15@69030
   517
          using Y by force
lp15@69030
   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)}}"
lp15@69030
   519
          apply clarsimp
lp15@69030
   520
          apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
lp15@69030
   521
          apply (auto simp: *)
lp15@69030
   522
          done
lp15@69030
   523
      next
lp15@69030
   524
        show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
lp15@69030
   525
        proof
lp15@69030
   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))"
lp15@69030
   527
            apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
lp15@69030
   528
            using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
lp15@69030
   529
          then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
lp15@69030
   530
            using \<open>U \<in> \<U>\<close>
lp15@69030
   531
            by fastforce
lp15@69030
   532
          moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
lp15@69030
   533
            using PiE_mem Y by fastforce
lp15@69030
   534
          ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
lp15@69030
   535
            by auto
lp15@69030
   536
        qed (use Y in fastforce)
lp15@69030
   537
      qed
lp15@69030
   538
    qed
lp15@69030
   539
    show ?thesis
lp15@69030
   540
      unfolding relative_to_def intersection_of_def
lp15@69030
   541
      by (safe; blast dest!: 1 2)
lp15@69030
   542
  qed
lp15@69030
   543
  show ?thesis
lp15@69030
   544
    unfolding product_topology_def generate_topology_on_eq
lp15@69030
   545
    apply (rule arg_cong [where f = topology])
lp15@69030
   546
    apply (rule arg_cong [where f = "(union_of)arbitrary"])
lp15@69030
   547
    apply (force simp: *)
lp15@69030
   548
    done
lp15@69030
   549
qed
lp15@69030
   550
lp15@69030
   551
lemma%important topspace_product_topology:
hoelzl@64289
   552
  "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
ak2110@68833
   553
proof%unimportant
hoelzl@64289
   554
  show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
lp15@69030
   555
    unfolding product_topology_def topology_generated_by_topspace
hoelzl@64289
   556
    unfolding topspace_def by auto
hoelzl@64289
   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)}}"
hoelzl@64289
   558
    using openin_topspace not_finite_existsD by auto
hoelzl@64289
   559
  then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
hoelzl@64289
   560
    unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
hoelzl@64289
   561
qed
hoelzl@64289
   562
ak2110@68833
   563
lemma%unimportant product_topology_basis:
hoelzl@64289
   564
  assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
hoelzl@64289
   565
  shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
lp15@69030
   566
  unfolding product_topology_def
lp15@69030
   567
  by (rule topology_generated_by_Basis) (use assms in auto)
hoelzl@64289
   568
ak2110@68833
   569
lemma%important product_topology_open_contains_basis:
lp15@69030
   570
  assumes "openin (product_topology T I) U" "x \<in> U"
hoelzl@64289
   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"
ak2110@68833
   572
proof%unimportant -
hoelzl@64289
   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"
hoelzl@64289
   574
    using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
hoelzl@64289
   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"
hoelzl@64289
   576
  proof induction
hoelzl@64289
   577
    case (Int U V x)
hoelzl@64289
   578
    then obtain XU XV where H:
hoelzl@64289
   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"
hoelzl@64289
   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"
hoelzl@64289
   581
      by auto meson
hoelzl@64289
   582
    define X where "X = (\<lambda>i. XU i \<inter> XV i)"
hoelzl@64289
   583
    have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
hoelzl@64289
   584
      unfolding X_def by (auto simp add: PiE_iff)
hoelzl@64289
   585
    then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
hoelzl@64289
   586
    moreover have "\<forall>i. openin (T i) (X i)"
hoelzl@64289
   587
      unfolding X_def using H by auto
hoelzl@64289
   588
    moreover have "finite {i. X i \<noteq> topspace (T i)}"
hoelzl@64289
   589
      apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
hoelzl@64289
   590
      unfolding X_def using H by auto
hoelzl@64289
   591
    moreover have "x \<in> Pi\<^sub>E I X"
hoelzl@64289
   592
      unfolding X_def using H by auto
hoelzl@64289
   593
    ultimately show ?case
hoelzl@64289
   594
      by auto
hoelzl@64289
   595
  next
hoelzl@64289
   596
    case (UN K x)
hoelzl@64289
   597
    then obtain k where "k \<in> K" "x \<in> k" by auto
hoelzl@64289
   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"
hoelzl@64289
   599
      by simp
hoelzl@64289
   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"
hoelzl@64289
   601
      by blast
hoelzl@64289
   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)"
wenzelm@64911
   603
      using \<open>k \<in> K\<close> by auto
hoelzl@64289
   604
    then show ?case
hoelzl@64289
   605
      by auto
hoelzl@64289
   606
  qed auto
wenzelm@64911
   607
  then show ?thesis using \<open>x \<in> U\<close> by auto
hoelzl@64289
   608
qed
hoelzl@64289
   609
hoelzl@64289
   610
lp15@69030
   611
lemma openin_product_topology:
lp15@69030
   612
   "openin (product_topology X I) =
lp15@69030
   613
    arbitrary union_of
lp15@69030
   614
          ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
lp15@69030
   615
           relative_to topspace (product_topology X I))"
lp15@69030
   616
  apply (subst product_topology)
lp15@69030
   617
  apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])
lp15@69030
   618
  done
lp15@69030
   619
lp15@69030
   620
lemma subtopology_PiE:
lp15@69030
   621
  "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
lp15@69030
   622
proof -
lp15@69030
   623
  let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
lp15@69030
   624
  let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"
lp15@69030
   625
  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
lp15@69030
   626
        finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"
lp15@69030
   627
    by (rule finite_intersection_of_relative_to)
lp15@69030
   628
  also have "\<dots> = finite intersection_of
lp15@69030
   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)
lp15@69030
   630
                       relative_to ?X \<inter> Pi\<^sub>E I S)
lp15@69030
   631
                   relative_to ?X \<inter> Pi\<^sub>E I S"
lp15@69030
   632
    apply (rule arg_cong2 [where f = "(relative_to)"])
lp15@69030
   633
     apply (rule arg_cong [where f = "(intersection_of)finite"])
lp15@69030
   634
     apply (rule ext)
lp15@69030
   635
     apply (auto simp: relative_to_def intersection_of_def)
lp15@69030
   636
    done
lp15@69030
   637
  finally
lp15@69030
   638
  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
lp15@69030
   639
        finite intersection_of
lp15@69030
   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)
lp15@69030
   641
          relative_to ?X \<inter> Pi\<^sub>E I S"
lp15@69030
   642
    by (metis finite_intersection_of_relative_to)
lp15@69030
   643
  then show ?thesis
lp15@69030
   644
  unfolding topology_eq
lp15@69030
   645
  apply clarify
lp15@69030
   646
  apply (simp add: openin_product_topology flip: openin_relative_to)
lp15@69030
   647
  apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)
lp15@69030
   648
  done
lp15@69030
   649
qed
lp15@69030
   650
lp15@69030
   651
lp15@69030
   652
lemma product_topology_base_alt:
lp15@69030
   653
   "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
lp15@69030
   654
    relative_to topspace(product_topology X I) =
lp15@69030
   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))))"
lp15@69030
   656
   (is "?lhs = ?rhs")
lp15@69030
   657
proof -
lp15@69030
   658
  have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"
lp15@69030
   659
    unfolding all_relative_to all_intersection_of topspace_product_topology
lp15@69030
   660
  proof clarify
lp15@69030
   661
    fix \<F>
lp15@69030
   662
    assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
lp15@69030
   663
    then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U \<and>
lp15@69030
   664
          finite {i \<in> I. U i \<noteq> topspace (X i)} \<and> (\<forall>i\<in>I. openin (X i) (U i))"
lp15@69030
   665
    proof (induction)
lp15@69030
   666
      case (insert F \<F>)
lp15@69030
   667
      then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"
lp15@69030
   668
        and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
lp15@69030
   669
        and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"
lp15@69030
   670
        by auto
lp15@69030
   671
      obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"
lp15@69030
   672
        using insert by auto
lp15@69030
   673
      let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
lp15@69030
   674
      show ?case
lp15@69030
   675
      proof (intro exI conjI)
lp15@69030
   676
        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"
lp15@69030
   677
        using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
lp15@69030
   678
      next
lp15@69030
   679
        show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
lp15@69030
   680
          by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
lp15@69030
   681
      next
lp15@69030
   682
        show "\<forall>i\<in>I. openin (X i) (?U i)"
lp15@69030
   683
          by (simp add: \<open>openin (X i) V\<close> ope openin_Int)
lp15@69030
   684
      qed
lp15@69030
   685
    qed (auto intro: dest: not_finite_existsD)
lp15@69030
   686
  qed
lp15@69030
   687
  moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"
lp15@69030
   688
  proof clarify
lp15@69030
   689
    fix U :: "'a \<Rightarrow> 'b set"
lp15@69030
   690
    assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"
lp15@69030
   691
    let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"
lp15@69030
   692
    show "?lhs (Pi\<^sub>E I U)"
lp15@69030
   693
      unfolding relative_to_def topspace_product_topology
lp15@69030
   694
    proof (intro exI conjI)
lp15@69030
   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"
lp15@69030
   696
        using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
lp15@69030
   697
      show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"
lp15@69030
   698
        using ope openin_subset by fastforce
lp15@69030
   699
    qed
lp15@69030
   700
  qed
lp15@69030
   701
  ultimately show ?thesis
lp15@69030
   702
    by meson
lp15@69030
   703
qed
lp15@69030
   704
lp15@69030
   705
lp15@69030
   706
lemma topspace_product_topology_alt:
lp15@69030
   707
   "topspace (product_topology Y I) = {f \<in> extensional I. \<forall>k \<in> I. f k \<in> topspace(Y k)}"
lp15@69030
   708
  by (force simp: product_topology PiE_def)
lp15@69030
   709
lp15@69030
   710
lemma openin_product_topology_alt:
lp15@69030
   711
  "openin (product_topology X I) S \<longleftrightarrow>
lp15@69030
   712
    (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
lp15@69030
   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)"
lp15@69030
   714
  apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto)
lp15@69030
   715
  apply (drule bspec; blast)
lp15@69030
   716
  done
lp15@69030
   717
lp15@69030
   718
wenzelm@64911
   719
text \<open>The basic property of the product topology is the continuity of projections:\<close>
hoelzl@64289
   720
ak2110@68833
   721
lemma%unimportant continuous_on_topo_product_coordinates [simp]:
hoelzl@64289
   722
  assumes "i \<in> I"
hoelzl@64289
   723
  shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
hoelzl@64289
   724
proof -
hoelzl@64289
   725
  {
hoelzl@64289
   726
    fix U assume "openin (T i) U"
hoelzl@64289
   727
    define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
hoelzl@64289
   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)"
wenzelm@64911
   729
      unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]
hoelzl@64289
   730
      by (auto simp add: PiE_iff, auto, metis subsetCE)
hoelzl@64289
   731
    have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
wenzelm@64911
   732
      unfolding X_def using \<open>openin (T i) U\<close> by auto
hoelzl@64289
   733
    have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
hoelzl@64289
   734
      unfolding product_topology_def
hoelzl@64289
   735
      apply (rule topology_generated_by_Basis)
hoelzl@64289
   736
      apply (subst *)
hoelzl@64289
   737
      using ** by auto
hoelzl@64289
   738
  }
hoelzl@64289
   739
  then show ?thesis unfolding continuous_on_topo_def
lp15@69030
   740
    by (auto simp add: assms topspace_product_topology PiE_iff)
hoelzl@64289
   741
qed
hoelzl@64289
   742
ak2110@68833
   743
lemma%important continuous_on_topo_coordinatewise_then_product [intro]:
hoelzl@64289
   744
  assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
hoelzl@64289
   745
          "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
hoelzl@64289
   746
  shows "continuous_on_topo T1 (product_topology T I) f"
hoelzl@64289
   747
unfolding product_topology_def
ak2110@68833
   748
proof%unimportant (rule continuous_on_generated_topo)
hoelzl@64289
   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)}}"
hoelzl@64289
   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)}"
hoelzl@64289
   751
    by blast
hoelzl@64289
   752
  define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
hoelzl@64289
   753
  have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
hoelzl@64289
   754
  have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
hoelzl@64289
   755
    using that assms(1) by (simp add: continuous_on_topo_preimage_topspace)
hoelzl@64289
   756
  then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
hoelzl@64289
   757
    using that unfolding J_def by auto
hoelzl@64289
   758
  have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
hoelzl@64289
   759
    by (subst H(1), auto simp add: PiE_iff assms)
hoelzl@64289
   760
  also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
wenzelm@64911
   761
    using * \<open>J \<subseteq> I\<close> by auto
hoelzl@64289
   762
  also have "openin T1 (...)"
hoelzl@64289
   763
    apply (rule openin_INT)
wenzelm@64911
   764
    apply (simp add: \<open>finite J\<close>)
wenzelm@64911
   765
    using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
hoelzl@64289
   766
  ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
hoelzl@64289
   767
next
hoelzl@64289
   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)}}"
hoelzl@64289
   769
    apply (subst topology_generated_by_topspace[symmetric])
hoelzl@64289
   770
    apply (subst product_topology_def[symmetric])
lp15@69030
   771
    apply (simp only: topspace_product_topology)
hoelzl@64289
   772
    apply (auto simp add: PiE_iff)
hoelzl@64289
   773
    using assms unfolding continuous_on_topo_def by auto
hoelzl@64289
   774
qed
hoelzl@64289
   775
ak2110@68833
   776
lemma%unimportant continuous_on_topo_product_then_coordinatewise [intro]:
hoelzl@64289
   777
  assumes "continuous_on_topo T1 (product_topology T I) f"
hoelzl@64289
   778
  shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
hoelzl@64289
   779
        "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
hoelzl@64289
   780
proof -
hoelzl@64289
   781
  fix i assume "i \<in> I"
hoelzl@64289
   782
  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
hoelzl@64289
   783
  also have "continuous_on_topo T1 (T i) (...)"
hoelzl@64289
   784
    apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
wenzelm@64911
   785
    using assms \<open>i \<in> I\<close> by auto
hoelzl@64289
   786
  ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
hoelzl@64289
   787
    by simp
hoelzl@64289
   788
next
hoelzl@64289
   789
  fix i x assume "i \<notin> I" "x \<in> topspace T1"
hoelzl@64289
   790
  have "f x \<in> topspace (product_topology T I)"
wenzelm@64911
   791
    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
hoelzl@64289
   792
  then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
lp15@69030
   793
    using topspace_product_topology by metis
hoelzl@64289
   794
  then show "f x i = undefined"
wenzelm@64911
   795
    using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
hoelzl@64289
   796
qed
hoelzl@64289
   797
ak2110@68833
   798
lemma%unimportant continuous_on_restrict:
hoelzl@64289
   799
  assumes "J \<subseteq> I"
hoelzl@64289
   800
  shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
hoelzl@64289
   801
proof (rule continuous_on_topo_coordinatewise_then_product)
hoelzl@64289
   802
  fix i assume "i \<in> J"
hoelzl@64289
   803
  then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
hoelzl@64289
   804
  then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
wenzelm@64911
   805
    using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
hoelzl@64289
   806
next
hoelzl@64289
   807
  fix i assume "i \<notin> J"
hoelzl@64289
   808
  then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
hoelzl@64289
   809
    unfolding restrict_def by auto
hoelzl@64289
   810
qed
hoelzl@64289
   811
hoelzl@64289
   812
ak2110@68833
   813
subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
hoelzl@64289
   814
hoelzl@64289
   815
instantiation "fun" :: (type, topological_space) topological_space
hoelzl@64289
   816
begin
hoelzl@64289
   817
ak2110@68833
   818
definition%important open_fun_def:
hoelzl@64289
   819
  "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
hoelzl@64289
   820
ak2110@68833
   821
instance proof%unimportant
hoelzl@64289
   822
  have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
lp15@69030
   823
    unfolding topspace_product_topology topspace_euclidean by auto
hoelzl@64289
   824
  then show "open (UNIV::('a \<Rightarrow> 'b) set)"
hoelzl@64289
   825
    unfolding open_fun_def by (metis openin_topspace)
hoelzl@64289
   826
qed (auto simp add: open_fun_def)
hoelzl@64289
   827
hoelzl@64289
   828
end
hoelzl@64289
   829
ak2110@68833
   830
lemma%unimportant euclidean_product_topology:
hoelzl@64289
   831
  "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
hoelzl@64289
   832
by (metis open_openin topology_eq open_fun_def)
hoelzl@64289
   833
ak2110@68833
   834
lemma%important product_topology_basis':
hoelzl@64289
   835
  fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
hoelzl@64289
   836
  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
hoelzl@64289
   837
  shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
ak2110@68833
   838
proof%unimportant -
hoelzl@64289
   839
  define J where "J = x`I"
hoelzl@64289
   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)"
hoelzl@64289
   841
  define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
hoelzl@64289
   842
  have *: "open (X i)" for i
hoelzl@64289
   843
    unfolding X_def V_def using assms by auto
hoelzl@64289
   844
  have **: "finite {i. X i \<noteq> UNIV}"
hoelzl@64289
   845
    unfolding X_def V_def J_def using assms(1) by auto
hoelzl@64289
   846
  have "open (Pi\<^sub>E UNIV X)"
hoelzl@64289
   847
    unfolding open_fun_def apply (rule product_topology_basis)
hoelzl@64289
   848
    using * ** unfolding open_openin topspace_euclidean by auto
hoelzl@64289
   849
  moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
hoelzl@64289
   850
    apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
hoelzl@64289
   851
    proof (auto)
hoelzl@64289
   852
      fix f :: "'a \<Rightarrow> 'b" and i :: 'i
hoelzl@64289
   853
      assume a1: "i \<in> I"
hoelzl@64289
   854
      assume a2: "\<forall>i. f i \<in> (if i \<in> x`I then if i \<in> x`I then \<Inter>{U ia |ia. ia \<in> I \<and> x ia = i} else UNIV else UNIV)"
hoelzl@64289
   855
      have f3: "x i \<in> x`I"
hoelzl@64289
   856
        using a1 by blast
hoelzl@64289
   857
      have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
hoelzl@64289
   858
        using a1 by blast
hoelzl@64289
   859
      then show "f (x i) \<in> U i"
hoelzl@64289
   860
        using f3 a2 by (meson Inter_iff)
hoelzl@64289
   861
    qed
hoelzl@64289
   862
  ultimately show ?thesis by simp
hoelzl@64289
   863
qed
hoelzl@64289
   864
wenzelm@64911
   865
text \<open>The results proved in the general situation of products of possibly different
wenzelm@64911
   866
spaces have their counterparts in this simpler setting.\<close>
hoelzl@64289
   867
ak2110@68833
   868
lemma%unimportant continuous_on_product_coordinates [simp]:
hoelzl@64289
   869
  "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
hoelzl@64289
   870
unfolding continuous_on_topo_UNIV euclidean_product_topology
hoelzl@64289
   871
by (rule continuous_on_topo_product_coordinates, simp)
hoelzl@64289
   872
ak2110@68833
   873
lemma%unimportant continuous_on_coordinatewise_then_product [intro, continuous_intros]:
hoelzl@64289
   874
  assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
hoelzl@64289
   875
  shows "continuous_on UNIV f"
hoelzl@64289
   876
using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
hoelzl@64289
   877
by (rule continuous_on_topo_coordinatewise_then_product, simp)
hoelzl@64289
   878
ak2110@68833
   879
lemma%unimportant continuous_on_product_then_coordinatewise:
hoelzl@64289
   880
  assumes "continuous_on UNIV f"
hoelzl@64289
   881
  shows "continuous_on UNIV (\<lambda>x. f x i)"
hoelzl@64289
   882
using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
hoelzl@64289
   883
by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
hoelzl@64289
   884
ak2110@68833
   885
lemma%unimportant continuous_on_product_coordinatewise_iff:
hoelzl@64289
   886
  "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
hoelzl@64289
   887
by (auto intro: continuous_on_product_then_coordinatewise)
hoelzl@64289
   888
ak2110@68833
   889
subsubsection%important \<open>Topological countability for product spaces\<close>
hoelzl@64289
   890
wenzelm@64911
   891
text \<open>The next two lemmas are useful to prove first or second countability
hoelzl@64289
   892
of product spaces, but they have more to do with countability and could
wenzelm@64911
   893
be put in the corresponding theory.\<close>
hoelzl@64289
   894
ak2110@68833
   895
lemma%unimportant countable_nat_product_event_const:
hoelzl@64289
   896
  fixes F::"'a set" and a::'a
hoelzl@64289
   897
  assumes "a \<in> F" "countable F"
hoelzl@64289
   898
  shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
hoelzl@64289
   899
proof -
hoelzl@64289
   900
  have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}
hoelzl@64289
   901
                  \<subseteq> (\<Union>N. {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)})"
hoelzl@64289
   902
    using infinite_nat_iff_unbounded_le by fastforce
hoelzl@64289
   903
  have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat
hoelzl@64289
   904
  proof (induction N)
hoelzl@64289
   905
    case 0
hoelzl@64289
   906
    have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
wenzelm@64911
   907
      using \<open>a \<in> F\<close> by auto
hoelzl@64289
   908
    then show ?case by auto
hoelzl@64289
   909
  next
hoelzl@64289
   910
    case (Suc N)
hoelzl@64289
   911
    define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
hoelzl@64289
   912
      where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
hoelzl@64289
   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)"
hoelzl@64289
   914
    proof (auto)
hoelzl@64289
   915
      fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
hoelzl@64289
   916
      define y where "y = (\<lambda>i. if i = N then a else x i)"
hoelzl@64289
   917
      have "f (y, x N) = x"
hoelzl@64289
   918
        unfolding f_def y_def by auto
hoelzl@64289
   919
      moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
wenzelm@64911
   920
        unfolding y_def using H \<open>a \<in> F\<close> by auto
hoelzl@64289
   921
      ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
hoelzl@64289
   922
        by (metis (no_types, lifting) image_eqI)
hoelzl@64289
   923
    qed
hoelzl@64289
   924
    moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
hoelzl@64289
   925
      using Suc.IH assms(2) by auto
hoelzl@64289
   926
    ultimately show ?case
hoelzl@64289
   927
      by (meson countable_image countable_subset)
hoelzl@64289
   928
  qed
hoelzl@64289
   929
  then show ?thesis using countable_subset[OF *] by auto
hoelzl@64289
   930
qed
hoelzl@64289
   931
ak2110@68833
   932
lemma%unimportant countable_product_event_const:
hoelzl@64289
   933
  fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
hoelzl@64289
   934
  assumes "\<And>i. countable (F i)"
hoelzl@64289
   935
  shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
hoelzl@64289
   936
proof -
hoelzl@64289
   937
  define G where "G = (\<Union>i. F i) \<union> {b}"
hoelzl@64289
   938
  have "countable G" unfolding G_def using assms by auto
hoelzl@64289
   939
  have "b \<in> G" unfolding G_def by auto
hoelzl@64289
   940
  define pi where "pi = (\<lambda>(x::(nat \<Rightarrow> 'b)). (\<lambda> i::'a. x ((to_nat::('a \<Rightarrow> nat)) i)))"
hoelzl@64289
   941
  have "{f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}
hoelzl@64289
   942
        \<subseteq> pi`{g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
hoelzl@64289
   943
  proof (auto)
hoelzl@64289
   944
    fix f assume H: "\<forall>i. f i \<in> F i" "finite {i. f i \<noteq> b}"
hoelzl@64289
   945
    define I where "I = {i. f i \<noteq> b}"
hoelzl@64289
   946
    define g where "g = (\<lambda>j. if j \<in> to_nat`I then f (from_nat j) else b)"
hoelzl@64289
   947
    have "{j. g j \<noteq> b} \<subseteq> to_nat`I" unfolding g_def by auto
hoelzl@64289
   948
    then have "finite {j. g j \<noteq> b}"
hoelzl@64289
   949
      unfolding I_def using H(2) using finite_surj by blast
hoelzl@64289
   950
    moreover have "g j \<in> G" for j
hoelzl@64289
   951
      unfolding g_def G_def using H by auto
hoelzl@64289
   952
    ultimately have "g \<in> {g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
hoelzl@64289
   953
      by auto
hoelzl@64289
   954
    moreover have "f = pi g"
hoelzl@64289
   955
      unfolding pi_def g_def I_def using H by fastforce
hoelzl@64289
   956
    ultimately show "f \<in> pi`{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"
hoelzl@64289
   957
      by auto
hoelzl@64289
   958
  qed
hoelzl@64289
   959
  then show ?thesis
wenzelm@64911
   960
    using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]
hoelzl@64289
   961
    by (meson countable_image countable_subset)
hoelzl@64289
   962
qed
hoelzl@64289
   963
hoelzl@64289
   964
instance "fun" :: (countable, first_countable_topology) first_countable_topology
ak2110@68833
   965
proof%unimportant
hoelzl@64289
   966
  fix x::"'a \<Rightarrow> 'b"
hoelzl@64289
   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))"
hoelzl@64289
   968
    apply (rule choice) using first_countable_basis by auto
hoelzl@64289
   969
  then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
hoelzl@64289
   970
                                                  "\<And>x i. open (A x i)"
hoelzl@64289
   971
                                                  "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
hoelzl@64289
   972
    by metis
wenzelm@64911
   973
  text \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>
hoelzl@64289
   974
  define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
hoelzl@64289
   975
  have "countable (B i)" for i unfolding B_def by auto
hoelzl@64289
   976
hoelzl@64289
   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}}"
hoelzl@64289
   978
  have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
hoelzl@64289
   979
    unfolding K_def B_def by auto
hoelzl@64289
   980
  then have "K \<noteq> {}" by auto
hoelzl@64289
   981
  have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
wenzelm@64911
   982
    apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
hoelzl@64289
   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}}"
hoelzl@64289
   984
    unfolding K_def by auto
hoelzl@64289
   985
  ultimately have "countable K" by auto
hoelzl@64289
   986
  have "x \<in> k" if "k \<in> K" for k
hoelzl@64289
   987
    using that unfolding K_def B_def apply auto using A(1) by auto
hoelzl@64289
   988
  have "open k" if "k \<in> K" for k
hoelzl@64289
   989
    using that unfolding open_fun_def K_def B_def apply (auto)
hoelzl@64289
   990
    apply (rule product_topology_basis)
hoelzl@64289
   991
    unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))
hoelzl@64289
   992
hoelzl@64289
   993
  have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
hoelzl@64289
   994
  proof -
hoelzl@64289
   995
    have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
wenzelm@64911
   996
      using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
hoelzl@64289
   997
    with product_topology_open_contains_basis[OF this]
hoelzl@64289
   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"
hoelzl@64289
   999
      unfolding topspace_euclidean open_openin by simp
hoelzl@64289
  1000
    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
hoelzl@64289
  1001
                           "\<And>i. open (X i)"
hoelzl@64289
  1002
                           "finite {i. X i \<noteq> UNIV}"
hoelzl@64289
  1003
                           "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
hoelzl@64289
  1004
      by auto
hoelzl@64289
  1005
    define I where "I = {i. X i \<noteq> UNIV}"
hoelzl@64289
  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)"
hoelzl@64289
  1007
    have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
hoelzl@64289
  1008
      unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
hoelzl@64289
  1009
    have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
hoelzl@64289
  1010
      apply (cases "i \<in> I")
hoelzl@64289
  1011
      unfolding Y_def using * that apply (auto)
hoelzl@64289
  1012
      apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
hoelzl@64289
  1013
      unfolding B_def apply simp
hoelzl@64289
  1014
      unfolding I_def apply auto
hoelzl@64289
  1015
      done
hoelzl@64289
  1016
    have "{i. Y i \<noteq> UNIV} \<subseteq> I"
hoelzl@64289
  1017
      unfolding Y_def by auto
hoelzl@64289
  1018
    then have ***: "finite {i. Y i \<noteq> UNIV}"
hoelzl@64289
  1019
      unfolding I_def using H(3) rev_finite_subset by blast
hoelzl@64289
  1020
    have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
hoelzl@64289
  1021
      using ** *** by auto
hoelzl@64289
  1022
    then have "Pi\<^sub>E UNIV Y \<in> K"
hoelzl@64289
  1023
      unfolding K_def by auto
hoelzl@64289
  1024
hoelzl@64289
  1025
    have "Y i \<subseteq> X i" for i
hoelzl@64289
  1026
      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
hoelzl@64289
  1027
    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
hoelzl@64289
  1028
    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
wenzelm@64911
  1029
    then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
hoelzl@64289
  1030
  qed
hoelzl@64289
  1031
hoelzl@64289
  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))"
hoelzl@64289
  1033
    apply (rule first_countableI[of K])
wenzelm@64911
  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
hoelzl@64289
  1035
qed
hoelzl@64289
  1036
ak2110@68833
  1037
lemma%important product_topology_countable_basis:
hoelzl@64289
  1038
  shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
hoelzl@64289
  1039
          topological_basis K \<and> countable K \<and>
wenzelm@64910
  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})"
ak2110@68833
  1041
proof%unimportant -
hoelzl@64289
  1042
  obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
hoelzl@64289
  1043
    using ex_countable_basis by auto
hoelzl@64289
  1044
  then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
hoelzl@64289
  1045
  define B2 where "B2 = B \<union> {UNIV}"
hoelzl@64289
  1046
  have "countable B2"
hoelzl@64289
  1047
    unfolding B2_def using B by auto
hoelzl@64289
  1048
  have "open U" if "U \<in> B2" for U
hoelzl@64289
  1049
    using that unfolding B2_def using B topological_basis_open by auto
hoelzl@64289
  1050
hoelzl@64289
  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}}"
wenzelm@64910
  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}"
wenzelm@64911
  1053
    unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
hoelzl@64289
  1054
hoelzl@64289
  1055
  have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
wenzelm@64911
  1056
    apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
hoelzl@64289
  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}}"
hoelzl@64289
  1058
    unfolding K_def by auto
hoelzl@64289
  1059
  ultimately have ii: "countable K" by auto
hoelzl@64289
  1060
hoelzl@64289
  1061
  have iii: "topological_basis K"
hoelzl@64289
  1062
  proof (rule topological_basisI)
hoelzl@64289
  1063
    fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
hoelzl@64289
  1064
    then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
hoelzl@64289
  1065
      unfolding open_fun_def by auto
wenzelm@64911
  1066
    with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
hoelzl@64289
  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"
hoelzl@64289
  1068
      unfolding topspace_euclidean open_openin by simp
hoelzl@64289
  1069
    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
hoelzl@64289
  1070
                           "\<And>i. open (X i)"
hoelzl@64289
  1071
                           "finite {i. X i \<noteq> UNIV}"
hoelzl@64289
  1072
                           "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
hoelzl@64289
  1073
      by auto
hoelzl@64289
  1074
    then have "x i \<in> X i" for i by auto
hoelzl@64289
  1075
    define I where "I = {i. X i \<noteq> UNIV}"
hoelzl@64289
  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)"
hoelzl@64289
  1077
    have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
wenzelm@64911
  1078
      unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
hoelzl@64289
  1079
    have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
hoelzl@64289
  1080
      using someI_ex[OF *]
hoelzl@64289
  1081
      apply (cases "i \<in> I")
hoelzl@64289
  1082
      unfolding Y_def using * apply (auto)
hoelzl@64289
  1083
      unfolding B2_def I_def by auto
hoelzl@64289
  1084
    have "{i. Y i \<noteq> UNIV} \<subseteq> I"
hoelzl@64289
  1085
      unfolding Y_def by auto
hoelzl@64289
  1086
    then have ***: "finite {i. Y i \<noteq> UNIV}"
hoelzl@64289
  1087
      unfolding I_def using H(3) rev_finite_subset by blast
hoelzl@64289
  1088
    have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
hoelzl@64289
  1089
      using ** *** by auto
hoelzl@64289
  1090
    then have "Pi\<^sub>E UNIV Y \<in> K"
hoelzl@64289
  1091
      unfolding K_def by auto
hoelzl@64289
  1092
hoelzl@64289
  1093
    have "Y i \<subseteq> X i" for i
hoelzl@64289
  1094
      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
hoelzl@64289
  1095
    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
hoelzl@64289
  1096
    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
hoelzl@64289
  1097
hoelzl@64289
  1098
    have "x \<in> Pi\<^sub>E UNIV Y"
hoelzl@64289
  1099
      using ** by auto
hoelzl@64289
  1100
hoelzl@64289
  1101
    show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
wenzelm@64911
  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
hoelzl@64289
  1103
  next
hoelzl@64289
  1104
    fix U assume "U \<in> K"
hoelzl@64289
  1105
    show "open U"
wenzelm@64911
  1106
      using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
hoelzl@64289
  1107
      apply (rule product_topology_basis)
wenzelm@64911
  1108
      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV unfolding topspace_euclidean open_openin[symmetric]
hoelzl@64289
  1109
      by auto
hoelzl@64289
  1110
  qed
hoelzl@64289
  1111
hoelzl@64289
  1112
  show ?thesis using i ii iii by auto
hoelzl@64289
  1113
qed
hoelzl@64289
  1114
hoelzl@64289
  1115
instance "fun" :: (countable, second_countable_topology) second_countable_topology
hoelzl@64289
  1116
  apply standard
hoelzl@64289
  1117
  using product_topology_countable_basis topological_basis_imp_subbasis by auto
hoelzl@64289
  1118
hoelzl@64289
  1119
ak2110@68833
  1120
subsection%important \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
hoelzl@64289
  1121
wenzelm@64911
  1122
text \<open>Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
hoelzl@64289
  1123
operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
hoelzl@64289
  1124
(the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
hoelzl@64289
  1125
hoelzl@64289
  1126
However, there is another topology on this space, the strong operator topology, where $T_n$ tends to
hoelzl@64289
  1127
$T$ iff, for all $x$ in 'a, then $T_n x$ tends to $T x$. This is precisely the product topology
hoelzl@64289
  1128
where the target space is endowed with the norm topology. It is especially useful when 'b is the set
hoelzl@64289
  1129
of real numbers, since then this topology is compact.
hoelzl@64289
  1130
hoelzl@64289
  1131
We can not implement it using type classes as there is already a topology, but at least we
hoelzl@64289
  1132
can define it as a topology.
hoelzl@64289
  1133
hoelzl@64289
  1134
Note that there is yet another (common and useful) topology on operator spaces, the weak operator
hoelzl@64289
  1135
topology, defined analogously using the product topology, but where the target space is given the
hoelzl@64289
  1136
weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
hoelzl@64289
  1137
canonical embedding of a space into its bidual. We do not define it there, although it could also be
hoelzl@64289
  1138
defined analogously.
wenzelm@64911
  1139
\<close>
hoelzl@64289
  1140
ak2110@68833
  1141
definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
hoelzl@64289
  1142
where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
hoelzl@64289
  1143
ak2110@68833
  1144
lemma%unimportant strong_operator_topology_topspace:
hoelzl@64289
  1145
  "topspace strong_operator_topology = UNIV"
hoelzl@64289
  1146
unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
hoelzl@64289
  1147
ak2110@68833
  1148
lemma%important strong_operator_topology_basis:
hoelzl@64289
  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"
hoelzl@64289
  1150
  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
hoelzl@64289
  1151
  shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
ak2110@68833
  1152
proof%unimportant -
hoelzl@64289
  1153
  have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
hoelzl@64289
  1154
    by (rule product_topology_basis'[OF assms])
hoelzl@64289
  1155
  moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
hoelzl@64289
  1156
                = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
hoelzl@64289
  1157
    by auto
hoelzl@64289
  1158
  ultimately show ?thesis
hoelzl@64289
  1159
    unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto
hoelzl@64289
  1160
qed
hoelzl@64289
  1161
ak2110@68833
  1162
lemma%important strong_operator_topology_continuous_evaluation:
hoelzl@64289
  1163
  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
ak2110@68833
  1164
proof%unimportant -
hoelzl@64289
  1165
  have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
hoelzl@64289
  1166
    unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
hoelzl@64289
  1167
    using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
hoelzl@64289
  1168
  then show ?thesis unfolding comp_def by simp
hoelzl@64289
  1169
qed
hoelzl@64289
  1170
ak2110@68833
  1171
lemma%unimportant continuous_on_strong_operator_topo_iff_coordinatewise:
hoelzl@64289
  1172
  "continuous_on_topo T strong_operator_topology f
hoelzl@64289
  1173
    \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
hoelzl@64289
  1174
proof (auto)
hoelzl@64289
  1175
  fix x::"'b"
hoelzl@64289
  1176
  assume "continuous_on_topo T strong_operator_topology f"
hoelzl@64289
  1177
  with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
hoelzl@64289
  1178
  have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
hoelzl@64289
  1179
    by simp
hoelzl@64289
  1180
  then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
hoelzl@64289
  1181
    unfolding comp_def by auto
hoelzl@64289
  1182
next
hoelzl@64289
  1183
  assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
hoelzl@64289
  1184
  have "continuous_on_topo T euclidean (blinfun_apply o f)"
hoelzl@64289
  1185
    unfolding euclidean_product_topology
hoelzl@64289
  1186
    apply (rule continuous_on_topo_coordinatewise_then_product, auto)
hoelzl@64289
  1187
    using * unfolding comp_def by auto
hoelzl@64289
  1188
  show "continuous_on_topo T strong_operator_topology f"
hoelzl@64289
  1189
    unfolding strong_operator_topology_def
hoelzl@64289
  1190
    apply (rule continuous_on_topo_pullback')
wenzelm@64911
  1191
    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
hoelzl@64289
  1192
qed
hoelzl@64289
  1193
ak2110@68833
  1194
lemma%important strong_operator_topology_weaker_than_euclidean:
hoelzl@64289
  1195
  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
ak2110@68833
  1196
by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise,
hoelzl@64289
  1197
    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
hoelzl@64289
  1198
hoelzl@64289
  1199
ak2110@68833
  1200
subsection%important \<open>Metrics on product spaces\<close>
hoelzl@64289
  1201
hoelzl@64289
  1202
wenzelm@64911
  1203
text \<open>In general, the product topology is not metrizable, unless the index set is countable.
hoelzl@64289
  1204
When the index set is countable, essentially any (convergent) combination of the metrics on the
hoelzl@64289
  1205
factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
hoelzl@64289
  1206
for instance.
hoelzl@64289
  1207
hoelzl@64289
  1208
What is not completely trivial is that the distance thus defined induces the same topology
hoelzl@64289
  1209
as the product topology. This is what we have to prove to show that we have an instance
hoelzl@64289
  1210
of \verb+metric_space+.
hoelzl@64289
  1211
hoelzl@64289
  1212
The proofs below would work verbatim for general countable products of metric spaces. However,
hoelzl@64289
  1213
since distances are only implemented in terms of type classes, we only develop the theory
wenzelm@64911
  1214
for countable products of the same space.\<close>
hoelzl@64289
  1215
hoelzl@64289
  1216
instantiation "fun" :: (countable, metric_space) metric_space
hoelzl@64289
  1217
begin
hoelzl@64289
  1218
ak2110@68833
  1219
definition%important dist_fun_def:
hoelzl@64289
  1220
  "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
  1221
ak2110@68833
  1222
definition%important uniformity_fun_def:
haftmann@69260
  1223
  "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
hoelzl@64289
  1224
wenzelm@64911
  1225
text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
hoelzl@64289
  1226
instance: once it is proved, they become trivial consequences of the general theory of metric
hoelzl@64289
  1227
spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
wenzelm@64911
  1228
to do this.\<close>
hoelzl@64289
  1229
ak2110@68833
  1230
lemma%important dist_fun_le_dist_first_terms:
hoelzl@64289
  1231
  "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
ak2110@68833
  1232
proof%unimportant -
hoelzl@64289
  1233
  have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
hoelzl@64289
  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))"
hoelzl@64289
  1235
    by (rule suminf_cong, simp add: power_add)
hoelzl@64289
  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)"
hoelzl@64289
  1237
    apply (rule suminf_mult)
hoelzl@64289
  1238
    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1239
  also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"
hoelzl@64289
  1240
    apply (simp, rule suminf_le, simp)
hoelzl@64289
  1241
    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1242
  also have "... = (1/2)^(Suc N) * 2"
hoelzl@64289
  1243
    using suminf_geometric[of "1/2"] by auto
hoelzl@64289
  1244
  also have "... = (1/2)^N"
hoelzl@64289
  1245
    by auto
hoelzl@64289
  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"
hoelzl@64289
  1247
    by simp
hoelzl@64289
  1248
hoelzl@64289
  1249
  define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"
hoelzl@64289
  1250
  have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"
hoelzl@64289
  1251
    unfolding M_def by (rule Max_ge, auto)
hoelzl@64289
  1252
  then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)
hoelzl@64289
  1253
  have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n
hoelzl@64289
  1254
    unfolding M_def apply (rule Max_ge) using that by auto
hoelzl@64289
  1255
  then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n
hoelzl@64289
  1256
    using that by force
hoelzl@64289
  1257
  have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>
hoelzl@64289
  1258
      (\<Sum>n< Suc N. M * (1 / 2) ^ n)"
hoelzl@64289
  1259
    by (rule sum_mono, simp add: i)
hoelzl@64289
  1260
  also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"
hoelzl@64289
  1261
    by (rule sum_distrib_left[symmetric])
hoelzl@64289
  1262
  also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"
hoelzl@64289
  1263
    by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)
hoelzl@64289
  1264
  also have "... = M * 2"
hoelzl@64289
  1265
    using suminf_geometric[of "1/2"] by auto
hoelzl@64289
  1266
  finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"
hoelzl@64289
  1267
    by simp
hoelzl@64289
  1268
hoelzl@64289
  1269
  have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
  1270
    unfolding dist_fun_def by simp
hoelzl@64289
  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)
hoelzl@64289
  1272
                  + (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
  1273
    apply (rule suminf_split_initial_segment)
hoelzl@64289
  1274
    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1275
  also have "... \<le> 2 * M + (1/2)^N"
hoelzl@64289
  1276
    using * ** by auto
hoelzl@64289
  1277
  finally show ?thesis unfolding M_def by simp
hoelzl@64289
  1278
qed
hoelzl@64289
  1279
ak2110@68833
  1280
lemma%unimportant open_fun_contains_ball_aux:
hoelzl@64289
  1281
  assumes "open (U::(('a \<Rightarrow> 'b) set))"
hoelzl@64289
  1282
          "x \<in> U"
hoelzl@64289
  1283
  shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
hoelzl@64289
  1284
proof -
hoelzl@64289
  1285
  have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
hoelzl@64289
  1286
    using open_fun_def assms by auto
hoelzl@64289
  1287
  obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
hoelzl@64289
  1288
                    "\<And>i. openin euclidean (X i)"
hoelzl@64289
  1289
                    "finite {i. X i \<noteq> topspace euclidean}"
hoelzl@64289
  1290
                    "x \<in> Pi\<^sub>E UNIV X"
wenzelm@64911
  1291
    using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
hoelzl@64289
  1292
  define I where "I = {i. X i \<noteq> topspace euclidean}"
hoelzl@64289
  1293
  have "finite I" unfolding I_def using H(3) by auto
hoelzl@64289
  1294
  {
hoelzl@64289
  1295
    fix i
wenzelm@64911
  1296
    have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
hoelzl@64289
  1297
    then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
wenzelm@64911
  1298
      using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
hoelzl@64289
  1299
    then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
hoelzl@64289
  1300
    define f where "f = min e (1/2)"
wenzelm@64911
  1301
    have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
wenzelm@64911
  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
hoelzl@64289
  1303
    ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
hoelzl@64289
  1304
  } note * = this
hoelzl@64289
  1305
  have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
hoelzl@64289
  1306
    by (rule choice, auto simp add: *)
hoelzl@64289
  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"
hoelzl@64289
  1308
    by blast
hoelzl@64289
  1309
  define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
hoelzl@64289
  1310
  have "m > 0" if "I\<noteq>{}"
lp15@65036
  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
hoelzl@64289
  1312
  moreover have "{y. dist x y < m} \<subseteq> U"
hoelzl@64289
  1313
  proof (auto)
hoelzl@64289
  1314
    fix y assume "dist x y < m"
hoelzl@64289
  1315
    have "y i \<in> X i" if "i \<in> I" for i
hoelzl@64289
  1316
    proof -
hoelzl@64289
  1317
      have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
  1318
        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1319
      define n where "n = to_nat i"
hoelzl@64289
  1320
      have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
wenzelm@64911
  1321
        using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
hoelzl@64289
  1322
      then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
wenzelm@64911
  1323
        using \<open>n = to_nat i\<close> by auto
hoelzl@64289
  1324
      also have "... \<le> (1/2)^(to_nat i) * e i"
wenzelm@64911
  1325
        unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
hoelzl@64289
  1326
      ultimately have "min (dist (x i) (y i)) 1 < e i"
hoelzl@64289
  1327
        by (auto simp add: divide_simps)
hoelzl@64289
  1328
      then have "dist (x i) (y i) < e i"
wenzelm@64911
  1329
        using \<open>e i < 1\<close> by auto
wenzelm@64911
  1330
      then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
hoelzl@64289
  1331
    qed
hoelzl@64289
  1332
    then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
wenzelm@64911
  1333
    then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
hoelzl@64289
  1334
  qed
hoelzl@64289
  1335
  ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
hoelzl@64289
  1336
hoelzl@64289
  1337
  have "U = UNIV" if "I = {}"
hoelzl@64289
  1338
    using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
hoelzl@64289
  1339
  then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
hoelzl@64289
  1340
  then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
hoelzl@64289
  1341
qed
hoelzl@64289
  1342
ak2110@68833
  1343
lemma%unimportant ball_fun_contains_open_aux:
hoelzl@64289
  1344
  fixes x::"('a \<Rightarrow> 'b)" and e::real
hoelzl@64289
  1345
  assumes "e>0"
hoelzl@64289
  1346
  shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
hoelzl@64289
  1347
proof -
hoelzl@64289
  1348
  have "\<exists>N::nat. 2^N > 8/e"
hoelzl@64289
  1349
    by (simp add: real_arch_pow)
hoelzl@64289
  1350
  then obtain N::nat where "2^N > 8/e" by auto
hoelzl@64289
  1351
  define f where "f = e/4"
hoelzl@64289
  1352
  have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto
hoelzl@64289
  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)"
hoelzl@64289
  1354
  have "{i. X i \<noteq> UNIV} \<subseteq> from_nat`{0..N}"
hoelzl@64289
  1355
    unfolding X_def by auto
hoelzl@64289
  1356
  then have "finite {i. X i \<noteq> topspace euclidean}"
hoelzl@64289
  1357
    unfolding topspace_euclidean using finite_surj by blast
hoelzl@64289
  1358
  have "\<And>i. open (X i)"
hoelzl@64289
  1359
    unfolding X_def using metric_space_class.open_ball open_UNIV by auto
hoelzl@64289
  1360
  then have "\<And>i. openin euclidean (X i)"
hoelzl@64289
  1361
    using open_openin by auto
hoelzl@64289
  1362
  define U where "U = Pi\<^sub>E UNIV X"
hoelzl@64289
  1363
  have "open U"
hoelzl@64289
  1364
    unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
wenzelm@64911
  1365
    unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
hoelzl@64289
  1366
    by auto
hoelzl@64289
  1367
  moreover have "x \<in> U"
hoelzl@64289
  1368
    unfolding U_def X_def by (auto simp add: PiE_iff)
hoelzl@64289
  1369
  moreover have "dist x y < e" if "y \<in> U" for y
hoelzl@64289
  1370
  proof -
hoelzl@64289
  1371
    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
wenzelm@64911
  1372
      using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
hoelzl@64289
  1373
      unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
hoelzl@64289
  1374
    have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
hoelzl@64289
  1375
      apply (rule Max.boundedI) using * by auto
hoelzl@64289
  1376
hoelzl@64289
  1377
    have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
hoelzl@64289
  1378
      by (rule dist_fun_le_dist_first_terms)
hoelzl@64289
  1379
    also have "... \<le> 2 * f + e / 8"
wenzelm@64911
  1380
      apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps divide_simps)
hoelzl@64289
  1381
    also have "... \<le> e/2 + e/8"
hoelzl@64289
  1382
      unfolding f_def by auto
hoelzl@64289
  1383
    also have "... < e"
hoelzl@64289
  1384
      by auto
hoelzl@64289
  1385
    finally show "dist x y < e" by simp
hoelzl@64289
  1386
  qed
hoelzl@64289
  1387
  ultimately show ?thesis by auto
hoelzl@64289
  1388
qed
hoelzl@64289
  1389
ak2110@68833
  1390
lemma%unimportant fun_open_ball_aux:
hoelzl@64289
  1391
  fixes U::"('a \<Rightarrow> 'b) set"
hoelzl@64289
  1392
  shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
hoelzl@64289
  1393
proof (auto)
hoelzl@64289
  1394
  assume "open U"
hoelzl@64289
  1395
  fix x assume "x \<in> U"
hoelzl@64289
  1396
  then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
wenzelm@64911
  1397
    using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
hoelzl@64289
  1398
next
hoelzl@64289
  1399
  assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
hoelzl@64289
  1400
  define K where "K = {V. open V \<and> V \<subseteq> U}"
hoelzl@64289
  1401
  {
hoelzl@64289
  1402
    fix x assume "x \<in> U"
hoelzl@64289
  1403
    then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
hoelzl@64289
  1404
    then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
wenzelm@64911
  1405
      using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
hoelzl@64289
  1406
    have "V \<in> K"
hoelzl@64289
  1407
      unfolding K_def using e(2) V(1) V(3) by auto
wenzelm@64911
  1408
    then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
hoelzl@64289
  1409
  }
hoelzl@64289
  1410
  then have "(\<Union>K) = U"
hoelzl@64289
  1411
    unfolding K_def by auto
hoelzl@64289
  1412
  moreover have "open (\<Union>K)"
hoelzl@64289
  1413
    unfolding K_def by auto
hoelzl@64289
  1414
  ultimately show "open U" by simp
hoelzl@64289
  1415
qed
hoelzl@64289
  1416
hoelzl@64289
  1417
instance proof
hoelzl@64289
  1418
  fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
hoelzl@64289
  1419
  proof
hoelzl@64289
  1420
    assume "x = y"
wenzelm@64911
  1421
    then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
hoelzl@64289
  1422
  next
hoelzl@64289
  1423
    assume "dist x y = 0"
hoelzl@64289
  1424
    have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
  1425
      by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1426
    have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
wenzelm@64911
  1427
      using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
hoelzl@64289
  1428
    then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
hoelzl@64289
  1429
      by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
hoelzl@64289
  1430
                zero_eq_1_divide_iff zero_neq_numeral)
hoelzl@64289
  1431
    then have "x (from_nat n) = y (from_nat n)" for n
hoelzl@64289
  1432
      by auto
hoelzl@64289
  1433
    then have "x i = y i" for i
hoelzl@64289
  1434
      by (metis from_nat_to_nat)
hoelzl@64289
  1435
    then show "x = y"
hoelzl@64289
  1436
      by auto
hoelzl@64289
  1437
  qed
hoelzl@64289
  1438
next
wenzelm@64911
  1439
  text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
hoelzl@64289
  1440
        with infinite series, hence we should justify the convergence at each step. In this
wenzelm@64911
  1441
        respect, the following simplification rule is extremely handy.\<close>
hoelzl@64289
  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"
hoelzl@64289
  1443
    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1444
  fix x y z::"'a \<Rightarrow> 'b"
hoelzl@64289
  1445
  {
hoelzl@64289
  1446
    fix n
hoelzl@64289
  1447
    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>
hoelzl@64289
  1448
            dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"
hoelzl@64289
  1449
      by (simp add: dist_triangle2)
hoelzl@64289
  1450
    have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"
hoelzl@64289
  1451
      using zero_le_dist by blast
hoelzl@64289
  1452
    moreover
hoelzl@64289
  1453
    {
hoelzl@64289
  1454
      assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"
hoelzl@64289
  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"
hoelzl@64289
  1456
        by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)
hoelzl@64289
  1457
    }
hoelzl@64289
  1458
    ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>
hoelzl@64289
  1459
            min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
hoelzl@64289
  1460
      using * by linarith
hoelzl@64289
  1461
  } note ineq = this
hoelzl@64289
  1462
  have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
  1463
    unfolding dist_fun_def by simp
hoelzl@64289
  1464
  also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
hoelzl@64289
  1465
                        + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
hoelzl@64289
  1466
    apply (rule suminf_le)
hoelzl@64289
  1467
    using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
hoelzl@64289
  1468
      le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
hoelzl@64289
  1469
    by (auto simp add: summable_add)
hoelzl@64289
  1470
  also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
hoelzl@64289
  1471
                  + (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
hoelzl@64289
  1472
    by (rule suminf_add[symmetric], auto)
hoelzl@64289
  1473
  also have "... = dist x z + dist y z"
hoelzl@64289
  1474
    unfolding dist_fun_def by simp
hoelzl@64289
  1475
  finally show "dist x y \<le> dist x z + dist y z"
hoelzl@64289
  1476
    by simp
hoelzl@64289
  1477
next
wenzelm@64911
  1478
  text\<open>Finally, we show that the topology generated by the distance and the product
hoelzl@64289
  1479
        topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
hoelzl@64289
  1480
        except that the condition to prove is expressed with filters. To deal with this,
hoelzl@64289
  1481
        we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
wenzelm@64911
  1482
        \verb+Real_Vector_Spaces.thy+\<close>
hoelzl@64289
  1483
  fix U::"('a \<Rightarrow> 'b) set"
hoelzl@64289
  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
hoelzl@64289
  1485
  unfolding uniformity_fun_def apply (subst eventually_INF_base)
hoelzl@64289
  1486
    by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
hoelzl@64289
  1487
  then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
hoelzl@64289
  1488
    unfolding fun_open_ball_aux by simp
hoelzl@64289
  1489
qed (simp add: uniformity_fun_def)
hoelzl@64289
  1490
hoelzl@64289
  1491
end
hoelzl@64289
  1492
wenzelm@64911
  1493
text \<open>Nice properties of spaces are preserved under countable products. In addition
hoelzl@64289
  1494
to first countability, second countability and metrizability, as we have seen above,
wenzelm@64911
  1495
completeness is also preserved, and therefore being Polish.\<close>
hoelzl@64289
  1496
hoelzl@64289
  1497
instance "fun" :: (countable, complete_space) complete_space
hoelzl@64289
  1498
proof
hoelzl@64289
  1499
  fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
hoelzl@64289
  1500
  have "Cauchy (\<lambda>n. u n i)" for i
hoelzl@64289
  1501
  unfolding cauchy_def proof (intro impI allI)
hoelzl@64289
  1502
    fix e assume "e>(0::real)"
hoelzl@64289
  1503
    obtain k where "i = from_nat k"
hoelzl@64289
  1504
      using from_nat_to_nat[of i] by metis
wenzelm@64911
  1505
    have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
hoelzl@64289
  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"
wenzelm@64911
  1507
      using \<open>Cauchy u\<close> unfolding cauchy_def by blast
hoelzl@64289
  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"
hoelzl@64289
  1509
      by blast
hoelzl@64289
  1510
    have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
hoelzl@64289
  1511
    proof (auto)
hoelzl@64289
  1512
      fix m n::nat assume "m \<ge> N" "n \<ge> N"
hoelzl@64289
  1513
      have "(1/2)^k * min (dist (u m i) (u n i)) 1
hoelzl@64289
  1514
              = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
wenzelm@64911
  1515
        using \<open>i = from_nat k\<close> by auto
hoelzl@64289
  1516
      also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
hoelzl@64289
  1517
        apply (rule sum_le_suminf)
hoelzl@64289
  1518
        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1519
      also have "... = dist (u m) (u n)"
hoelzl@64289
  1520
        unfolding dist_fun_def by auto
hoelzl@64289
  1521
      also have "... < (1/2)^k * min e 1"
wenzelm@64911
  1522
        using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
hoelzl@64289
  1523
      finally have "min (dist (u m i) (u n i)) 1 < min e 1"
hoelzl@64289
  1524
        by (auto simp add: algebra_simps divide_simps)
hoelzl@64289
  1525
      then show "dist (u m i) (u n i) < e" by auto
hoelzl@64289
  1526
    qed
hoelzl@64289
  1527
    then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
hoelzl@64289
  1528
      by blast
hoelzl@64289
  1529
  qed
hoelzl@64289
  1530
  then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
hoelzl@64289
  1531
    using Cauchy_convergent convergent_def by auto
hoelzl@64289
  1532
  then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"
hoelzl@64289
  1533
    using choice by force
hoelzl@64289
  1534
  then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast
hoelzl@64289
  1535
  have "u \<longlonglongrightarrow> x"
hoelzl@64289
  1536
  proof (rule metric_LIMSEQ_I)
hoelzl@64289
  1537
    fix e assume [simp]: "e>(0::real)"
hoelzl@64289
  1538
    have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i
hoelzl@64289
  1539
      by (rule metric_LIMSEQ_D, auto simp add: *)
hoelzl@64289
  1540
    have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"
hoelzl@64289
  1541
      apply (rule choice) using i by auto
hoelzl@64289
  1542
    then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"
hoelzl@64289
  1543
      by blast
hoelzl@64289
  1544
hoelzl@64289
  1545
    have "\<exists>N::nat. 2^N > 4/e"
hoelzl@64289
  1546
      by (simp add: real_arch_pow)
hoelzl@64289
  1547
    then obtain N::nat where "2^N > 4/e" by auto
hoelzl@64289
  1548
    define L where "L = Max {K (from_nat n)|n. n \<le> N}"
hoelzl@64289
  1549
    have "dist (u k) x < e" if "k \<ge> L" for k
hoelzl@64289
  1550
    proof -
hoelzl@64289
  1551
      have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
hoelzl@64289
  1552
      proof -
hoelzl@64289
  1553
        have "K (from_nat n) \<le> L"
wenzelm@64911
  1554
          unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
wenzelm@64911
  1555
        then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
hoelzl@64289
  1556
        then show ?thesis using K less_imp_le by auto
hoelzl@64289
  1557
      qed
hoelzl@64289
  1558
      have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
hoelzl@64289
  1559
        apply (rule Max.boundedI) using * by auto
hoelzl@64289
  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"
hoelzl@64289
  1561
        using dist_fun_le_dist_first_terms by auto
hoelzl@64289
  1562
      also have "... \<le> 2 * e/4 + e/4"
hoelzl@64289
  1563
        apply (rule add_mono)
wenzelm@64911
  1564
        using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps divide_simps)
hoelzl@64289
  1565
      also have "... < e" by auto
hoelzl@64289
  1566
      finally show ?thesis by simp
hoelzl@64289
  1567
    qed
hoelzl@64289
  1568
    then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
hoelzl@64289
  1569
  qed
hoelzl@64289
  1570
  then show "convergent u" using convergent_def by blast
hoelzl@64289
  1571
qed
hoelzl@64289
  1572
hoelzl@64289
  1573
instance "fun" :: (countable, polish_space) polish_space
hoelzl@64289
  1574
by standard
hoelzl@64289
  1575
hoelzl@64289
  1576
lp15@69030
  1577
lp15@69030
  1578
ak2110@68833
  1579
subsection%important \<open>Measurability\<close> (*FIX ME mv *)
hoelzl@64289
  1580
wenzelm@64911
  1581
text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
hoelzl@64289
  1582
generated by open sets in the product, and the product sigma algebra, countably generated by
hoelzl@64289
  1583
products of measurable sets along finitely many coordinates. The second one is defined and studied
hoelzl@64289
  1584
in \verb+Finite_Product_Measure.thy+.
hoelzl@64289
  1585
hoelzl@64289
  1586
These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
hoelzl@64289
  1587
but there is a fundamental difference: open sets are generated by arbitrary unions, not only
hoelzl@64289
  1588
countable ones, so typically many open sets will not be measurable with respect to the product sigma
hoelzl@64289
  1589
algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
hoelzl@64289
  1590
only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
hoelzl@64289
  1591
the factor is countably generated).
hoelzl@64289
  1592
hoelzl@64289
  1593
In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
hoelzl@64289
  1594
compare it with the product sigma algebra as explained above.
wenzelm@64911
  1595
\<close>
hoelzl@64289
  1596
ak2110@68833
  1597
lemma%unimportant measurable_product_coordinates [measurable (raw)]:
hoelzl@64289
  1598
  "(\<lambda>x. x i) \<in> measurable borel borel"
hoelzl@64289
  1599
by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
hoelzl@64289
  1600
ak2110@68833
  1601
lemma%unimportant measurable_product_then_coordinatewise:
hoelzl@64289
  1602
  fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
hoelzl@64289
  1603
  assumes [measurable]: "f \<in> borel_measurable M"
hoelzl@64289
  1604
  shows "(\<lambda>x. f x i) \<in> borel_measurable M"
hoelzl@64289
  1605
proof -
hoelzl@64289
  1606
  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
hoelzl@64289
  1607
    unfolding comp_def by auto
hoelzl@64289
  1608
  then show ?thesis by simp
hoelzl@64289
  1609
qed
hoelzl@64289
  1610
wenzelm@64911
  1611
text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
hoelzl@64289
  1612
of the product sigma algebra that is more similar to the one we used above for the product
wenzelm@64911
  1613
topology.\<close>
hoelzl@64289
  1614
ak2110@68833
  1615
lemma%important sets_PiM_finite:
hoelzl@64289
  1616
  "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
hoelzl@64289
  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)}}"
ak2110@68833
  1618
proof%unimportant
hoelzl@64289
  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)"
hoelzl@64289
  1620
  proof (auto)
hoelzl@64289
  1621
    fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
hoelzl@64289
  1622
    then have *: "X i \<in> sets (M i)" for i by simp
hoelzl@64289
  1623
    define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
hoelzl@64289
  1624
    have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
hoelzl@64289
  1625
    define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
hoelzl@64289
  1626
    have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
wenzelm@64911
  1627
      unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
hoelzl@64289
  1628
    moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
hoelzl@64289
  1629
      unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
hoelzl@64289
  1630
      by (auto simp add: PiE_iff, blast)
hoelzl@64289
  1631
    ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
hoelzl@64289
  1632
  qed
hoelzl@64289
  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)}}
hoelzl@64289
  1634
              \<subseteq> sets (Pi\<^sub>M I M)"
hoelzl@64289
  1635
    by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
hoelzl@64289
  1636
hoelzl@64289
  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>
hoelzl@64289
  1638
                (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
hoelzl@64289
  1639
    if "i \<in> I" "A \<in> sets (M i)" for i A
hoelzl@64289
  1640
  proof -
hoelzl@64289
  1641
    define X where "X = (\<lambda>j. if j = i then A else space (M j))"
hoelzl@64289
  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"
wenzelm@64911
  1643
      unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
hoelzl@64289
  1644
      by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
hoelzl@64289
  1645
    moreover have "X j \<in> sets (M j)" for j
wenzelm@64911
  1646
      unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
hoelzl@64289
  1647
    moreover have "finite {j. X j \<noteq> space (M j)}"
hoelzl@64289
  1648
      unfolding X_def by simp
hoelzl@64289
  1649
    ultimately show ?thesis by auto
hoelzl@64289
  1650
  qed
hoelzl@64289
  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)}}"
hoelzl@64289
  1652
    unfolding sets_PiM_single
hoelzl@64289
  1653
    apply (rule sigma_sets_mono')
hoelzl@64289
  1654
    apply (auto simp add: PiE_iff *)
hoelzl@64289
  1655
    done
hoelzl@64289
  1656
qed
hoelzl@64289
  1657
ak2110@68833
  1658
lemma%important sets_PiM_subset_borel:
hoelzl@64289
  1659
  "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
ak2110@68833
  1660
proof%unimportant -
hoelzl@64289
  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"
hoelzl@64289
  1662
  proof -
hoelzl@64289
  1663
    define I where "I = {i. X i \<noteq> UNIV}"
hoelzl@64289
  1664
    have "finite I" unfolding I_def using that by simp
hoelzl@64289
  1665
    have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
hoelzl@64289
  1666
      unfolding I_def by auto
hoelzl@64289
  1667
    also have "... \<in> sets borel"
wenzelm@64911
  1668
      using that \<open>finite I\<close> by measurable
hoelzl@64289
  1669
    finally show ?thesis by simp
hoelzl@64289
  1670
  qed
hoelzl@64289
  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"
hoelzl@64289
  1672
    by auto
hoelzl@64289
  1673
  then show ?thesis unfolding sets_PiM_finite space_borel
hoelzl@64289
  1674
    by (simp add: * sets.sigma_sets_subset')
hoelzl@64289
  1675
qed
hoelzl@64289
  1676
ak2110@68833
  1677
lemma%important sets_PiM_equal_borel:
hoelzl@64289
  1678
  "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
ak2110@68833
  1679
proof%unimportant
hoelzl@64289
  1680
  obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
wenzelm@64910
  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}"
hoelzl@64289
  1682
    using product_topology_countable_basis by fast
hoelzl@64289
  1683
  have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
hoelzl@64289
  1684
  proof -
wenzelm@64910
  1685
    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
wenzelm@64911
  1686
      using K(3)[OF \<open>k \<in> K\<close>] by blast
hoelzl@64289
  1687
    show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
hoelzl@64289
  1688
  qed
hoelzl@64289
  1689
  have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
hoelzl@64289
  1690
  proof -
hoelzl@64289
  1691
    obtain B where "B \<subseteq> K" "U = (\<Union>B)"
wenzelm@64911
  1692
      using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
wenzelm@64911
  1693
    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
hoelzl@64289
  1694
    moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
wenzelm@64911
  1695
      using \<open>B \<subseteq> K\<close> * that by auto
wenzelm@64911
  1696
    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
hoelzl@64289
  1697
  qed
hoelzl@64289
  1698
  have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
hoelzl@64289
  1699
    apply (rule sets.sigma_sets_subset') using ** by auto
hoelzl@64289
  1700
  then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
hoelzl@64289
  1701
    unfolding borel_def by auto
hoelzl@64289
  1702
qed (simp add: sets_PiM_subset_borel)
hoelzl@64289
  1703
ak2110@68833
  1704
lemma%important measurable_coordinatewise_then_product:
hoelzl@64289
  1705
  fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
hoelzl@64289
  1706
  assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
hoelzl@64289
  1707
  shows "f \<in> borel_measurable M"
ak2110@68833
  1708
proof%unimportant -
hoelzl@64289
  1709
  have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
hoelzl@64289
  1710
    by (rule measurable_PiM_single', auto simp add: assms)
hoelzl@64289
  1711
  then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
hoelzl@64289
  1712
qed
hoelzl@64289
  1713
hoelzl@64289
  1714
end