(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2005 - 2008 Slawomir Kolodynski 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. *) header{*\isaheader{Topology\_ZF\_1.thy}*} theory Topology_ZF_1 imports Topology_ZF begin text{*In this theory file we study separation axioms and the notion of base and subbase. Using the products of open sets as a subbase we define a natural topology on a product of two topological spaces. *} section{*Separation axioms.*} text{*Topological spaces cas be classified according to certain properties called "separation axioms". In this section we define what it means that a topological space is $T_0$, $T_1$ or $T_2$.*} text{*A topology on $X$ is $T_0$ if for every pair of distinct points of $X$ there is an open set that contains only one of them. *} definition isT0 ("_ {is T⇩_{0}}" [90] 91) where "T {is T⇩_{0}} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y) --> (∃U∈T. (x∈U ∧ y∉U) ∨ (y∈U ∧ x∉U)))" text{* A topology is $T_1$ if for every such pair there exist an open set that contains the first point but not the second.*} definition isT1 ("_ {is T⇩_{1}}" [90] 91) where "T {is T⇩_{1}} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y) --> (∃U∈T. (x∈U ∧ y∉U)))" text{* A topology is $T_2$ (Hausdorff) if for every pair of points there exist a pair of disjoint open sets each containing one of the points. This is an important class of topological spaces. In particular, metric spaces are Hausdorff.*} definition isT2 ("_ {is T⇩_{2}}" [90] 91) where "T {is T⇩_{2}} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y) --> (∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0))" text{*If a topology is $T_1$ then it is $T_0$. We don't really assume here that $T$ is a topology on $X$. Instead, we prove the relation between isT0 condition and isT1. *} lemma T1_is_T0: assumes A1: "T {is T⇩_{1}}" shows "T {is T⇩_{0}}" proof - from A1 have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y --> (∃U∈T. x∈U ∧ y∉U)" using isT1_def by simp then have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y --> (∃U∈T. x∈U ∧ y∉U ∨ y∈U ∧ x∉U)" by auto then show "T {is T⇩_{0}}" using isT0_def by simp qed text{*If a topology is $T_2$ then it is $T_1$.*} lemma T2_is_T1: assumes A1: "T {is T⇩_{2}}" shows "T {is T⇩_{1}}" proof - { fix x y assume "x ∈ \<Union>T" "y ∈ \<Union>T" "x≠y" with A1 have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0" using isT2_def by auto then have "∃U∈T. x∈U ∧ y∉U" by auto } then have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y --> (∃U∈T. x∈U ∧ y∉U)" by simp then show "T {is T⇩_{1}}" using isT1_def by simp qed text{*In a $T_0$ space two points that can not be separated by an open set are equal. Proof by contradiction.*} lemma Top_1_1_L1: assumes A1: "T {is T⇩_{0}}" and A2: "x ∈ \<Union>T" "y ∈ \<Union>T" and A3: "∀U∈T. (x∈U <-> y∈U)" shows "x=y" proof - { assume "x≠y" with A1 A2 have "∃U∈T. x∈U ∧ y∉U ∨ y∈U ∧ x∉U" using isT0_def by simp with A3 have False by auto } then show "x=y" by auto qed section{*Bases and subbases.*} text{*Sometimes it is convenient to talk about topologies in terms of their bases and subbases. These are certain collections of open sets that define the whole topology.*} text{*A base of topology is a collection of open sets such that every open set is a union of the sets from the base.*} definition IsAbaseFor (infixl "{is a base for}" 65) where "B {is a base for} T ≡ B⊆T ∧ T = {\<Union>A. A∈Pow(B)}" text{* A subbase is a collection of open sets such that finite intersection of those sets form a base.*} definition IsAsubBaseFor (infixl "{is a subbase for}" 65) where "B {is a subbase for} T ≡ B ⊆ T ∧ {\<Inter>A. A ∈ FinPow(B)} {is a base for} T" text{*Below we formulate a condition that we will prove to be necessary and sufficient for a collection $B$ of open sets to form a base. It says that for any two sets $U,V$ from the collection $B$ we can find a point $x\in U\cap V$ with a neighboorhod from $B$ contained in $U\cap V$.*} definition SatisfiesBaseCondition ("_ {satisfies the base condition}" [50] 50) where "B {satisfies the base condition} ≡ ∀U V. ((U∈B ∧ V∈B) --> (∀x ∈ U∩V. ∃W∈B. x∈W ∧ W ⊆ U∩V))" text{*A collection that is closed with respect to intersection satisfies the base condition.*} lemma inter_closed_base: assumes "∀U∈B.(∀V∈B. U∩V ∈ B)" shows "B {satisfies the base condition}" proof - { fix U V x assume "U∈B" and "V∈B" and "x ∈ U∩V" with assms have "∃W∈B. x∈W ∧ W ⊆ U∩V" by blast } then show ?thesis using SatisfiesBaseCondition_def by simp qed text{*Each open set is a union of some sets from the base.*} lemma Top_1_2_L1: assumes "B {is a base for} T" and "U∈T" shows "∃A∈Pow(B). U = \<Union>A" using assms IsAbaseFor_def by simp text{* Elements of base are open. *} lemma base_sets_open: assumes "B {is a base for} T" and "U ∈ B" shows "U ∈ T" using assms IsAbaseFor_def by auto; text{*A base defines topology uniquely.*} lemma same_base_same_top: assumes "B {is a base for} T" and "B {is a base for} S" shows "T = S" using assms IsAbaseFor_def by simp; text{*Every point from an open set has a neighboorhood from the base that is contained in the set.*} lemma point_open_base_neigh: assumes A1: "B {is a base for} T" and A2: "U∈T" and A3: "x∈U" shows "∃V∈B. V⊆U ∧ x∈V" proof - from A1 A2 obtain A where "A ∈ Pow(B)" and "U = \<Union>A" using Top_1_2_L1 by blast; with A3 obtain V where "V∈A" and "x∈V" by auto; with `A ∈ Pow(B)` `U = \<Union>A` show ?thesis by auto; qed; text{* A criterion for a collection to be a base for a topology that is a slight reformulation of the definition. The only thing different that in the definition is that we assume only that every open set is a union of some sets from the base. The definition requires also the opposite inclusion that every union of the sets from the base is open, but that we can prove if we assume that $T$ is a topology.*} lemma is_a_base_criterion: assumes A1: "T {is a topology}" and A2: "B ⊆ T" and A3: "∀V ∈ T. ∃A ∈ Pow(B). V = \<Union>A" shows "B {is a base for} T" proof - from A3 have "T ⊆ {\<Union>A. A∈Pow(B)}" by auto; moreover have "{\<Union>A. A∈Pow(B)} ⊆ T" proof; fix U assume "U ∈ {\<Union>A. A∈Pow(B)}" then obtain A where "A ∈ Pow(B)" and "U = \<Union>A" by auto; with `B ⊆ T` have "A ∈ Pow(T)" by auto; with A1 `U = \<Union>A` show "U ∈ T" unfolding IsATopology_def by simp; qed ultimately have "T = {\<Union>A. A∈Pow(B)}" by auto; with A2 show "B {is a base for} T" unfolding IsAbaseFor_def by simp; qed; text{*A necessary condition for a collection of sets to be a base for some topology : every point in the intersection of two sets in the base has a neighboorhood from the base contained in the intersection.*} lemma Top_1_2_L2: assumes A1:"∃T. T {is a topology} ∧ B {is a base for} T" and A2: "V∈B" "W∈B" shows "∀ x ∈ V∩W. ∃U∈B. x∈U ∧ U ⊆ V ∩ W" proof - from A1 obtain T where D1: "T {is a topology}" "B {is a base for} T" by auto then have "B ⊆ T" using IsAbaseFor_def by auto with A2 have "V∈T" and "W∈T" using IsAbaseFor_def by auto with D1 have "∃A∈Pow(B). V∩W = \<Union>A" using IsATopology_def Top_1_2_L1 by auto then obtain A where "A ⊆ B" and "V ∩ W = \<Union>A" by auto then show "∀ x ∈ V∩W. ∃U∈B. (x∈U ∧ U ⊆ V ∩ W)" by auto qed text{*We will construct a topology as the collection of unions of (would-be) base. First we prove that if the collection of sets satisfies the condition we want to show to be sufficient, the the intersection belongs to what we will define as topology (am I clear here?). Having this fact ready simplifies the proof of the next lemma. There is not much topology here, just some set theory.*} lemma Top_1_2_L3: assumes A1: "∀x∈ V∩W . ∃U∈B. x∈U ∧ U ⊆ V∩W" shows "V∩W ∈ {\<Union>A. A∈Pow(B)}" proof let ?A = "\<Union>x∈V∩W. {U∈B. x∈U ∧ U ⊆ V∩W}" show "?A∈Pow(B)" by auto from A1 show "V∩W = \<Union>?A" by blast qed text{*The next lemma is needed when proving that the would-be topology is closed with respect to taking intersections. We show here that intersection of two sets from this (would-be) topology can be written as union of sets from the topology.*} lemma Top_1_2_L4: assumes A1: "U⇩_{1}∈ {\<Union>A. A∈Pow(B)}" "U⇩_{2}∈ {\<Union>A. A∈Pow(B)}" and A2: "B {satisfies the base condition}" shows "∃C. C ⊆ {\<Union>A. A∈Pow(B)} ∧ U⇩_{1}∩U⇩_{2}= \<Union>C" proof - from A1 A2 obtain A⇩_{1}A⇩_{2}where D1: "A⇩_{1}∈ Pow(B)" "U⇩_{1}= \<Union>A⇩_{1}" "A⇩_{2}∈ Pow(B)" "U⇩_{2}= \<Union>A⇩_{2}" by auto let ?C = "\<Union>U∈A⇩_{1}.{U∩V. V∈A⇩_{2}}" from D1 have "(∀U∈A⇩_{1}. U∈B) ∧ (∀V∈A⇩_{2}. V∈B)" by auto with A2 have "?C ⊆ {\<Union>A . A ∈ Pow(B)}" using Top_1_2_L3 SatisfiesBaseCondition_def by auto moreover from D1 have "U⇩_{1}∩ U⇩_{2}= \<Union>?C" by auto ultimately show ?thesis by auto qed text{*If $B$ satisfies the base condition, then the collection of unions of sets from $B$ is a topology and $B$ is a base for this topology.*} theorem Top_1_2_T1: assumes A1: "B {satisfies the base condition}" and A2: "T = {\<Union>A. A∈Pow(B)}" shows "T {is a topology}" and "B {is a base for} T" proof - show "T {is a topology}" proof - have I: "∀C∈Pow(T). \<Union>C ∈ T" proof - { fix C assume A3: "C ∈ Pow(T)" let ?Q = "\<Union> {\<Union>{A∈Pow(B). U = \<Union>A}. U∈C}" from A2 A3 have "∀U∈C. ∃A∈Pow(B). U = \<Union>A" by auto then have "\<Union>?Q = \<Union>C" using ZF1_1_L10 by simp moreover from A2 have "\<Union>?Q ∈ T" by auto ultimately have "\<Union>C ∈ T" by simp } thus "∀C∈Pow(T). \<Union>C ∈ T" by auto qed moreover have "∀U∈T. ∀ V∈T. U∩V ∈ T" proof - { fix U V assume "U ∈ T" "V ∈ T" with A1 A2 have "∃C.(C ⊆ T ∧ U∩V = \<Union>C)" using Top_1_2_L4 by simp then obtain C where "C ⊆ T" and "U∩V = \<Union>C" by auto with I have "U∩V ∈ T" by simp } then show "∀U∈T. ∀ V∈T. U∩V ∈ T" by simp qed ultimately show "T {is a topology}" using IsATopology_def by simp qed from A2 have "B⊆T" by auto with A2 show "B {is a base for} T" using IsAbaseFor_def by simp qed; text{*The carrier of the base and topology are the same.*} lemma Top_1_2_L5: assumes "B {is a base for} T" shows "\<Union>T = \<Union>B" using assms IsAbaseFor_def by auto text{*If $B$ is a base for $T$, then $T$ is the smallest topology containing $B$. *} lemma base_smallest_top: assumes A1: "B {is a base for} T" and A2: "S {is a topology}" and A3: "B⊆S" shows "T⊆S" proof fix U assume "U∈T" with A1 obtain B⇩_{U}where "B⇩_{U}⊆ B" and "U = \<Union>B⇩_{U}" using IsAbaseFor_def by auto with A3 have "B⇩_{U}⊆ S" by auto with A2 `U = \<Union>B⇩_{U}` show "U∈S" using IsATopology_def by simp qed text{*If $B$ is a base for $T$ and $B$ is a topology, then $B=T$.*} lemma base_topology: assumes "B {is a topology}" and "B {is a base for} T" shows "B=T" using assms base_sets_open base_smallest_top by blast section{*Product topology*} text{*In this section we consider a topology defined on a product of two sets.*} text{*Given two topological spaces we can define a topology on the product of the carriers such that the cartesian products of the sets of the topologies are a base for the product topology. Recall that for two collections $S,T$ of sets the product collection is defined (in @{text "ZF1.thy"}) as the collections of cartesian products $A\times B$, where $A\in S, B\in T$.*} definition "ProductTopology(T,S) ≡ {\<Union>W. W ∈ Pow(ProductCollection(T,S))}" text{*The product collection satisfies the base condition.*} lemma Top_1_4_L1: assumes A1: "T {is a topology}" "S {is a topology}" and A2: "A ∈ ProductCollection(T,S)" "B ∈ ProductCollection(T,S)" shows "∀x∈(A∩B). ∃W∈ProductCollection(T,S). (x∈W ∧ W ⊆ A ∩ B)" proof fix x assume A3: "x ∈ A∩B" from A2 obtain U⇩_{1}V⇩_{1}U⇩_{2}V⇩_{2}where D1: "U⇩_{1}∈T" "V⇩_{1}∈S" "A=U⇩_{1}×V⇩_{1}" "U⇩_{2}∈T" "V⇩_{2}∈S" "B=U⇩_{2}×V⇩_{2}" using ProductCollection_def by auto let ?W = "(U⇩_{1}∩U⇩_{2}) × (V⇩_{1}∩V⇩_{2})" from A1 D1 have "U⇩_{1}∩U⇩_{2}∈ T" and "V⇩_{1}∩V⇩_{2}∈ S" using IsATopology_def by auto then have "?W ∈ ProductCollection(T,S)" using ProductCollection_def by auto moreover from A3 D1 have "x∈?W" and "?W ⊆ A∩B" by auto ultimately have "∃W. (W ∈ ProductCollection(T,S) ∧ x∈W ∧ W ⊆ A∩B)" by auto thus "∃W∈ProductCollection(T,S). (x∈W ∧ W ⊆ A ∩ B)" by auto qed text{*The product topology is indeed a topology on the product.*} theorem Top_1_4_T1: assumes A1: "T {is a topology}" "S {is a topology}" shows "ProductTopology(T,S) {is a topology}" "ProductCollection(T,S) {is a base for} ProductTopology(T,S)" "\<Union> ProductTopology(T,S) = \<Union>T × \<Union>S" proof - from A1 show "ProductTopology(T,S) {is a topology}" "ProductCollection(T,S) {is a base for} ProductTopology(T,S)" using Top_1_4_L1 ProductCollection_def SatisfiesBaseCondition_def ProductTopology_def Top_1_2_T1 by auto then show "\<Union> ProductTopology(T,S) = \<Union>T × \<Union>S" using Top_1_2_L5 ZF1_1_L6 by simp qed text{*Each point of a set open in the product topology has a neighborhood which is a cartesian product of open sets.*} lemma prod_top_point_neighb: assumes A1: "T {is a topology}" "S {is a topology}" and A2: "U ∈ ProductTopology(T,S)" and A3: "x ∈ U" shows "∃V W. V∈T ∧ W∈S ∧ V×W ⊆ U ∧ x ∈ V×W" proof - from A1 have "ProductCollection(T,S) {is a base for} ProductTopology(T,S)" using Top_1_4_T1 by simp; with A2 A3 obtain Z where "Z ∈ ProductCollection(T,S)" and "Z ⊆ U ∧ x∈Z" using point_open_base_neigh by blast; then obtain V W where "V ∈ T" and "W∈S" and" V×W ⊆ U ∧ x ∈ V×W" using ProductCollection_def by auto; thus ?thesis by auto; qed text{*Products of open sets are open in the product topology.*} lemma prod_open_open_prod: assumes A1: "T {is a topology}" "S {is a topology}" and A2: "U∈T" "V∈S" shows "U×V ∈ ProductTopology(T,S)" proof - from A1 have "ProductCollection(T,S) {is a base for} ProductTopology(T,S)" using Top_1_4_T1 by simp; moreover from A2 have "U×V ∈ ProductCollection(T,S)" unfolding ProductCollection_def by auto; ultimately show "U×V ∈ ProductTopology(T,S)" using base_sets_open by simp; qed text{*Sets that are open in th product topology are contained in the product of the carrier.*} lemma prod_open_type: assumes A1: "T {is a topology}" "S {is a topology}" and A2: "V ∈ ProductTopology(T,S)" shows "V ⊆ \<Union>T × \<Union>S" proof - from A2 have "V ⊆ \<Union> ProductTopology(T,S)" by auto with A1 show ?thesis using Top_1_4_T1 by simp qed text{*Suppose we have subsets $A\subseteq X, B\subseteq Y$, where $X,Y$ are topological spaces with topologies $T,S$. We can the consider relative topologies on $T_A, S_B$ on sets $A,B$ and the collection of cartesian products of sets open in $T_A, S_B$, (namely $\{U\times V: U\in T_A, V\in S_B\}$. The next lemma states that this collection is a base of the product topology on $X\times Y$ restricted to the product $A\times B$. *} lemma prod_restr_base_restr: assumes A1: "T {is a topology}" "S {is a topology}" shows "ProductCollection(T {restricted to} A, S {restricted to} B) {is a base for} (ProductTopology(T,S) {restricted to} A×B)" proof -; let ?\<B> = "ProductCollection(T {restricted to} A, S {restricted to} B)" let ?τ = "ProductTopology(T,S)" from A1 have "(?τ {restricted to} A×B) {is a topology}" using Top_1_4_T1 topology0_def topology0.Top_1_L4 by simp; moreover have "?\<B> ⊆ (?τ {restricted to} A×B)" proof fix U assume "U ∈ ?\<B>" then obtain U⇩_{A}U⇩_{B}where "U = U⇩_{A}× U⇩_{B}" and "U⇩_{A}∈ (T {restricted to} A)" and "U⇩_{B}∈ (S {restricted to} B)" using ProductCollection_def by auto; then obtain W⇩_{A}W⇩_{B}where "W⇩_{A}∈ T" "U⇩_{A}= W⇩_{A}∩ A" and "W⇩_{B}∈ S" "U⇩_{B}= W⇩_{B}∩ B" using RestrictedTo_def by auto; with `U = U⇩_{A}× U⇩_{B}` have "U = W⇩_{A}×W⇩_{B}∩ (A×B)" by auto; moreover from A1 `W⇩_{A}∈ T` and `W⇩_{B}∈ S` have "W⇩_{A}×W⇩_{B}∈ ?τ" using prod_open_open_prod by simp; ultimately show "U ∈ ?τ {restricted to} A×B" using RestrictedTo_def by auto; qed; moreover have "∀U ∈ ?τ {restricted to} A×B. ∃C ∈ Pow(?\<B>). U = \<Union>C" proof; fix U assume "U ∈ ?τ {restricted to} A×B" then obtain W where "W ∈ ?τ" and "U = W ∩ (A×B)" using RestrictedTo_def by auto; from A1 `W ∈ ?τ` obtain A⇩_{W}where "A⇩_{W}∈ Pow(ProductCollection(T,S))" and "W = \<Union>A⇩_{W}" using Top_1_4_T1 IsAbaseFor_def by auto; let ?C = "{V ∩ A×B. V ∈ A⇩_{W}}" have "?C ∈ Pow(?\<B>)" and "U = \<Union>?C" proof - { fix R assume "R ∈ ?C" then obtain V where "V ∈ A⇩_{W}" and "R = V ∩ A×B" by auto; with `A⇩_{W}∈ Pow(ProductCollection(T,S))` obtain V⇩_{T}V⇩_{S}where "V⇩_{T}∈ T" and "V⇩_{S}∈ S" and "V = V⇩_{T}× V⇩_{S}" using ProductCollection_def by auto; with `R = V ∩ A×B` have "R ∈ ?\<B>" using ProductCollection_def RestrictedTo_def by auto; } then show "?C ∈ Pow(?\<B>)" by auto; from `U = W ∩ (A×B)` and `W = \<Union>A⇩_{W}` show "U = \<Union>?C" by auto; qed; thus "∃C ∈ Pow(?\<B>). U = \<Union>C" by blast; qed; ultimately show ?thesis by (rule is_a_base_criterion); qed; text{*We can commute taking restriction (relative topology) and product topology. The reason the two topologies are the same is that they have the same base.*} lemma prod_top_restr_comm: assumes A1: "T {is a topology}" "S {is a topology}" shows "ProductTopology(T {restricted to} A,S {restricted to} B) = ProductTopology(T,S) {restricted to} (A×B)" proof - let ?\<B> = "ProductCollection(T {restricted to} A, S {restricted to} B)" from A1 have "?\<B> {is a base for} ProductTopology(T {restricted to} A,S {restricted to} B)" using topology0_def topology0.Top_1_L4 Top_1_4_T1 by simp; moreover from A1 have "?\<B> {is a base for} ProductTopology(T,S) {restricted to} (A×B)" using prod_restr_base_restr by simp; ultimately show ?thesis by (rule same_base_same_top); qed text{*Projection of a section of an open set is open.*} lemma prod_sec_open1: assumes A1: "T {is a topology}" "S {is a topology}" and A2: "V ∈ ProductTopology(T,S)" and A3: "x ∈ \<Union>T" shows "{y ∈ \<Union>S. ⟨x,y⟩ ∈ V} ∈ S" proof - let ?A = "{y ∈ \<Union>S. ⟨x,y⟩ ∈ V}" from A1 have "topology0(S)" using topology0_def by simp moreover have "∀y∈?A.∃W∈S. (y∈W ∧ W⊆?A)" proof fix y assume "y ∈ ?A" then have "⟨x,y⟩ ∈ V" by simp with A1 A2 have "⟨x,y⟩ ∈ \<Union>T × \<Union>S" using prod_open_type by blast hence "x ∈ \<Union>T" and "y ∈ \<Union>S" by auto from A1 A2 `⟨x,y⟩ ∈ V` have "∃U W. U∈T ∧ W∈S ∧ U×W ⊆ V ∧ ⟨x,y⟩ ∈ U×W" by (rule prod_top_point_neighb) then obtain U W where "U∈T" "W∈S" "U×W ⊆ V" "⟨x,y⟩ ∈ U×W" by auto with A1 A2 show "∃W∈S. (y∈W ∧ W⊆?A)" using prod_open_type section_proj by auto qed ultimately show ?thesis by (rule topology0.open_neigh_open) qed text{*Projection of a section of an open set is open. This is dual of @{text "prod_sec_open1"} with a very similar proof.*} lemma prod_sec_open2: assumes A1: "T {is a topology}" "S {is a topology}" and A2: "V ∈ ProductTopology(T,S)" and A3: "y ∈ \<Union>S" shows "{x ∈ \<Union>T. ⟨x,y⟩ ∈ V} ∈ T" proof - let ?A = "{x ∈ \<Union>T. ⟨x,y⟩ ∈ V}" from A1 have "topology0(T)" using topology0_def by simp moreover have "∀x∈?A.∃W∈T. (x∈W ∧ W⊆?A)" proof fix x assume "x ∈ ?A" then have "⟨x,y⟩ ∈ V" by simp with A1 A2 have "⟨x,y⟩ ∈ \<Union>T × \<Union>S" using prod_open_type by blast hence "x ∈ \<Union>T" and "y ∈ \<Union>S" by auto from A1 A2 `⟨x,y⟩ ∈ V` have "∃U W. U∈T ∧ W∈S ∧ U×W ⊆ V ∧ ⟨x,y⟩ ∈ U×W" by (rule prod_top_point_neighb) then obtain U W where "U∈T" "W∈S" "U×W ⊆ V" "⟨x,y⟩ ∈ U×W" by auto with A1 A2 show "∃W∈T. (x∈W ∧ W⊆?A)" using prod_open_type section_proj by auto qed ultimately show ?thesis by (rule topology0.open_neigh_open) qed end