(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2012-2013 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Topology 6› theory Topology_ZF_6 imports Topology_ZF_4 Topology_ZF_2 Topology_ZF_1 begin text‹ This theory deals with the relations between continuous functions and convergence of filters. At the end of the file there some results about the building of functions in cartesian products. › subsection‹Image filter› text‹First of all, we will define the appropriate tools to work with functions and filters together.› text‹We define the image filter as the collections of supersets of of images of sets from a filter. › definition ImageFilter ("_[_].._" 98) where "𝔉 {is a filter on} X ⟹ f:X→Y ⟹ f[𝔉]..Y ≡ {A∈Pow(Y). ∃D∈{f``(B) .B∈𝔉}. D⊆A}" text‹Note that in the previous definition, it is necessary to state $Y$ as the final set because $f$ is also a function to every superset of its range. $X$ can be changed by ‹domain(f)› without any change in the definition.› lemma base_image_filter: assumes "𝔉 {is a filter on} X" "f:X→Y" shows "{f``B .B∈𝔉} {is a base filter} (f[𝔉]..Y)" and "(f[𝔉]..Y) {is a filter on} Y" proof- { assume "0 ∈ {f``B .B∈𝔉}" then obtain B where "B∈𝔉" and f_B:"f``B=0" by auto then have "B∈Pow(X)" using assms(1) IsFilter_def by auto then have "f``B={f`b. b∈B}" using image_fun assms(2) by auto with f_B have "{f`b. b∈B}=0" by auto then have "B=0" by auto with ‹B∈𝔉› have "False" using IsFilter_def assms(1) by auto } then have "0∉{f``B .B∈𝔉}" by auto moreover from assms(1) obtain S where "S∈𝔉" using IsFilter_def by auto then have "f``S∈{f``B .B∈𝔉}" by auto then have nA:"{f``B .B∈𝔉}≠0" by auto moreover { fix A B assume "A∈{f``B .B∈𝔉}" and "B∈{f``B .B∈𝔉}" then obtain AB BB where "A=f``AB" "B=f``BB" "AB∈𝔉" "BB∈𝔉" by auto then have "A∩B=(f``AB)∩(f``BB)" by auto then have I: "f``(AB∩BB)⊆A∩B" by auto moreover from assms(1) I ‹AB∈𝔉›‹BB∈𝔉› have "AB∩BB∈𝔉" using IsFilter_def by auto ultimately have "∃D∈{f``B .B∈𝔉}. D⊆A∩B" by auto } then have "∀A∈{f``B .B∈𝔉}. ∀B∈{f``B .B∈𝔉}. ∃D∈{f``B .B∈𝔉}. D⊆A∩B" by auto ultimately have sbc:"{f``B .B∈𝔉} {satisfies the filter base condition}" using SatisfiesFilterBase_def by auto moreover { fix t assume "t∈{f``B . B∈𝔉}" then obtain B where "B∈𝔉" and im_def:"f``B=t" by auto with assms(1) have "B∈Pow(X)" unfolding IsFilter_def by auto with im_def assms(2) have "t={f`x. x∈B}" using image_fun by auto with assms(2) ‹B∈Pow(X)› have "t⊆Y" using apply_funtype by auto } then have nB:"{f``B . B∈𝔉}⊆Pow(Y)" by auto ultimately have "(({f``B .B∈𝔉} {is a base filter} {A ∈ Pow(Y) . ∃D∈{f``B .B∈𝔉}. D ⊆ A}) ∧ (⋃{A ∈ Pow(Y) . ∃D∈{f``B .B∈𝔉}. D ⊆ A}=Y))" using base_unique_filter_set2 by force then have "{f``B .B∈𝔉} {is a base filter} {A ∈ Pow(Y) . ∃D∈{f``B .B∈𝔉}. D ⊆ A}" by auto with assms show "{f``B .B∈𝔉} {is a base filter} (f[𝔉]..Y)" using ImageFilter_def by auto moreover note sbc moreover { from nA obtain D where I: "D∈{f``B .B∈𝔉}" by blast moreover from I nB have "D⊆Y" by auto ultimately have "Y∈{A∈Pow(Y). ∃D∈{f``B .B∈𝔉}. D⊆A}" by auto } then have "⋃{A∈Pow(Y). ∃D∈{f``B .B∈𝔉}. D⊆A}=Y" by auto ultimately show "(f[𝔉]..Y) {is a filter on} Y" using basic_filter ImageFilter_def assms by auto qed subsection‹Continuous at a point vs. globally continuous› text‹In this section we show that continuity of a function implies local continuity (at a point) and that local continuity at all points implies (global) continuity.› text‹If a function is continuous, then it is continuous at every point.› lemma cont_global_imp_continuous_x: assumes "x∈⋃τ⇩_{1}" "IsContinuous(τ⇩_{1},τ⇩_{2},f)" "f:(⋃τ⇩_{1})→(⋃τ⇩_{2})" "x∈⋃τ⇩_{1}" shows "∀U∈τ⇩_{2}. f`(x)∈U ⟶ (∃V∈τ⇩_{1}. x∈V ∧ f``(V)⊆U)" proof- { fix U assume AS:"U∈τ⇩_{2}" "f`(x)∈U" then have "f-``(U)∈τ⇩_{1}" using assms(2) IsContinuous_def by auto moreover from assms(3) have "f``(f-``(U))⊆U" using function_image_vimage fun_is_fun by auto moreover from assms(3) assms(4) AS(2) have "x∈f-``(U)" using func1_1_L15 by auto ultimately have "∃V∈τ⇩_{1}. x∈V ∧ f``V⊆U" by auto } then show "∀U∈τ⇩_{2}. f`(x)∈U ⟶ (∃V∈τ⇩_{1}. x∈V ∧ f``(V)⊆U)" by auto qed text‹A function that is continuous at every point of its domain is continuous.› lemma ccontinuous_all_x_imp_cont_global: assumes "∀x∈⋃τ⇩_{1}. ∀U∈τ⇩_{2}. f`x∈U ⟶ (∃V∈τ⇩_{1}. x∈V ∧ f``V⊆U)" "f∈(⋃τ⇩_{1})→(⋃τ⇩_{2})" and "τ⇩_{1}{is a topology}" shows "IsContinuous(τ⇩_{1},τ⇩_{2},f)" proof- { fix U assume "U∈τ⇩_{2}" { fix x assume AS: "x∈f-``U" note ‹U∈τ⇩_{2}› moreover from assms(2) have "f -`` U ⊆ ⋃τ⇩_{1}" using func1_1_L6A by auto with AS have "x∈⋃τ⇩_{1}" by auto with assms(1) have "∀U∈τ⇩_{2}. f`x∈U ⟶ (∃V∈τ⇩_{1}. x∈V ∧ f``V⊆U)" by auto moreover from AS assms(2) have "f`x∈U" using func1_1_L15 by auto ultimately have "∃V∈τ⇩_{1}. x∈V ∧ f``V⊆U" by auto then obtain V where I: "V∈τ⇩_{1}" "x∈V" "f``(V)⊆U" by auto moreover from I have "V⊆⋃τ⇩_{1}" by auto moreover from assms(2) ‹V⊆⋃τ⇩_{1}› have "V⊆f-``(f``V)" using func1_1_L9 by auto ultimately have "V ⊆ f-``(U)" by blast with ‹V∈τ⇩_{1}› ‹x∈V› have "∃V∈τ⇩_{1}. x∈V ∧ V ⊆ f-``(U)" by auto } hence "∀x∈f-``(U). ∃V∈τ⇩_{1}. x∈V ∧ V⊆f-``(U)" by auto with assms(3) have "f-``(U) ∈ τ⇩_{1}" using topology0.open_neigh_open topology0_def by auto } hence "∀U∈τ⇩_{2}. f-``U∈τ⇩_{1}" by auto then show ?thesis using IsContinuous_def by auto qed subsection‹Continuous functions and filters› text‹In this section we consider the relations between filters and continuity.› text‹If the function is continuous then if the filter converges to a point the image filter converges to the image point.› lemma (in two_top_spaces0) cont_imp_filter_conver_preserved: assumes "𝔉 {is a filter on} X⇩_{1}" "f {is continuous}" "𝔉 →⇩_{F}x {in} τ⇩_{1}" shows "(f[𝔉]..X⇩_{2}) →⇩_{F}(f`(x)) {in} τ⇩_{2}" proof - from assms(1) assms(3) have "x∈X⇩_{1}" using topology0.FilterConverges_def topol_cntxs_valid(1) X1_def by auto have "topology0(τ⇩_{2})" using topol_cntxs_valid(2) by simp moreover from assms(1) have "(f[𝔉]..X⇩_{2}) {is a filter on} (⋃τ⇩_{2})" and "{f``B .B∈𝔉} {is a base filter} (f[𝔉]..X⇩_{2})" using base_image_filter fmapAssum X1_def X2_def by auto moreover have "∀U∈Pow(⋃τ⇩_{2}). (f`x)∈Interior(U,τ⇩_{2}) ⟶ (∃D∈{f``B .B∈𝔉}. D⊆U)" proof - { fix U assume "U∈Pow(X⇩_{2})" "(f`x)∈Interior(U,τ⇩_{2})" with ‹x∈X⇩_{1}› have xim: "x∈f-``(Interior(U,τ⇩_{2}))" and sub: "f-``(Interior(U,τ⇩_{2}))∈Pow(X⇩_{1})" using func1_1_L6A fmapAssum func1_1_L15 fmapAssum by auto note sub moreover have "Interior(U,τ⇩_{2})∈τ⇩_{2}" using topology0.Top_2_L2 topol_cntxs_valid(2) by auto with assms(2) have "f-``(Interior(U,τ⇩_{2}))∈τ⇩_{1}" unfolding isContinuous_def IsContinuous_def by auto with xim have "x∈Interior(f-``(Interior(U,τ⇩_{2})),τ⇩_{1})" using topology0.Top_2_L3 topol_cntxs_valid(1) by auto moreover from assms(1) assms(3) have "{U∈Pow(X⇩_{1}). x∈Interior(U,τ⇩_{1})}⊆𝔉" using topology0.FilterConverges_def topol_cntxs_valid(1) X1_def by auto ultimately have "f-``(Interior(U,τ⇩_{2}))∈𝔉" by auto moreover have "f``(f-``(Interior(U,τ⇩_{2})))⊆Interior(U,τ⇩_{2})" using function_image_vimage fun_is_fun fmapAssum by auto then have "f``(f-``(Interior(U,τ⇩_{2})))⊆U" using topology0.Top_2_L1 topol_cntxs_valid(2) by auto ultimately have "∃D∈{f``(B) .B∈𝔉}. D⊆U" by auto } thus ?thesis by auto qed moreover from fmapAssum ‹x∈X⇩_{1}› have "f`(x) ∈ X⇩_{2}" by (rule apply_funtype) hence "f`(x) ∈ ⋃τ⇩_{2}" by simp ultimately show ?thesis by (rule topology0.convergence_filter_base2) qed text‹Continuity in filter at every point of the domain implies global continuity.› lemma (in two_top_spaces0) filter_conver_preserved_imp_cont: assumes "∀x∈⋃τ⇩_{1}. ∀𝔉. ((𝔉 {is a filter on} X⇩_{1}) ∧ (𝔉 →⇩_{F}x {in} τ⇩_{1})) ⟶ ((f[𝔉]..X⇩_{2}) →⇩_{F}(f`x) {in} τ⇩_{2})" shows "f{is continuous}" proof- { fix x assume as2: "x∈⋃τ⇩_{1}" with assms have reg: "∀𝔉. ((𝔉 {is a filter on} X⇩_{1}) ∧ (𝔉 →⇩_{F}x {in} τ⇩_{1})) ⟶ ((f[𝔉]..X⇩_{2}) →⇩_{F}(f`x) {in} τ⇩_{2})" by auto let ?Neig = "{U ∈ Pow(⋃τ⇩_{1}) . x ∈ Interior(U, τ⇩_{1})}" from as2 have NFil: "?Neig{is a filter on}X⇩_{1}" and NCon: "?Neig →⇩_{F}x {in} τ⇩_{1}" using topol_cntxs_valid(1) topology0.neigh_filter by auto { fix U assume "U∈τ⇩_{2}" "f`x∈U" then have "U∈Pow(⋃τ⇩_{2})" "f`x∈Interior(U,τ⇩_{2})" using topol_cntxs_valid(2) topology0.Top_2_L3 by auto moreover from NCon NFil reg have "(f[?Neig]..X⇩_{2}) →⇩_{F}(f`x) {in} τ⇩_{2}" by auto moreover have "(f[?Neig]..X⇩_{2}) {is a filter on} X⇩_{2}" using base_image_filter(2) NFil fmapAssum by auto ultimately have "U∈(f[?Neig]..X⇩_{2})" using topology0.FilterConverges_def topol_cntxs_valid(2) unfolding X1_def X2_def by auto moreover from fmapAssum NFil have "{f``B .B∈?Neig} {is a base filter} (f[?Neig]..X⇩_{2})" using base_image_filter(1) X1_def X2_def by auto ultimately have "∃V∈{f``B .B∈?Neig}. V⊆U" using basic_element_filter by blast then obtain B where "B∈?Neig" "f``B⊆U" by auto moreover have "Interior(B,τ⇩_{1})⊆B" using topology0.Top_2_L1 topol_cntxs_valid(1) by auto hence "f``Interior(B,τ⇩_{1}) ⊆ f``(B)" by auto moreover have "Interior(B,τ⇩_{1})∈τ⇩_{1}" using topology0.Top_2_L2 topol_cntxs_valid(1) by auto ultimately have "∃V∈τ⇩_{1}. x∈V ∧ f``V⊆U" by force } hence "∀U∈τ⇩_{2}. f`x∈U ⟶ (∃V∈τ⇩_{1}. x∈V ∧ f``V⊆U)" by auto } hence "∀x∈⋃τ⇩_{1}. ∀U∈τ⇩_{2}. f`x∈U ⟶ (∃V∈τ⇩_{1}. x∈V ∧ f``V⊆U)" by auto then show ?thesis using ccontinuous_all_x_imp_cont_global fmapAssum X1_def X2_def isContinuous_def tau1_is_top by auto qed end