:: Properties of the Product of Compact Topological Spaces :: by Adam Grabowski :: :: Received February 13, 1999 :: Copyright (c) 1999-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies PRE_TOPC, SUBSET_1, ZFMISC_1, XBOOLE_0, FUNCOP_1, ORDINAL2, FUNCT_1, RELAT_1, STRUCT_0, TOPS_2, T_0TOPSP, RCOMP_1, MCART_1, PARTFUN1, TARSKI, PBOOLE, BORSUK_1, TOPS_1, CONNSP_2, SETFAM_1, FINSET_1, FUNCT_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP, FINSET_1, FUNCT_3, CONNSP_2; constructors FUNCT_3, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, T_0TOPSP, FUNCOP_1, BINOP_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, COMPTS_1, BORSUK_2, ZFMISC_1; requirements SUBSET, BOOLE; definitions TARSKI, TOPS_2, COMPTS_1, T_0TOPSP, FUNCT_1, XBOOLE_0; equalities BINOP_1, STRUCT_0; expansions TARSKI, TOPS_2, COMPTS_1, T_0TOPSP, XBOOLE_0; theorems BORSUK_1, FUNCOP_1, TOPS_2, FUNCT_2, FUNCT_1, PRE_TOPC, TARSKI, TOPS_1, TOPMETR, ZFMISC_1, CONNSP_2, FUNCT_3, COMPTS_1, FINSET_1, YELLOW12, TSEP_1, TOPGRP_1, XBOOLE_0, XBOOLE_1, SETFAM_1; schemes PBOOLE, CLASSES1, XFAMILY; begin :: Preliminaries theorem for S, T being TopSpace holds [#][:S, T:] = [:[#]S, [#]T:] by BORSUK_1:def 2; theorem Th2: for X, Y being non empty TopSpace, x being Point of X holds Y --> x is continuous Function of Y, X|{x} proof let X, Y be non empty TopSpace, x be Point of X; set Z = {x}; set f = Y --> x; x in Z & the carrier of (X|Z) = Z by PRE_TOPC:8,TARSKI:def 1; then reconsider g = f as Function of Y, X|Z by FUNCOP_1:45; g is continuous by TOPMETR:6; hence thesis; end; registration let T be TopStruct; cluster id T -> being_homeomorphism; coherence by TOPGRP_1:20; end; Lm1: for S being TopStruct holds S, S are_homeomorphic proof let S be TopStruct; take id S; thus thesis; end; Lm2: for S, T being non empty TopStruct st S, T are_homeomorphic holds T, S are_homeomorphic proof let S, T be non empty TopStruct; assume S, T are_homeomorphic; then consider f being Function of S, T such that A1: f is being_homeomorphism; f" is being_homeomorphism by A1,TOPS_2:56; hence thesis; end; definition let S, T be TopStruct; redefine pred S, T are_homeomorphic; reflexivity by Lm1; end; definition let S, T be non empty TopStruct; redefine pred S, T are_homeomorphic; reflexivity by Lm1; symmetry by Lm2; end; theorem for S, T, V being non empty TopSpace st S, T are_homeomorphic & T, V are_homeomorphic holds S, V are_homeomorphic proof let S, T, V be non empty TopSpace; assume that A1: S, T are_homeomorphic and A2: T, V are_homeomorphic; consider f being Function of S, T such that A3: f is being_homeomorphism by A1; consider g being Function of T, V such that A4: g is being_homeomorphism by A2; g * f is being_homeomorphism by A3,A4,TOPS_2:57; hence thesis; end; begin :: On the projections and empty topological spaces registration let T be TopStruct, P be empty Subset of T; cluster T | P -> empty; coherence; end; registration cluster empty -> compact for TopSpace; coherence; end; theorem Th4: for X, Y being non empty TopSpace, x being Point of X, f being Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f is one-to-one proof let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | { x}:], Y; set Z = {x}; assume A1: f = pr1(the carrier of Y, Z); let z, y be object such that A2: z in dom f and A3: y in dom f and A4: f.z = f.y; A5: dom f = [:the carrier of Y, Z:] by A1,FUNCT_3:def 4; then consider x1, x2 being object such that A6: x1 in the carrier of Y and A7: x2 in Z and A8: z = [x1, x2] by A2,ZFMISC_1:def 2; consider y1, y2 being object such that A9: y1 in the carrier of Y and A10: y2 in Z and A11: y = [y1, y2] by A5,A3,ZFMISC_1:def 2; A12: x2 = x by A7,TARSKI:def 1 .= y2 by A10,TARSKI:def 1; x1 = f.(x1, x2) by A1,A6,A7,FUNCT_3:def 4 .= f.(y1, y2) by A4,A8,A11 .= y1 by A1,A9,A10,FUNCT_3:def 4; hence thesis by A8,A11,A12; end; theorem Th5: for X, Y being non empty TopSpace, x being Point of X, f being Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f is one-to-one proof let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x}, Y:], Y; set Z = {x}; assume A1: f = pr2(Z, the carrier of Y); let z, y be object such that A2: z in dom f and A3: y in dom f and A4: f.z = f.y; A5: dom f = [:Z, the carrier of Y:] by A1,FUNCT_3:def 5; then consider x1, x2 being object such that A6: x1 in Z and A7: x2 in the carrier of Y and A8: z = [x1,x2] by A2,ZFMISC_1:def 2; consider y1, y2 being object such that A9: y1 in Z and A10: y2 in the carrier of Y and A11: y = [y1,y2] by A5,A3,ZFMISC_1:def 2; A12: x1 = x by A6,TARSKI:def 1 .= y1 by A9,TARSKI:def 1; x2= f.(x1, x2) by A1,A6,A7,FUNCT_3:def 5 .= f.(y1, y2) by A4,A8,A11 .= y2 by A1,A9,A10,FUNCT_3:def 5; hence thesis by A8,A11,A12; end; theorem Th6: for X, Y being non empty TopSpace, x being Point of X, f being Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f" = <:id Y, Y --> x:> proof let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | { x}:], Y; set Z = {x}; set idZ = id Y; A1: rng idZ c= the carrier of Y; assume A2: f = pr1(the carrier of Y, Z); then A3: rng f = the carrier of Y by FUNCT_3:44; reconsider Z as non empty Subset of X; reconsider idY = Y --> x as continuous Function of Y, (X|Z) by Th2; reconsider KA = <:idZ, idY:> as continuous Function of Y, [:Y, (X|Z):] by YELLOW12:41; A4: [:the carrier of Y, Z:] c= rng KA proof let y be object; assume y in [:the carrier of Y, Z:]; then consider y1, y2 being object such that A5: y1 in the carrier of Y and A6: y2 in {x} & y = [y1,y2] by ZFMISC_1:def 2; A7: y = [y1, x] by A6,TARSKI:def 1; A8: idY.y1 = ((the carrier of Y) --> x).y1 .= x by A5,FUNCOP_1:7; A9: y1 in dom KA by A5,FUNCT_2:def 1; then KA. y1 = [idZ.y1, idY.y1] by FUNCT_3:def 7 .= [y1, x] by A5,A8,FUNCT_1:18; hence thesis by A7,A9,FUNCT_1:def 3; end; rng idY c= the carrier of (X|Z); then A10: rng idY c= Z by PRE_TOPC:8; then rng KA c= [:rng idZ, rng idY:] & [:rng idZ, rng idY:] c= [:the carrier of Y, Z:] by FUNCT_3:51,ZFMISC_1:96; then rng KA c= [:the carrier of Y, Z:]; then A11: rng KA = [:the carrier of Y, Z:] by A4 .= dom f by A2,FUNCT_3:def 4; A12: f is one-to-one by A2,Th4; A13: f is onto by A3,FUNCT_2:def 3; dom idY = the carrier of Y by FUNCT_2:def 1 .= dom idZ by FUNCT_2:def 1; then f*KA = id rng f by A2,A3,A10,A1,FUNCT_3:52; then KA = (f qua Function)" by A12,A11,FUNCT_1:42; hence thesis by A12,A13,TOPS_2:def 4; end; theorem Th7: for X, Y being non empty TopSpace, x being Point of X, f being Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f" = <:Y --> x, id Y:> proof let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x}, Y:], Y; set Z = {x}; set idY = id Y; A1: rng idY c= the carrier of Y; assume A2: f = pr2(Z, the carrier of Y); then A3: rng f = the carrier of Y by FUNCT_3:46; reconsider Z as non empty Subset of X; reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2; reconsider KA = <:idZ, idY:> as continuous Function of Y, [:(X|Z), Y:] by YELLOW12:41; A4: [:{x}, the carrier of Y:] c= rng KA proof let y be object; assume y in [:{x}, the carrier of Y:]; then consider y1, y2 being object such that A5: y1 in {x} and A6: y2 in the carrier of Y and A7: y = [y1,y2] by ZFMISC_1:def 2; A8: y = [x, y2] by A5,A7,TARSKI:def 1; A9: idZ.y2 = ((the carrier of Y) --> x).y2 .= x by A6,FUNCOP_1:7; A10: y2 in dom KA by A6,FUNCT_2:def 1; then KA. y2 = [idZ.y2, idY.y2] by FUNCT_3:def 7 .= [x, y2] by A6,A9,FUNCT_1:18; hence thesis by A8,A10,FUNCT_1:def 3; end; rng idZ c= the carrier of (X|Z); then A11: rng idZ c= Z by PRE_TOPC:8; then rng KA c= [:rng idZ, rng idY:] & [:rng idZ, rng idY:] c= [:{x},the carrier of Y:] by FUNCT_3:51,ZFMISC_1:96; then rng KA c= [:{x}, the carrier of Y:]; then A12: rng KA = [:Z, the carrier of Y:] by A4 .= dom f by A2,FUNCT_3:def 5; A13: f is one-to-one by A2,Th5; A14: f is onto by A3,FUNCT_2:def 3; dom idZ = the carrier of Y by FUNCT_2:def 1 .= dom idY by FUNCT_2:def 1; then f*KA = id rng f by A2,A3,A11,A1,FUNCT_3:52; then KA = (f qua Function)" by A13,A12,FUNCT_1:42; hence thesis by A13,A14,TOPS_2:def 4; end; theorem for X, Y being non empty TopSpace, x being Point of X, f being Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f is being_homeomorphism proof let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | { x}:], Y; set Z = {x}; assume A1: f = pr1(the carrier of Y, Z); thus dom f = [#][:Y, (X|Z):] by FUNCT_2:def 1; thus rng f = [#]Y by A1,FUNCT_3:44; thus f is one-to-one by A1,Th4; the carrier of (X|Z) = Z by PRE_TOPC:8; hence f is continuous by A1,YELLOW12:39; reconsider Z as non empty Subset of X; reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2; reconsider KA = <:id Y, idZ:> as continuous Function of Y, [:Y, (X|Z):] by YELLOW12:41; KA = f" by A1,Th6; hence thesis; end; theorem Th9: for X, Y being non empty TopSpace, x being Point of X, f being Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f is being_homeomorphism proof let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x}, Y:], Y; set Z = {x}; assume A1: f = pr2(Z, the carrier of Y); thus dom f = [#][:(X|Z), Y:] by FUNCT_2:def 1; thus rng f = [#]Y by A1,FUNCT_3:46; thus f is one-to-one by A1,Th5; the carrier of (X|Z) = Z by PRE_TOPC:8; hence f is continuous by A1,YELLOW12:40; reconsider Z as non empty Subset of X; reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2; reconsider KA = <:idZ, id Y:> as continuous Function of Y, [:(X|Z), Y:] by YELLOW12:41; KA = f" by A1,Th7; hence thesis; end; begin :: On the product of compact spaces theorem for X being non empty TopSpace, Y being compact non empty TopSpace, G being open Subset of [:X, Y:], x being set st [:{x}, the carrier of Y:] c= G ex f being ManySortedSet of the carrier of Y st for i being object st i in the carrier of Y ex G1 being Subset of X, H1 being Subset of Y st f.i = [G1,H1] & [ x, i] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G proof let X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:X, Y:], x be set; set y = the Point of Y; A1: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] & [x,y] in [:{x},the carrier of Y:] by BORSUK_1:def 2,ZFMISC_1:105; defpred P[object,object] means ex G1 be Subset of X, H1 be Subset of Y st $2 = [ G1,H1] & [x, $1] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G; assume A2: [:{x}, the carrier of Y:] c= G; then [:{x}, the carrier of Y:] c= the carrier of [:X,Y:] by XBOOLE_1:1; then reconsider x9 = x as Point of X by A1,ZFMISC_1:87; A3: [:{x9}, the carrier of Y:] c= union Base-Appr G by A2,BORSUK_1:13; A4: now let y be set; A5: x in {x9} by TARSKI:def 1; assume y in the carrier of Y; then [x,y] in [:{x9}, the carrier of Y:] by A5,ZFMISC_1:87; then consider Z be set such that A6: [x, y] in Z and A7: Z in Base-Appr G by A3,TARSKI:def 4; Base-Appr G = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y: [:X1,Y1:] c= G & X1 is open & Y1 is open} by BORSUK_1:def 3; then ex X1 be Subset of X, Y1 be Subset of Y st Z = [:X1, Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open by A7; hence ex G1 be Subset of X, H1 be Subset of Y st [x, y] in [:G1, H1:] & [: G1,H1:] c= G & G1 is open & H1 is open by A6; end; A8: for i be object st i in the carrier of Y ex j be object st P[i,j] proof let i be object; assume i in the carrier of Y; then consider G1 be Subset of X, H1 be Subset of Y such that A9: [x, i] in [:G1, H1:] & [:G1, H1:] c= G & G1 is open & H1 is open by A4; ex G2 be Subset of X, H2 be Subset of Y st [G1,H1] = [G2,H2] & [x, i] in [:G2, H2:] & G2 is open & H2 is open & [:G2, H2:] c= G by A9; hence thesis; end; ex f being ManySortedSet of the carrier of Y st for i be object st i in the carrier of Y holds P[i,f.i] from PBOOLE:sch 3 (A8 ); hence thesis; end; theorem Th11: for X being non empty TopSpace, Y being compact non empty TopSpace, G being open Subset of [:Y, X:] holds for x being set st [:[#]Y, {x} :] c= G holds ex R be open Subset of X st x in R & R c= { y where y is Point of X: [:[#]Y, {y}:] c= G } proof let X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:Y, X:]; let x be set; set y = the Point of Y; A1: the carrier of [:Y,X:] = [: the carrier of Y, the carrier of X:] & [y,x] in [:the carrier of Y,{x}:] by BORSUK_1:def 2,ZFMISC_1:106; assume A2: [:[#]Y, {x}:] c= G; then [:[#]Y,{x}:] c= the carrier of [:Y,X:] by XBOOLE_1:1; then reconsider x9 = x as Point of X by A1,ZFMISC_1:87; Int G = G by TOPS_1:23; then [#]Y is compact & G is a_neighborhood of [:[#]Y, {x9}:] by A2,COMPTS_1:1 ,CONNSP_2:def 2; then consider W being a_neighborhood of [#]Y, V being a_neighborhood of x9 such that A3: [:W, V:] c= G by BORSUK_1:25; take R = Int V; Int W c= W & [#]Y c= Int W by CONNSP_2:def 2,TOPS_1:16; then A4: [#]Y c= W; A5: Int V c= V by TOPS_1:16; R c= { z where z is Point of X : [:[#]Y, {z}:] c= G } proof let r be object; assume A6: r in R; then reconsider r9 = r as Point of X; {r} c= V by A5,A6,ZFMISC_1:31; then [:[#]Y, {r9}:] c= [:W, V:] by A4,ZFMISC_1:96; then [:[#]Y, {r9}:] c= G by A3; hence thesis; end; hence thesis by CONNSP_2:def 1; end; theorem Th12: for X being non empty TopSpace, Y being compact non empty TopSpace, G being open Subset of [:Y, X:] holds { x where x is Point of X : [: [#]Y, {x}:] c= G } in the topology of X proof let X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:Y, X:]; set Q = { x where x is Point of X : [:[#]Y, {x}:] c= G }; Q c= the carrier of X proof let q be object; assume q in Q; then ex x9 being Point of X st q = x9 & [:[#]Y, {x9}:] c= G; hence thesis; end; then reconsider Q as Subset of X; defpred P[set] means ex y be set st y in Q & ex S be Subset of X st S = $1 & S is open & y in S & S c= Q; consider RR be set such that A1: for x be set holds x in RR iff x in bool Q & P[x] from XFAMILY:sch 1; RR c= bool Q by A1; then reconsider RR as Subset-Family of Q; Q c= union RR proof let a be object; assume a in Q; then ex x9 being Point of X st a = x9 & [:[#]Y, {x9}:] c= G; then consider R be open Subset of X such that A2: a in R and A3: R c= Q by Th11; R in RR by A1,A2,A3; hence thesis by A2,TARSKI:def 4; end; then A4: union RR = Q; bool Q c= bool the carrier of X by ZFMISC_1:67; then reconsider RR as Subset-Family of X by XBOOLE_1:1; RR c= the topology of X proof let x be object; assume x in RR; then ex y be set st y in Q & ex S be Subset of X st S = x & S is open & y in S & S c= Q by A1; hence thesis by PRE_TOPC:def 2; end; hence thesis by A4,PRE_TOPC:def 1; end; theorem Th13: for X, Y being non empty TopSpace, x being Point of X holds [: X | {x}, Y :], Y are_homeomorphic proof let X be non empty TopSpace, Y be non empty TopSpace, x be Point of X; set Z = {x}; the carrier of [:(X|Z), Y:] = [:the carrier of (X|Z), the carrier of Y :] by BORSUK_1:def 2 .= [:Z, the carrier of Y:] by PRE_TOPC:8; then reconsider f= pr2(Z, the carrier of Y) as Function of [:X|Z, Y:], Y; take f; thus thesis by Th9; end; Lm3: for X being non empty TopSpace, Y being non empty TopSpace, x being Point of X, Z being non empty Subset of X st Z = {x} holds [: Y, X | Z :], Y are_homeomorphic proof let X be non empty TopSpace, Y be non empty TopSpace, x be Point of X, Z be non empty Subset of X; [: Y, X | Z :], [: X | Z, Y :] are_homeomorphic by YELLOW12:44; then consider g being Function of [: Y, X | Z :], [: X | Z, Y :] such that A1: g is being_homeomorphism; assume Z = {x}; then [: X | Z, Y :], Y are_homeomorphic by Th13; then consider f being Function of [: X | Z, Y :], Y such that A2: f is being_homeomorphism; reconsider gf = f * g as Function of [: Y, X | Z :], Y; gf is being_homeomorphism by A2,A1,TOPS_2:57; hence thesis; end; theorem Th14: for S, T being non empty TopSpace st S, T are_homeomorphic & S is compact holds T is compact proof let S, T be non empty TopSpace; assume that A1: S, T are_homeomorphic and A2: S is compact; consider f being Function of S, T such that A3: f is being_homeomorphism by A1; f is continuous & rng f = [#] T by A3; hence thesis by A2,COMPTS_1:14; end; theorem Th15: for X, Y being TopSpace, XV being SubSpace of X holds [:Y, XV:] is SubSpace of [:Y, X:] proof let X, Y be TopSpace, XV be SubSpace of X; set S = [:Y, XV:], T = [:Y, X:]; A1: the carrier of [:Y, XV:] = [:the carrier of Y, the carrier of XV:] by BORSUK_1:def 2; A2: the carrier of [:Y, X:] = [:the carrier of Y, the carrier of X:] & the carrier of XV c= the carrier of X by BORSUK_1:1,def 2; A3: for P being Subset of S holds P in the topology of S iff ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S proof reconsider oS = [#]S as Subset of T by A1,A2,ZFMISC_1:96; let P be Subset of S; reconsider P9 = P as Subset of S; hereby assume P in the topology of S; then P9 is open by PRE_TOPC:def 2; then consider A being Subset-Family of S such that A4: P9 = union A and A5: for e be set st e in A ex X1 being Subset of Y, Y1 being Subset of XV st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5; set AA = {[:X1, Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st Y1 = Y2 /\ [#](XV) & X1 is open & Y2 is open & [:X1, Y1:] in A }; AA c= bool the carrier of T proof let a be object; assume a in AA; then ex Xx1 being Subset of Y, Yy2 being Subset of X st a = [: Xx1, Yy2 :] & ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open & Yy2 is open & [:Xx1, Y1:] in A; hence thesis; end; then reconsider AA as Subset-Family of T; reconsider AA as Subset-Family of T; A6: P c= union AA /\ [#]S proof let p be object; assume p in P; then consider A1 be set such that A7: p in A1 and A8: A1 in A by A4,TARSKI:def 4; reconsider A1 as Subset of S by A8; consider X2 being Subset of Y, Y2 being Subset of XV such that A9: A1 = [:X2,Y2:] and A10: X2 is open and A11: Y2 is open by A5,A8; Y2 in the topology of XV by A11,PRE_TOPC:def 2; then consider Q1 being Subset of X such that A12: Q1 in the topology of X and A13: Y2 = Q1 /\ [#]XV by PRE_TOPC:def 4; consider p1, p2 being object such that A14: p1 in X2 and A15: p2 in Y2 and A16: p = [p1, p2] by A7,A9,ZFMISC_1:def 2; reconsider Q1 as Subset of X; set EX = [:X2, Q1:]; p2 in Q1 by A15,A13,XBOOLE_0:def 4; then A17: p in EX by A14,A16,ZFMISC_1:87; Q1 is open by A12,PRE_TOPC:def 2; then EX in {[:Xx1, Yy2:] where Xx1 is Subset of Y, Yy2 is Subset of X: ex Z1 being Subset of XV st Z1 = Yy2 /\ [#](XV) & Xx1 is open & Yy2 is open & [:Xx1, Z1:] in A } by A8,A9,A10,A13; then p in union AA by A17,TARSKI:def 4; hence thesis by A7,A8,XBOOLE_0:def 4; end; AA c= the topology of T proof let t be object; set A9 = { t }; assume t in AA; then consider Xx1 being Subset of Y, Yy2 being Subset of X such that A18: t = [:Xx1, Yy2:] and A19: ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open & Yy2 is open & [:Xx1, Y1:] in A; A9 c= bool the carrier of T proof let a be object; assume a in A9; then a = t by TARSKI:def 1; hence thesis by A18; end; then reconsider A9 as Subset-Family of T; A20: A9 c= { [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : X1 in the topology of Y & Y1 in the topology of X } proof let x be object; assume x in A9; then A21: x = [:Xx1,Yy2:] by A18,TARSKI:def 1; Xx1 in the topology of Y & Yy2 in the topology of X by A19, PRE_TOPC:def 2; hence thesis by A21; end; t = union A9; then t in { union As where As is Subset-Family of T : As c= { [:X1,Y1 :] where X1 is Subset of Y, Y1 is Subset of X : X1 in the topology of Y & Y1 in the topology of X}} by A20; hence thesis by BORSUK_1:def 2; end; then A22: union AA in the topology of T by PRE_TOPC:def 1; union AA /\ [#]S c= P proof let h be object; assume A23: h in union AA /\ [#]S; then h in union AA by XBOOLE_0:def 4; then consider A2 being set such that A24: h in A2 and A25: A2 in AA by TARSKI:def 4; consider Xx1 being Subset of Y, Yy2 being Subset of X such that A26: A2 = [:Xx1, Yy2:] and A27: ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open & Yy2 is open & [:Xx1, Y1:] in A by A25; consider Yy1 being Subset of XV such that A28: Yy1 = Yy2 /\ [#](XV) and Xx1 is open and Yy2 is open and A29: [:Xx1, Yy1:] in A by A27; consider p1, p2 being object such that A30: p1 in Xx1 and A31: p2 in Yy2 and A32: h = [p1, p2] by A24,A26,ZFMISC_1:def 2; p2 in the carrier of XV by A1,A23,A32,ZFMISC_1:87; then p2 in Yy2 /\ [#]XV by A31,XBOOLE_0:def 4; then h in [:Xx1, Yy1:] by A30,A32,A28,ZFMISC_1:87; hence thesis by A4,A29,TARSKI:def 4; end; then P = union AA /\ [#]S by A6; hence ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S by A22; end; given Q being Subset of T such that A33: Q in the topology of T and A34: P = Q /\ [#]S; reconsider Q9 = Q as Subset of T; Q9 is open by A33,PRE_TOPC:def 2; then consider A being Subset-Family of T such that A35: Q9 = union A and A36: for e be set st e in A ex X1 being Subset of Y, Y1 being Subset of X st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5; reconsider A as Subset-Family of T; reconsider AA = A | oS as Subset-Family of T|oS; reconsider AA as Subset-Family of S by PRE_TOPC:8; reconsider AA as Subset-Family of S; A37: for e be set st e in AA ex X1 being Subset of Y, Y1 being Subset of XV st e = [:X1,Y1:] & X1 is open & Y1 is open proof let e be set; assume A38: e in AA; then reconsider e9 = e as Subset of T|oS; consider R being Subset of T such that A39: R in A and A40: R /\ oS = e9 by A38,TOPS_2:def 3; consider X1 being Subset of Y, Y1 being Subset of X such that A41: R = [:X1,Y1:] and A42: X1 is open and A43: Y1 is open by A36,A39; reconsider D2 = Y1 /\ [#]XV as Subset of XV; Y1 in the topology of X by A43,PRE_TOPC:def 2; then D2 in the topology of XV by PRE_TOPC:def 4; then A44: D2 is open by PRE_TOPC:def 2; [#][:Y, XV:] = [:[#]Y, [#]XV:] by BORSUK_1:def 2; then e9 = [:X1 /\ [#]Y, Y1 /\ [#](XV):] by A40,A41,ZFMISC_1:100; hence thesis by A42,A44; end; A45: union A /\ oS c= union AA proof let s be object; assume A46: s in union A /\ oS; then s in union A by XBOOLE_0:def 4; then consider A1 being set such that A47: s in A1 and A48: A1 in A by TARSKI:def 4; s in oS by A46,XBOOLE_0:def 4; then A49: s in A1 /\ oS by A47,XBOOLE_0:def 4; reconsider A1 as Subset of T by A48; A1 /\ oS in AA by A48,TOPS_2:31; hence thesis by A49,TARSKI:def 4; end; union AA c= union A by TOPS_2:34; then union AA c= union A /\ oS by XBOOLE_1:19; then P = union AA by A34,A35,A45; then P9 is open by A37,BORSUK_1:5; hence thesis by PRE_TOPC:def 2; end; [#]S c= [#]T by A1,A2,ZFMISC_1:96; hence thesis by A3,PRE_TOPC:def 4; end; Lm4: for X, Y being TopSpace, Z being Subset of [:Y, X:], V being Subset of X st Z = [:[#]Y, V:] holds the TopStruct of [:Y, X | V:] = the TopStruct of [:Y, X:] | Z proof let X, Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X; reconsider A = [:Y, X | V:] as SubSpace of [:Y, X:] by Th15; assume A1: Z = [:[#]Y, V:]; the carrier of A = [:the carrier of Y, the carrier of (X|V):] by BORSUK_1:def 2 .= Z by A1,PRE_TOPC:8 .= the carrier of ([:Y, X:]|Z) by PRE_TOPC:8; then A is SubSpace of [:Y, X:] | Z & [:Y, X:] | Z is SubSpace of A by TOPMETR:3; hence thesis by TSEP_1:6; end; theorem Th16: for X being non empty TopSpace, Y being compact non empty TopSpace, x being Point of X, Z being Subset of [:Y, X:] st Z = [:[#]Y, {x}:] holds Z is compact proof let X be non empty TopSpace, Y be compact non empty TopSpace, x be Point of X, Z be Subset of [:Y, X:]; reconsider V = {x} as non empty Subset of X; Y, [: Y, X | V :] are_homeomorphic by Lm3; then A1: [:Y, X | V:] is compact by Th14; assume A2: Z = [:[#]Y, {x}:]; then the TopStruct of [:Y, X | V:] = the TopStruct of ([:Y, X:] | Z) by Lm4; hence thesis by A2,A1,COMPTS_1:3; end; registration let X be non empty TopSpace, Y be compact non empty TopSpace, x be Point of X; cluster [:Y, X|{x}:] -> compact; coherence proof Y, [: Y, X | {x} :] are_homeomorphic by Lm3; hence thesis by Th14; end; end; theorem for X, Y being compact non empty TopSpace, R being Subset-Family of X st R = { Q where Q is open Subset of X : [:[#]Y, Q:] c= union Base-Appr [#][:Y, X:] } holds R is open & R is Cover of [#]X proof let X, Y be compact non empty TopSpace, R be Subset-Family of X; assume A1: R = { Q where Q is open Subset of X : [:[#]Y, Q:] c= union Base-Appr [#][:Y, X:] }; now let P be Subset of X; assume P in R; then ex E being open Subset of X st E = P & [:[#]Y, E:] c= union Base-Appr [#][:Y, X:] by A1; hence P is open; end; hence R is open; [#]X c= union R proof let k be object; assume k in [#]X; then reconsider k9 = k as Point of X; reconsider Z = [:[#]Y, {k9}:] as Subset of [:Y, X:]; Z c= [#][:Y, X:]; then Z c= union Base-Appr [#][:Y, X:] by BORSUK_1:13; then A2: Base-Appr [#][:Y, X:] is Cover of Z by SETFAM_1:def 11; Z is compact by Th16; then consider G being Subset-Family of [:Y, X:] such that A3: G c= Base-Appr [#][:Y, X:] and A4: G is Cover of Z and G is finite by A2; set uR = union G; set Q = { x where x is Point of X : [:[#]Y, {x}:] c= uR }; Q c= the carrier of X proof let k be object; assume k in Q; then ex x1 being Point of X st k = x1 & [:[#]Y, {x1}:] c= uR; hence thesis; end; then reconsider Q as Subset of X; Z c= union G by A4,SETFAM_1:def 11; then A5: k9 in Q; A6: [:[#]Y, Q:] c= union Base-Appr [#][:Y, X:] proof let z be object; assume z in [:[#]Y, Q:]; then consider x1, x2 be object such that A7: x1 in [#]Y and A8: x2 in Q and A9: z = [x1, x2] by ZFMISC_1:def 2; consider x29 being Point of X such that A10: x29 = x2 and A11: [:[#]Y, {x29}:] c= uR by A8; x2 in {x29} by A10,TARSKI:def 1; then A12: z in [:[#]Y, {x29}:] by A7,A9,ZFMISC_1:87; uR c= union Base-Appr [#][:Y, X:] by A3,ZFMISC_1:77; then [:[#]Y, {x29}:] c= union Base-Appr [#][:Y, X:] by A11; hence thesis by A12; end; uR is open by A3,TOPS_2:11,19; then Q in the topology of X by Th12; then Q is open by PRE_TOPC:def 2; then Q in R by A1,A6; hence thesis by A5,TARSKI:def 4; end; hence thesis by SETFAM_1:def 11; end; theorem Th18: for X, Y being compact non empty TopSpace, R being Subset-Family of X, F being Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open & R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } holds R is open & R is Cover of X proof let X, Y be compact non empty TopSpace, R be Subset-Family of X, F be Subset-Family of [:Y, X:]; assume that A1: F is Cover of [:Y, X:] and A2: F is open and A3: R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ }; now let P be Subset of X; assume P in R; then ex E being open Subset of X st E = P & ex FQ being Subset-Family of [:Y , X:] st FQ c= F & FQ is finite & [: [#]Y, E:] c= union FQ by A3; hence P is open; end; hence R is open; A4: union F = [#] [:Y, X:] by A1,SETFAM_1:45; [#]X c= union R proof let k be object; assume k in [#]X; then reconsider k9 = k as Point of X; reconsider Z = [:[#]Y, {k9}:] as Subset of [:Y, X:]; F is Cover of Z & Z is compact by A4,Th16,SETFAM_1:def 11; then consider G being Subset-Family of [:Y, X:] such that A5: G c= F and A6: G is Cover of Z and A7: G is finite by A2; set uR = union G; set Q = { x where x is Point of X : [:[#]Y, {x}:] c= uR }; Q c= the carrier of X proof let k be object; assume k in Q; then ex x1 being Point of X st k = x1 & [:[#]Y, {x1}:] c= uR; hence thesis; end; then reconsider Q as Subset of X; Z c= union G by A6,SETFAM_1:def 11; then A8: k9 in Q; A9: ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [: [#]Y, Q:] c= union FQ proof take G; [:[#]Y, Q:] c= union G proof let z be object; assume z in [:[#]Y, Q:]; then consider x1, x2 be object such that A10: x1 in [#]Y and A11: x2 in Q and A12: z = [x1, x2] by ZFMISC_1:def 2; consider x29 being Point of X such that A13: x29 = x2 and A14: [:[#]Y, {x29}:] c= uR by A11; x2 in {x29} by A13,TARSKI:def 1; then z in [:[#]Y, {x29}:] by A10,A12,ZFMISC_1:87; hence thesis by A14; end; hence thesis by A5,A7; end; uR is open by A2,A5,TOPS_2:11,19; then Q in the topology of X by Th12; then Q is open by PRE_TOPC:def 2; then Q in R by A3,A9; hence thesis by A8,TARSKI:def 4; end; hence thesis by SETFAM_1:def 11; end; theorem Th19: for X, Y being compact non empty TopSpace, R being Subset-Family of X, F being Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open & R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } holds ex C being Subset-Family of X st C c= R & C is finite & C is Cover of X proof let X, Y be compact non empty TopSpace, R be Subset-Family of X, F be Subset-Family of [:Y, X:]; assume F is Cover of [:Y, X:] & F is open & R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y , Q:] c= union FQ }; then R is open & R is Cover of X by Th18; then ex G being Subset-Family of X st G c= R & G is Cover of X & G is finite by COMPTS_1:def 1; hence thesis; end; theorem Th20: for X, Y being compact non empty TopSpace, F being Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open ex G being Subset-Family of [:Y, X:] st G c= F & G is Cover of [:Y, X:] & G is finite proof let X, Y be compact non empty TopSpace; let F be Subset-Family of [:Y, X:]; set R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ }; R c= bool the carrier of X proof let s be object; assume s in R; then ex Q1 being open Subset of X st s = Q1 & ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [: [#]Y, Q1:] c= union FQ; hence thesis; end; then reconsider R as Subset-Family of X; reconsider R as Subset-Family of X; defpred P[object,object] means ex D1 being set, FQ being Subset-Family of [:Y, X:] st D1 = $1 & FQ c= F & FQ is finite & [:[#]Y, D1:] c= union FQ & $2 = FQ; deffunc F(set) = [:[#]Y, $1:]; assume F is Cover of [:Y, X:] & F is open; then consider C being Subset-Family of X such that A1: C c= R and A2: C is finite and A3: C is Cover of X by Th19; set CX = { F(f) where f is Subset of X : f in C }; CX c= bool the carrier of [:Y, X:] proof let s be object; assume s in CX; then consider f1 being Subset of X such that A4: s = F(f1) and f1 in C; [:[#]Y, f1:] c= the carrier of [:Y, X:]; hence thesis by A4; end; then reconsider CX as Subset-Family of [:Y, X:]; reconsider CX as Subset-Family of [:Y, X:]; A5: for e be object st e in C ex u be object st P[e,u] proof let e be object; assume e in C; then e in R by A1; then ex Q1 being open Subset of X st Q1 = e & ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q1:] c= union FQ; hence thesis; end; consider t being Function such that A6: dom t = C & for s being object st s in C holds P[s, t.s] from CLASSES1 :sch 1(A5); set G = union rng t; A7: union rng t c= F proof let k be object; assume k in union rng t; then consider K be set such that A8: k in K and A9: K in rng t by TARSKI:def 4; consider x1 be object such that A10: x1 in dom t & K = t.x1 by A9,FUNCT_1:def 3; reconsider x1 as set by TARSKI:1; P[x1, t.x1] by A6,A10; then ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [: [#]Y, x1:] c= union FQ & K = FQ by A10; hence thesis by A8; end; G c= bool the carrier of [:Y, X:] proof let s be object; assume s in G; then s in F by A7; hence thesis; end; then reconsider G as Subset-Family of [:Y, X:]; reconsider G as Subset-Family of [:Y, X:]; take G; thus G c= F by A7; union CX = [:[#]Y, union C:] proof hereby let g be object; assume g in union CX; then consider GG being set such that A11: g in GG and A12: GG in CX by TARSKI:def 4; consider FF being Subset of X such that A13: GG = [:[#]Y, FF:] and A14: FF in C by A12; consider g1, g2 be object such that A15: g1 in [#]Y and A16: g2 in FF and A17: g = [g1, g2] by A11,A13,ZFMISC_1:def 2; g2 in union C by A14,A16,TARSKI:def 4; hence g in [:[#]Y, union C:] by A15,A17,ZFMISC_1:87; end; let g be object; assume g in [:[#]Y, union C:]; then consider g1, g2 be object such that A18: g1 in [#]Y and A19: g2 in union C and A20: g = [g1, g2] by ZFMISC_1:def 2; consider GG being set such that A21: g2 in GG and A22: GG in C by A19,TARSKI:def 4; GG in { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } by A1,A22; then consider Q1 being open Subset of X such that A23: GG = Q1 and ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [: [#]Y, Q1:] c= union FQ; A24: [:[#]Y, Q1:] in CX by A22,A23; g in [:[#]Y, Q1:] by A18,A20,A21,A23,ZFMISC_1:87; hence thesis by A24,TARSKI:def 4; end; then A25: union CX = [:[#]Y, [#]X:] by A3,SETFAM_1:45 .= [#][:Y, X:] by BORSUK_1:def 2; [#][:Y, X:] c= union union rng t proof let d be object; assume d in [#][:Y, X:]; then consider CC being set such that A26: d in CC and A27: CC in CX by A25,TARSKI:def 4; consider Cc being Subset of X such that A28: CC = [:[#]Y, Cc:] and A29: Cc in C by A27; Cc in R by A1,A29; then consider Qq being open Subset of X such that A30: Cc = Qq and ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [: [#]Y, Qq:] c= union FQ; P[Cc, t.Cc] by A6,A29; then consider FQ1 being Subset-Family of [:Y, X:] such that FQ1 c= F and FQ1 is finite and A31: [:[#]Y, Qq:] c= union FQ1 and A32: t.Qq = FQ1 by A30; consider DC being set such that A33: d in DC and A34: DC in FQ1 by A26,A28,A30,A31,TARSKI:def 4; FQ1 in rng t by A6,A29,A30,A32,FUNCT_1:def 3; then DC in union rng t by A34,TARSKI:def 4; hence thesis by A33,TARSKI:def 4; end; hence G is Cover of [:Y, X:] by SETFAM_1:def 11; A35: for X1 be set st X1 in rng t holds X1 is finite proof let X1 be set; assume X1 in rng t; then consider x1 be object such that A36: x1 in dom t and A37: X1 = t.x1 by FUNCT_1:def 3; reconsider x1 as set by TARSKI:1; P[x1, t.x1] by A6,A36; then ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [: [#]Y, x1:] c= union FQ & t.x1 = FQ; hence thesis by A37; end; rng t is finite by A2,A6,FINSET_1:8; hence thesis by A35,FINSET_1:7; end; Lm5: for T1, T2 be compact non empty TopSpace holds [:T1, T2:] is compact by Th20; registration let T1,T2 be compact TopSpace; cluster [:T1, T2:] -> compact; coherence proof per cases; suppose T1 is non empty & T2 is non empty; hence thesis by Lm5; end; suppose T1 is empty & T2 is empty; hence thesis; end; suppose T1 is empty & T2 is non empty; hence thesis; end; suppose T1 is non empty & T2 is empty; hence thesis; end; end; end; Lm6: for X, Y being TopSpace, XV being SubSpace of X holds [:XV, Y:] is SubSpace of [:X, Y:] proof let X, Y be TopSpace, XV be SubSpace of X; set S = [:XV, Y:], T = [:X, Y:]; A1: the carrier of S = [:the carrier of XV, the carrier of Y:] by BORSUK_1:def 2; A2: the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] & the carrier of XV c= the carrier of X by BORSUK_1:1,def 2; A3: for P being Subset of S holds P in the topology of S iff ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S proof reconsider oS = [#]S as Subset of T by A1,A2,ZFMISC_1:96; let P be Subset of S; reconsider P9 = P as Subset of S; hereby assume P in the topology of S; then P9 is open by PRE_TOPC:def 2; then consider A being Subset-Family of S such that A4: P9 = union A and A5: for e be set st e in A ex X1 being Subset of XV, Y1 being Subset of Y st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5; set AA = {[:X1, Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st Y1 = X1 /\ [#](XV) & X1 is open & Y2 is open & [:Y1, Y2:] in A }; AA c= bool the carrier of T proof let a be object; assume a in AA; then ex Xx1 being Subset of X, Yy2 being Subset of Y st a = [: Xx1, Yy2 :] & ex Y1 being Subset of XV st Y1 = Xx1 /\ [#](XV) & Xx1 is open & Yy2 is open & [:Y1, Yy2:] in A; hence thesis; end; then reconsider AA as Subset-Family of T; reconsider AA as Subset-Family of T; A6: P c= union AA /\ [#]S proof let p be object; assume p in P; then consider A1 be set such that A7: p in A1 and A8: A1 in A by A4,TARSKI:def 4; reconsider A1 as Subset of S by A8; consider X2 being Subset of XV, Y2 being Subset of Y such that A9: A1 = [:X2,Y2:] and A10: X2 is open and A11: Y2 is open by A5,A8; X2 in the topology of XV by A10,PRE_TOPC:def 2; then consider Q1 being Subset of X such that A12: Q1 in the topology of X and A13: X2 = Q1 /\ [#]XV by PRE_TOPC:def 4; consider p1, p2 being object such that A14: p1 in X2 and A15: p2 in Y2 & p = [p1, p2] by A7,A9,ZFMISC_1:def 2; reconsider Q1 as Subset of X; set EX = [:Q1, Y2:]; p1 in Q1 by A14,A13,XBOOLE_0:def 4; then A16: p in EX by A15,ZFMISC_1:87; Q1 is open by A12,PRE_TOPC:def 2; then EX in {[:Xx1, Yy2:] where Xx1 is Subset of X, Yy2 is Subset of Y: ex Z1 being Subset of XV st Z1 = Xx1 /\ [#](XV) & Xx1 is open & Yy2 is open & [:Z1, Yy2:] in A } by A8,A9,A11,A13; then p in union AA by A16,TARSKI:def 4; hence thesis by A7,A8,XBOOLE_0:def 4; end; AA c= the topology of T proof let t be object; set A9 = { t }; assume t in AA; then consider Xx1 being Subset of X, Yy2 being Subset of Y such that A17: t = [:Xx1, Yy2:] and A18: ex Y1 being Subset of XV st Y1 = Xx1 /\ [#](XV) & Xx1 is open & Yy2 is open & [:Y1, Yy2:] in A; A9 c= bool the carrier of T proof let a be object; assume a in A9; then a = t by TARSKI:def 1; hence thesis by A17; end; then reconsider A9 as Subset-Family of T; A19: A9 c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : X1 in the topology of X & Y1 in the topology of Y } proof let x be object; assume x in A9; then A20: x = [:Xx1,Yy2:] by A17,TARSKI:def 1; Xx1 in the topology of X & Yy2 in the topology of Y by A18, PRE_TOPC:def 2; hence thesis by A20; end; t = union A9; then t in { union As where As is Subset-Family of T : As c= { [:X1,Y1 :] where X1 is Subset of X, Y1 is Subset of Y : X1 in the topology of X & Y1 in the topology of Y}} by A19; hence thesis by BORSUK_1:def 2; end; then A21: union AA in the topology of T by PRE_TOPC:def 1; union AA /\ [#]S c= P proof let h be object; assume A22: h in union AA /\ [#]S; then h in union AA by XBOOLE_0:def 4; then consider A2 being set such that A23: h in A2 and A24: A2 in AA by TARSKI:def 4; consider Xx1 being Subset of X, Yy2 being Subset of Y such that A25: A2 = [:Xx1, Yy2:] and A26: ex Y1 being Subset of XV st Y1 = Xx1 /\ [#]XV & Xx1 is open & Yy2 is open & [:Y1, Yy2:] in A by A24; consider Yy1 being Subset of XV such that A27: Yy1 = Xx1 /\ [#]XV and Xx1 is open and Yy2 is open and A28: [:Yy1, Yy2:] in A by A26; consider p1, p2 being object such that A29: p1 in Xx1 and A30: p2 in Yy2 and A31: h = [p1, p2] by A23,A25,ZFMISC_1:def 2; p1 in the carrier of XV by A1,A22,A31,ZFMISC_1:87; then p1 in Xx1 /\ [#](XV) by A29,XBOOLE_0:def 4; then h in [:Yy1, Yy2:] by A30,A31,A27,ZFMISC_1:87; hence thesis by A4,A28,TARSKI:def 4; end; then P = union AA /\ [#]S by A6; hence ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S by A21; end; given Q being Subset of T such that A32: Q in the topology of T and A33: P = Q /\ [#]S; reconsider Q9 = Q as Subset of T; Q9 is open by A32,PRE_TOPC:def 2; then consider A being Subset-Family of T such that A34: Q9 = union A and A35: for e be set st e in A ex X1 being Subset of X, Y1 being Subset of Y st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5; reconsider A as Subset-Family of T; reconsider AA = A | oS as Subset-Family of T|oS; reconsider AA as Subset-Family of S by PRE_TOPC:8; reconsider AA as Subset-Family of S; A36: for e be set st e in AA ex X1 being Subset of XV, Y1 being Subset of Y st e = [:X1,Y1:] & X1 is open & Y1 is open proof let e be set; assume A37: e in AA; then reconsider e9 = e as Subset of T|oS; consider R being Subset of T such that A38: R in A and A39: R /\ oS = e9 by A37,TOPS_2:def 3; consider X1 being Subset of X, Y1 being Subset of Y such that A40: R = [:X1,Y1:] and A41: X1 is open and A42: Y1 is open by A35,A38; reconsider D2 = X1 /\ [#](XV) as Subset of XV; X1 in the topology of X by A41,PRE_TOPC:def 2; then D2 in the topology of XV by PRE_TOPC:def 4; then A43: D2 is open by PRE_TOPC:def 2; [#][:XV, Y:] = [:[#]XV, [#]Y:] by BORSUK_1:def 2; then e9 = [:X1 /\ [#]XV, Y1 /\ [#]Y:] by A39,A40,ZFMISC_1:100; hence thesis by A42,A43; end; A44: union A /\ oS c= union AA proof let s be object; assume A45: s in union A /\ oS; then s in union A by XBOOLE_0:def 4; then consider A1 being set such that A46: s in A1 and A47: A1 in A by TARSKI:def 4; s in oS by A45,XBOOLE_0:def 4; then A48: s in A1 /\ oS by A46,XBOOLE_0:def 4; reconsider A1 as Subset of T by A47; A1 /\ oS in AA by A47,TOPS_2:31; hence thesis by A48,TARSKI:def 4; end; union AA c= union A by TOPS_2:34; then union AA c= union A /\ oS by XBOOLE_1:19; then P = union AA by A33,A34,A44; then P9 is open by A36,BORSUK_1:5; hence thesis by PRE_TOPC:def 2; end; [#]S c= [#]T by A1,A2,ZFMISC_1:96; hence thesis by A3,PRE_TOPC:def 4; end; theorem Th21: for X, Y being TopSpace, XV being SubSpace of X, YV being SubSpace of Y holds [:XV, YV:] is SubSpace of [:X, Y:] proof let X, Y be TopSpace, XV be SubSpace of X, YV be SubSpace of Y; [:XV, Y:] is SubSpace of [:X, Y:] & [:XV, YV:] is SubSpace of [:XV, Y:] by Lm6,Th15; hence thesis by TSEP_1:7; end; theorem Th22: for X, Y being TopSpace, Z being Subset of [:Y, X:], V being Subset of X, W being Subset of Y st Z = [:W, V:] holds the TopStruct of [:Y | W , X | V:] = the TopStruct of [:Y, X:] | Z proof let X, Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X, W be Subset of Y; reconsider A = [:Y | W, X | V:] as SubSpace of [:Y, X:] by Th21; assume A1: Z = [:W, V:]; the carrier of A = [:the carrier of (Y|W), the carrier of (X|V):] by BORSUK_1:def 2 .= [:the carrier of (Y|W), V:] by PRE_TOPC:8 .= Z by A1,PRE_TOPC:8 .= the carrier of ([:Y, X:]|Z) by PRE_TOPC:8; then A is SubSpace of [:Y, X:] | Z & [:Y, X:] | Z is SubSpace of A by TOPMETR:3; hence thesis by TSEP_1:6; end; registration let T be TopSpace; cluster empty for Subset of T; existence proof take {}T; thus thesis; end; end; registration let T be TopSpace, P be compact Subset of T; cluster T | P -> compact; coherence proof per cases; suppose P is non empty; hence thesis by COMPTS_1:3; end; suppose P is empty; hence thesis; end; end; end; theorem for T1, T2 being TopSpace, S1 being Subset of T1, S2 being Subset of T2 st S1 is compact & S2 is compact holds [:S1, S2:] is compact Subset of [:T1, T2:] proof let T1, T2 be TopSpace, S1 be Subset of T1, S2 be Subset of T2; assume that A1: S1 is compact and A2: S2 is compact; per cases; suppose A3: S1 is non empty & S2 is non empty; then (ex x be object st x in S1 )& ex y be object st y in S2; then reconsider T1, T2 as non empty TopSpace; reconsider S2 as compact non empty Subset of T2 by A2,A3; reconsider S1 as compact non empty Subset of T1 by A1,A3; reconsider X = [:S1, S2:] as Subset of [:T1, T2:]; the TopStruct of [:T1|S1, T2|S2:] = the TopStruct of ([:T1, T2:] | X) by Th22; hence thesis by COMPTS_1:3; end; suppose S1 is empty & S2 is non empty; then reconsider S1 as empty Subset of T1; [:S1, S2:] = {}([:T1, T2:]); hence thesis; end; suppose S1 is non empty & S2 is empty; then reconsider S2 as empty Subset of T2; [:S1, S2:] = {}([:T1, T2:]); hence thesis; end; suppose S1 is empty & S2 is empty; then reconsider S2 as empty Subset of T2; [:S1, S2:] = {}([:T1, T2:]); hence thesis; end; end;