:: BORSUK_3 semantic presentation begin theorem :: BORSUK_3:1 for S, T being TopSpace holds [#] [:S,T:] = [:([#] S),([#] T):] by BORSUK_1:def_2; theorem Th2: :: BORSUK_3:2 for X, Y being non empty TopSpace for x being Point of X holds Y --> x is continuous Function of Y,(X | {x}) proof let X, Y be non empty TopSpace; ::_thesis: for x being Point of X holds Y --> x is continuous Function of Y,(X | {x}) let x be Point of X; ::_thesis: Y --> x is continuous Function of Y,(X | {x}) set Z = {x}; set f = Y --> x; ( x in {x} & the carrier of (X | {x}) = {x} ) by PRE_TOPC:8, TARSKI:def_1; then reconsider g = Y --> x as Function of Y,(X | {x}) by FUNCOP_1:45; g is continuous by TOPMETR:6; hence Y --> x is continuous Function of Y,(X | {x}) ; ::_thesis: verum end; registration let T be TopStruct ; cluster id T -> being_homeomorphism ; coherence id T is being_homeomorphism by TOPGRP_1:20; end; Lm1: for S being TopStruct holds S,S are_homeomorphic proof let S be TopStruct ; ::_thesis: S,S are_homeomorphic take id S ; :: according to T_0TOPSP:def_1 ::_thesis: id S is being_homeomorphism thus id S is being_homeomorphism ; ::_thesis: verum 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 ; ::_thesis: ( S,T are_homeomorphic implies T,S are_homeomorphic ) assume S,T are_homeomorphic ; ::_thesis: T,S are_homeomorphic then consider f being Function of S,T such that A1: f is being_homeomorphism by T_0TOPSP:def_1; f " is being_homeomorphism by A1, TOPS_2:56; hence T,S are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum end; definition let S, T be TopStruct ; :: original: are_homeomorphic redefine predS,T are_homeomorphic ; reflexivity for S being TopStruct holds R36(b1,b1) by Lm1; end; definition let S, T be non empty TopStruct ; :: original: are_homeomorphic redefine predS,T are_homeomorphic ; reflexivity for S being non empty TopStruct holds R36(b1,b1) by Lm1; symmetry for S, T being non empty TopStruct st R36(b1,b2) holds R36(b2,b1) by Lm2; end; theorem :: BORSUK_3:3 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; ::_thesis: ( S,T are_homeomorphic & T,V are_homeomorphic implies S,V are_homeomorphic ) assume that A1: S,T are_homeomorphic and A2: T,V are_homeomorphic ; ::_thesis: S,V are_homeomorphic consider f being Function of S,T such that A3: f is being_homeomorphism by A1, T_0TOPSP:def_1; consider g being Function of T,V such that A4: g is being_homeomorphism by A2, T_0TOPSP:def_1; g * f is being_homeomorphism by A3, A4, TOPS_2:57; hence S,V are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum end; begin registration let T be TopStruct ; let P be empty Subset of T; clusterT | P -> empty ; coherence T | P is empty ; end; registration cluster empty TopSpace-like -> compact for TopStruct ; coherence for b1 being TopSpace st b1 is empty holds b1 is compact ; end; theorem Th4: :: BORSUK_3:4 for X, Y being non empty TopSpace for x being Point of X for 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; ::_thesis: for x being Point of X for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f is one-to-one let x be Point of X; ::_thesis: for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f is one-to-one let f be Function of [:Y,(X | {x}):],Y; ::_thesis: ( f = pr1 ( the carrier of Y,{x}) implies f is one-to-one ) set Z = {x}; assume A1: f = pr1 ( the carrier of Y,{x}) ; ::_thesis: f is one-to-one let z, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not z in dom f or not y in dom f or not f . z = f . y or z = y ) assume that A2: z in dom f and A3: y in dom f and A4: f . z = f . y ; ::_thesis: z = y A5: dom f = [: the carrier of Y,{x}:] by A1, FUNCT_3:def_4; then consider x1, x2 being set such that A6: x1 in the carrier of Y and A7: x2 in {x} and A8: z = [x1,x2] by A2, ZFMISC_1:def_2; consider y1, y2 being set such that A9: y1 in the carrier of Y and A10: y2 in {x} 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 z = y by A8, A11, A12; ::_thesis: verum end; theorem Th5: :: BORSUK_3:5 for X, Y being non empty TopSpace for x being Point of X for 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; ::_thesis: for x being Point of X for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f is one-to-one let x be Point of X; ::_thesis: for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f is one-to-one let f be Function of [:(X | {x}),Y:],Y; ::_thesis: ( f = pr2 ({x}, the carrier of Y) implies f is one-to-one ) set Z = {x}; assume A1: f = pr2 ({x}, the carrier of Y) ; ::_thesis: f is one-to-one let z, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not z in dom f or not y in dom f or not f . z = f . y or z = y ) assume that A2: z in dom f and A3: y in dom f and A4: f . z = f . y ; ::_thesis: z = y A5: dom f = [:{x}, the carrier of Y:] by A1, FUNCT_3:def_5; then consider x1, x2 being set such that A6: x1 in {x} and A7: x2 in the carrier of Y and A8: z = [x1,x2] by A2, ZFMISC_1:def_2; consider y1, y2 being set such that A9: y1 in {x} 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 z = y by A8, A11, A12; ::_thesis: verum end; theorem Th6: :: BORSUK_3:6 for X, Y being non empty TopSpace for x being Point of X for 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; ::_thesis: for x being Point of X for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f " = <:(id Y),(Y --> x):> let x be Point of X; ::_thesis: for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f " = <:(id Y),(Y --> x):> let f be Function of [:Y,(X | {x}):],Y; ::_thesis: ( f = pr1 ( the carrier of Y,{x}) implies f " = <:(id Y),(Y --> x):> ) set Z = {x}; set idZ = id Y; A1: rng (id Y) c= the carrier of Y ; assume A2: f = pr1 ( the carrier of Y,{x}) ; ::_thesis: f " = <:(id Y),(Y --> x):> then A3: rng f = the carrier of Y by FUNCT_3:44; reconsider Z = {x} as non empty Subset of X ; reconsider idY = Y --> x as continuous Function of Y,(X | Z) by Th2; reconsider KA = <:(id Y),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 set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [: the carrier of Y,Z:] or y in rng KA ) assume y in [: the carrier of Y,Z:] ; ::_thesis: y in rng KA then consider y1, y2 being set 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 = [((id Y) . y1),(idY . y1)] by FUNCT_3:def_7 .= [y1,x] by A5, A8, FUNCT_1:18 ; hence y in rng KA by A7, A9, FUNCT_1:def_3; ::_thesis: verum end; rng idY c= the carrier of (X | Z) ; then A10: rng idY c= Z by PRE_TOPC:8; then ( rng KA c= [:(rng (id Y)),(rng idY):] & [:(rng (id Y)),(rng idY):] c= [: the carrier of Y,Z:] ) by FUNCT_3:51, ZFMISC_1:96; then rng KA c= [: the carrier of Y,Z:] by XBOOLE_1:1; then A11: rng KA = [: the carrier of Y,Z:] by A4, XBOOLE_0:def_10 .= 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 (id Y) by FUNCT_2:def_1 ; then f * KA = id (rng f) by A2, A3, A10, A1, FUNCT_3:52; then KA = f " by A12, A11, FUNCT_1:42; hence f " = <:(id Y),(Y --> x):> by A12, A13, TOPS_2:def_4; ::_thesis: verum end; theorem Th7: :: BORSUK_3:7 for X, Y being non empty TopSpace for x being Point of X for 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; ::_thesis: for x being Point of X for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f " = <:(Y --> x),(id Y):> let x be Point of X; ::_thesis: for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f " = <:(Y --> x),(id Y):> let f be Function of [:(X | {x}),Y:],Y; ::_thesis: ( f = pr2 ({x}, the carrier of Y) implies f " = <:(Y --> x),(id Y):> ) set Z = {x}; set idY = id Y; A1: rng (id Y) c= the carrier of Y ; assume A2: f = pr2 ({x}, the carrier of Y) ; ::_thesis: f " = <:(Y --> x),(id Y):> then A3: rng f = the carrier of Y by FUNCT_3:46; reconsider Z = {x} 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; A4: [:{x}, the carrier of Y:] c= rng KA proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [:{x}, the carrier of Y:] or y in rng KA ) assume y in [:{x}, the carrier of Y:] ; ::_thesis: y in rng KA then consider y1, y2 being set 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),((id Y) . y2)] by FUNCT_3:def_7 .= [x,y2] by A6, A9, FUNCT_1:18 ; hence y in rng KA by A8, A10, FUNCT_1:def_3; ::_thesis: verum 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 (id Y)):] & [:(rng idZ),(rng (id Y)):] c= [:{x}, the carrier of Y:] ) by FUNCT_3:51, ZFMISC_1:96; then rng KA c= [:{x}, the carrier of Y:] by XBOOLE_1:1; then A12: rng KA = [:Z, the carrier of Y:] by A4, XBOOLE_0:def_10 .= 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 (id Y) by FUNCT_2:def_1 ; then f * KA = id (rng f) by A2, A3, A11, A1, FUNCT_3:52; then KA = f " by A13, A12, FUNCT_1:42; hence f " = <:(Y --> x),(id Y):> by A13, A14, TOPS_2:def_4; ::_thesis: verum end; theorem :: BORSUK_3:8 for X, Y being non empty TopSpace for x being Point of X for 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; ::_thesis: for x being Point of X for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f is being_homeomorphism let x be Point of X; ::_thesis: for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f is being_homeomorphism let f be Function of [:Y,(X | {x}):],Y; ::_thesis: ( f = pr1 ( the carrier of Y,{x}) implies f is being_homeomorphism ) set Z = {x}; assume A1: f = pr1 ( the carrier of Y,{x}) ; ::_thesis: f is being_homeomorphism thus dom f = [#] [:Y,(X | {x}):] by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] Y & f is one-to-one & f is continuous & f " is continuous ) thus rng f = [#] Y by A1, FUNCT_3:44; ::_thesis: ( f is one-to-one & f is continuous & f " is continuous ) thus f is one-to-one by A1, Th4; ::_thesis: ( f is continuous & f " is continuous ) the carrier of (X | {x}) = {x} by PRE_TOPC:8; hence f is continuous by A1, YELLOW12:39; ::_thesis: f " is continuous reconsider Z = {x} 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 f " is continuous ; ::_thesis: verum end; theorem Th9: :: BORSUK_3:9 for X, Y being non empty TopSpace for x being Point of X for 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; ::_thesis: for x being Point of X for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f is being_homeomorphism let x be Point of X; ::_thesis: for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f is being_homeomorphism let f be Function of [:(X | {x}),Y:],Y; ::_thesis: ( f = pr2 ({x}, the carrier of Y) implies f is being_homeomorphism ) set Z = {x}; assume A1: f = pr2 ({x}, the carrier of Y) ; ::_thesis: f is being_homeomorphism thus dom f = [#] [:(X | {x}),Y:] by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] Y & f is one-to-one & f is continuous & f " is continuous ) thus rng f = [#] Y by A1, FUNCT_3:46; ::_thesis: ( f is one-to-one & f is continuous & f " is continuous ) thus f is one-to-one by A1, Th5; ::_thesis: ( f is continuous & f " is continuous ) the carrier of (X | {x}) = {x} by PRE_TOPC:8; hence f is continuous by A1, YELLOW12:40; ::_thesis: f " is continuous reconsider Z = {x} 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 f " is continuous ; ::_thesis: verum end; begin theorem :: BORSUK_3:10 for X being non empty TopSpace for Y being non empty compact TopSpace for G being open Subset of [:X,Y:] for x being set st [:{x}, the carrier of Y:] c= G holds ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds ex G1 being Subset of X ex 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; ::_thesis: for Y being non empty compact TopSpace for G being open Subset of [:X,Y:] for x being set st [:{x}, the carrier of Y:] c= G holds ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds ex G1 being Subset of X ex 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 ) let Y be non empty compact TopSpace; ::_thesis: for G being open Subset of [:X,Y:] for x being set st [:{x}, the carrier of Y:] c= G holds ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds ex G1 being Subset of X ex 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 ) let G be open Subset of [:X,Y:]; ::_thesis: for x being set st [:{x}, the carrier of Y:] c= G holds ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds ex G1 being Subset of X ex 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 ) let x be set ; ::_thesis: ( [:{x}, the carrier of Y:] c= G implies ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds ex G1 being Subset of X ex 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 ) ) set y = the Point of Y; A1: ( the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] & [x, the Point of Y] in [:{x}, the carrier of Y:] ) by BORSUK_1:def_2, ZFMISC_1:105; defpred S1[ set , set ] means ex G1 being Subset of X ex H1 being 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 ; ::_thesis: ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds ex G1 being Subset of X ex 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 ) 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__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_Y_holds_ ex_G1_being_Subset_of_X_ex_H1_being_Subset_of_Y_st_ (_[x,y]_in_[:G1,H1:]_&_[:G1,H1:]_c=_G_&_G1_is_open_&_H1_is_open_) let y be set ; ::_thesis: ( y in the carrier of Y implies ex G1 being Subset of X ex H1 being Subset of Y st ( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) ) A5: x in {x9} by TARSKI:def_1; assume y in the carrier of Y ; ::_thesis: ex G1 being Subset of X ex H1 being Subset of Y st ( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) then [x,y] in [:{x9}, the carrier of Y:] by A5, ZFMISC_1:87; then consider Z being 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 being Subset of X ex Y1 being Subset of Y st ( Z = [:X1,Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open ) by A7; hence ex G1 being Subset of X ex H1 being Subset of Y st ( [x,y] in [:G1,H1:] & [:G1,H1:] c= G & G1 is open & H1 is open ) by A6; ::_thesis: verum end; A8: for i being set st i in the carrier of Y holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in the carrier of Y implies ex j being set st S1[i,j] ) assume i in the carrier of Y ; ::_thesis: ex j being set st S1[i,j] then consider G1 being Subset of X, H1 being 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 being Subset of X ex H2 being 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 ex j being set st S1[i,j] ; ::_thesis: verum end; ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds S1[i,f . i] from PBOOLE:sch_3(A8); hence ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds ex G1 being Subset of X ex 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 ) ; ::_thesis: verum end; theorem Th11: :: BORSUK_3:11 for X being non empty TopSpace for Y being non empty compact TopSpace for G being open Subset of [:Y,X:] for x being set st [:([#] Y),{x}:] c= G holds ex R being 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; ::_thesis: for Y being non empty compact TopSpace for G being open Subset of [:Y,X:] for x being set st [:([#] Y),{x}:] c= G holds ex R being open Subset of X st ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) let Y be non empty compact TopSpace; ::_thesis: for G being open Subset of [:Y,X:] for x being set st [:([#] Y),{x}:] c= G holds ex R being open Subset of X st ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) let G be open Subset of [:Y,X:]; ::_thesis: for x being set st [:([#] Y),{x}:] c= G holds ex R being open Subset of X st ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) let x be set ; ::_thesis: ( [:([#] Y),{x}:] c= G implies ex R being open Subset of X st ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) ) set y = the Point of Y; A1: ( the carrier of [:Y,X:] = [: the carrier of Y, the carrier of X:] & [ the Point of Y,x] in [: the carrier of Y,{x}:] ) by BORSUK_1:def_2, ZFMISC_1:106; assume A2: [:([#] Y),{x}:] c= G ; ::_thesis: ex R being open Subset of X st ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] 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; ::_thesis: ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) ( Int W c= W & [#] Y c= Int W ) by CONNSP_2:def_2, TOPS_1:16; then A4: [#] Y c= W by XBOOLE_1:1; 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not r in R or r in { z where z is Point of X : [:([#] Y),{z}:] c= G } ) assume A6: r in R ; ::_thesis: r in { z where z is Point of X : [:([#] Y),{z}:] c= G } 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, XBOOLE_1:1; hence r in { z where z is Point of X : [:([#] Y),{z}:] c= G } ; ::_thesis: verum end; hence ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) by CONNSP_2:def_1; ::_thesis: verum end; theorem Th12: :: BORSUK_3:12 for X being non empty TopSpace for Y being non empty compact TopSpace for 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; ::_thesis: for Y being non empty compact TopSpace for G being open Subset of [:Y,X:] holds { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X let Y be non empty compact TopSpace; ::_thesis: for G being open Subset of [:Y,X:] holds { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X let G be open Subset of [:Y,X:]; ::_thesis: { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X set Q = { x where x is Point of X : [:([#] Y),{x}:] c= G } ; { x where x is Point of X : [:([#] Y),{x}:] c= G } c= the carrier of X proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { x where x is Point of X : [:([#] Y),{x}:] c= G } or q in the carrier of X ) assume q in { x where x is Point of X : [:([#] Y),{x}:] c= G } ; ::_thesis: q in the carrier of X then ex x9 being Point of X st ( q = x9 & [:([#] Y),{x9}:] c= G ) ; hence q in the carrier of X ; ::_thesis: verum end; then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= G } as Subset of X ; defpred S1[ set ] means ex y being set st ( y in Q & ex S being Subset of X st ( S = \$1 & S is open & y in S & S c= Q ) ); consider RR being set such that A1: for x being set holds ( x in RR iff ( x in bool Q & S1[x] ) ) from XBOOLE_0:sch_1(); RR c= bool Q proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in RR or x in bool Q ) assume x in RR ; ::_thesis: x in bool Q hence x in bool Q by A1; ::_thesis: verum end; then reconsider RR = RR as Subset-Family of Q ; Q c= union RR proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Q or a in union RR ) assume a in Q ; ::_thesis: a in union RR then ex x9 being Point of X st ( a = x9 & [:([#] Y),{x9}:] c= G ) ; then consider R being 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 a in union RR by A2, TARSKI:def_4; ::_thesis: verum end; then A4: union RR = Q by XBOOLE_0:def_10; bool Q c= bool the carrier of X by ZFMISC_1:67; then reconsider RR = RR as Subset-Family of X by XBOOLE_1:1; RR c= the topology of X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in RR or x in the topology of X ) assume x in RR ; ::_thesis: x in the topology of X then ex y being set st ( y in Q & ex S being Subset of X st ( S = x & S is open & y in S & S c= Q ) ) by A1; hence x in the topology of X by PRE_TOPC:def_2; ::_thesis: verum end; hence { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X by A4, PRE_TOPC:def_1; ::_thesis: verum end; theorem Th13: :: BORSUK_3:13 for X, Y being non empty TopSpace for x being Point of X holds [:(X | {x}),Y:],Y are_homeomorphic proof let X, Y be non empty TopSpace; ::_thesis: for x being Point of X holds [:(X | {x}),Y:],Y are_homeomorphic let x be Point of X; ::_thesis: [:(X | {x}),Y:],Y are_homeomorphic set Z = {x}; the carrier of [:(X | {x}),Y:] = [: the carrier of (X | {x}), the carrier of Y:] by BORSUK_1:def_2 .= [:{x}, the carrier of Y:] by PRE_TOPC:8 ; then reconsider f = pr2 ({x}, the carrier of Y) as Function of [:(X | {x}),Y:],Y ; take f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism thus f is being_homeomorphism by Th9; ::_thesis: verum end; Lm3: for X, Y being non empty TopSpace for x being Point of X for Z being non empty Subset of X st Z = {x} holds [:Y,(X | Z):],Y are_homeomorphic proof let X, Y be non empty TopSpace; ::_thesis: for x being Point of X for Z being non empty Subset of X st Z = {x} holds [:Y,(X | Z):],Y are_homeomorphic let x be Point of X; ::_thesis: for Z being non empty Subset of X st Z = {x} holds [:Y,(X | Z):],Y are_homeomorphic let Z be non empty Subset of X; ::_thesis: ( Z = {x} implies [:Y,(X | Z):],Y are_homeomorphic ) [: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 by T_0TOPSP:def_1; assume Z = {x} ; ::_thesis: [:Y,(X | Z):],Y are_homeomorphic 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 by T_0TOPSP:def_1; reconsider gf = f * g as Function of [:Y,(X | Z):],Y ; gf is being_homeomorphism by A2, A1, TOPS_2:57; hence [:Y,(X | Z):],Y are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum end; theorem Th14: :: BORSUK_3:14 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; ::_thesis: ( S,T are_homeomorphic & S is compact implies T is compact ) assume that A1: S,T are_homeomorphic and A2: S is compact ; ::_thesis: T is compact consider f being Function of S,T such that A3: f is being_homeomorphism by A1, T_0TOPSP:def_1; ( f is continuous & rng f = [#] T ) by A3, TOPS_2:def_5; hence T is compact by A2, COMPTS_1:14; ::_thesis: verum end; theorem Th15: :: BORSUK_3:15 for X, Y being TopSpace for XV being SubSpace of X holds [:Y,XV:] is SubSpace of [:Y,X:] proof let X, Y be TopSpace; ::_thesis: for XV being SubSpace of X holds [:Y,XV:] is SubSpace of [:Y,X:] let XV be SubSpace of X; ::_thesis: [:Y,XV:] is SubSpace of [:Y,X:] set S = [:Y,XV:]; set 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, BORSUK_1:def_2; A3: for P being Subset of [:Y,XV:] holds ( P in the topology of [:Y,XV:] iff ex Q being Subset of [:Y,X:] st ( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) ) proof reconsider oS = [#] [:Y,XV:] as Subset of [:Y,X:] by A1, A2, ZFMISC_1:96; let P be Subset of [:Y,XV:]; ::_thesis: ( P in the topology of [:Y,XV:] iff ex Q being Subset of [:Y,X:] st ( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) ) reconsider P9 = P as Subset of [:Y,XV:] ; hereby ::_thesis: ( ex Q being Subset of [:Y,X:] st ( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) implies P in the topology of [:Y,XV:] ) assume P in the topology of [:Y,XV:] ; ::_thesis: ex Q being Subset of [:Y,X:] st ( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) then P9 is open by PRE_TOPC:def_2; then consider A being Subset-Family of [:Y,XV:] such that A4: P9 = union A and A5: for e being set st e in A holds ex X1 being Subset of Y ex 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 ) } ; { [: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 ) } c= bool the carrier of [:Y,X:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [: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 ) } or a in bool the carrier of [:Y,X:] ) assume a in { [: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 ) } ; ::_thesis: a in bool the carrier of [:Y,X:] then ex Xx1 being Subset of Y ex 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 a in bool the carrier of [:Y,X:] ; ::_thesis: verum end; then reconsider 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 ) } as Subset-Family of [:Y,X:] ; reconsider AA = AA as Subset-Family of [:Y,X:] ; A6: P c= (union AA) /\ ([#] [:Y,XV:]) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in P or p in (union AA) /\ ([#] [:Y,XV:]) ) assume p in P ; ::_thesis: p in (union AA) /\ ([#] [:Y,XV:]) then consider A1 being set such that A7: p in A1 and A8: A1 in A by A4, TARSKI:def_4; reconsider A1 = A1 as Subset of [:Y,XV:] 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 set 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 = Q1 as Subset of X ; set EX = [:X2,Q1:]; p2 in Q1 by A15, A13, XBOOLE_0:def_4; then A17: p in [:X2,Q1:] by A14, A16, ZFMISC_1:87; Q1 is open by A12, PRE_TOPC:def_2; then [:X2,Q1:] 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 p in (union AA) /\ ([#] [:Y,XV:]) by A7, A8, XBOOLE_0:def_4; ::_thesis: verum end; AA c= the topology of [:Y,X:] proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in AA or t in the topology of [:Y,X:] ) set A9 = {t}; assume t in AA ; ::_thesis: t in the topology of [:Y,X:] 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 ) ; {t} c= bool the carrier of [:Y,X:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {t} or a in bool the carrier of [:Y,X:] ) assume a in {t} ; ::_thesis: a in bool the carrier of [:Y,X:] then a = t by TARSKI:def_1; hence a in bool the carrier of [:Y,X:] by A18; ::_thesis: verum end; then reconsider A9 = {t} as Subset-Family of [:Y,X:] ; 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A9 or x in { [: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 ) } ) assume x in A9 ; ::_thesis: x in { [: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 ) } 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 x in { [: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 A21; ::_thesis: verum end; t = union A9 by ZFMISC_1:25; then t in { (union As) where As is Subset-Family of [:Y,X:] : 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 t in the topology of [:Y,X:] by BORSUK_1:def_2; ::_thesis: verum end; then A22: union AA in the topology of [:Y,X:] by PRE_TOPC:def_1; (union AA) /\ ([#] [:Y,XV:]) c= P proof let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in (union AA) /\ ([#] [:Y,XV:]) or h in P ) assume A23: h in (union AA) /\ ([#] [:Y,XV:]) ; ::_thesis: h in P 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 set 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 h in P by A4, A29, TARSKI:def_4; ::_thesis: verum end; then P = (union AA) /\ ([#] [:Y,XV:]) by A6, XBOOLE_0:def_10; hence ex Q being Subset of [:Y,X:] st ( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) by A22; ::_thesis: verum end; given Q being Subset of [:Y,X:] such that A33: Q in the topology of [:Y,X:] and A34: P = Q /\ ([#] [:Y,XV:]) ; ::_thesis: P in the topology of [:Y,XV:] reconsider Q9 = Q as Subset of [:Y,X:] ; Q9 is open by A33, PRE_TOPC:def_2; then consider A being Subset-Family of [:Y,X:] such that A35: Q9 = union A and A36: for e being set st e in A holds ex X1 being Subset of Y ex Y1 being Subset of X st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5; reconsider A = A as Subset-Family of [:Y,X:] ; reconsider AA = A | oS as Subset-Family of ([:Y,X:] | oS) ; reconsider AA = AA as Subset-Family of [:Y,XV:] by PRE_TOPC:8; reconsider AA = AA as Subset-Family of [:Y,XV:] ; A37: for e being set st e in AA holds ex X1 being Subset of Y ex Y1 being Subset of XV st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) proof let e be set ; ::_thesis: ( e in AA implies ex X1 being Subset of Y ex Y1 being Subset of XV st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) assume A38: e in AA ; ::_thesis: ex X1 being Subset of Y ex Y1 being Subset of XV st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) then reconsider e9 = e as Subset of ([:Y,X:] | oS) ; consider R being Subset of [:Y,X:] 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 ex X1 being Subset of Y ex Y1 being Subset of XV st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A42, A44; ::_thesis: verum end; A45: (union A) /\ oS c= union AA proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in (union A) /\ oS or s in union AA ) assume A46: s in (union A) /\ oS ; ::_thesis: s in union AA 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 = A1 as Subset of [:Y,X:] by A48; A1 /\ oS in AA by A48, TOPS_2:31; hence s in union AA by A49, TARSKI:def_4; ::_thesis: verum 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, XBOOLE_0:def_10; then P9 is open by A37, BORSUK_1:5; hence P in the topology of [:Y,XV:] by PRE_TOPC:def_2; ::_thesis: verum end; [#] [:Y,XV:] c= [#] [:Y,X:] by A1, A2, ZFMISC_1:96; hence [:Y,XV:] is SubSpace of [:Y,X:] by A3, PRE_TOPC:def_4; ::_thesis: verum end; Lm4: for X, Y being TopSpace for Z being Subset of [:Y,X:] for V being Subset of X st Z = [:([#] Y),V:] holds TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) proof let X, Y be TopSpace; ::_thesis: for Z being Subset of [:Y,X:] for V being Subset of X st Z = [:([#] Y),V:] holds TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) let Z be Subset of [:Y,X:]; ::_thesis: for V being Subset of X st Z = [:([#] Y),V:] holds TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) let V be Subset of X; ::_thesis: ( Z = [:([#] Y),V:] implies TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) ) reconsider A = [:Y,(X | V):] as SubSpace of [:Y,X:] by Th15; assume A1: Z = [:([#] Y),V:] ; ::_thesis: TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) 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 TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) by TSEP_1:6; ::_thesis: verum end; theorem Th16: :: BORSUK_3:16 for X being non empty TopSpace for Y being non empty compact TopSpace for x being Point of X for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds Z is compact proof let X be non empty TopSpace; ::_thesis: for Y being non empty compact TopSpace for x being Point of X for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds Z is compact let Y be non empty compact TopSpace; ::_thesis: for x being Point of X for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds Z is compact let x be Point of X; ::_thesis: for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds Z is compact let Z be Subset of [:Y,X:]; ::_thesis: ( Z = [:([#] Y),{x}:] implies Z is compact ) 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}:] ; ::_thesis: Z is compact then TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) by Lm4; hence Z is compact by A2, A1, COMPTS_1:3; ::_thesis: verum end; registration let X be non empty TopSpace; let Y be non empty compact TopSpace; let x be Point of X; cluster[:Y,(X | {x}):] -> compact ; coherence [:Y,(X | {x}):] is compact proof Y,[:Y,(X | {x}):] are_homeomorphic by Lm3; hence [:Y,(X | {x}):] is compact by Th14; ::_thesis: verum end; end; theorem :: BORSUK_3:17 for X, Y being non empty compact TopSpace for 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 non empty compact TopSpace; ::_thesis: for 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 ) let R be Subset-Family of X; ::_thesis: ( R = { Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:])) } implies ( R is open & R is Cover of [#] X ) ) assume A1: R = { Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:])) } ; ::_thesis: ( R is open & R is Cover of [#] X ) now__::_thesis:_for_P_being_Subset_of_X_st_P_in_R_holds_ P_is_open let P be Subset of X; ::_thesis: ( P in R implies P is open ) assume P in R ; ::_thesis: P is open 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 ; ::_thesis: verum end; hence R is open by TOPS_2:def_1; ::_thesis: R is Cover of [#] X [#] X c= union R proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in [#] X or k in union R ) assume k in [#] X ; ::_thesis: k in union R 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, COMPTS_1:def_4; set uR = union G; set Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } ; { x where x is Point of X : [:([#] Y),{x}:] c= union G } c= the carrier of X proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { x where x is Point of X : [:([#] Y),{x}:] c= union G } or k in the carrier of X ) assume k in { x where x is Point of X : [:([#] Y),{x}:] c= union G } ; ::_thesis: k in the carrier of X then ex x1 being Point of X st ( k = x1 & [:([#] Y),{x1}:] c= union G ) ; hence k in the carrier of X ; ::_thesis: verum end; then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:([#] Y),Q:] or z in union (Base-Appr ([#] [:Y,X:])) ) assume z in [:([#] Y),Q:] ; ::_thesis: z in union (Base-Appr ([#] [:Y,X:])) then consider x1, x2 being set 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= union G by A8; x2 in {x29} by A10, TARSKI:def_1; then A12: z in [:([#] Y),{x29}:] by A7, A9, ZFMISC_1:87; union G c= union (Base-Appr ([#] [:Y,X:])) by A3, ZFMISC_1:77; then [:([#] Y),{x29}:] c= union (Base-Appr ([#] [:Y,X:])) by A11, XBOOLE_1:1; hence z in union (Base-Appr ([#] [:Y,X:])) by A12; ::_thesis: verum end; union G is open by A3, TOPS_2:11, TOPS_2: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 k in union R by A5, TARSKI:def_4; ::_thesis: verum end; hence R is Cover of [#] X by SETFAM_1:def_11; ::_thesis: verum end; theorem Th18: :: BORSUK_3:18 for X, Y being non empty compact TopSpace for R being Subset-Family of X for 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 non empty compact TopSpace; ::_thesis: for R being Subset-Family of X for 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 ) let R be Subset-Family of X; ::_thesis: for 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 ) let F be Subset-Family of [:Y,X:]; ::_thesis: ( 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 ) } implies ( R is open & R is Cover of 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 ) } ; ::_thesis: ( R is open & R is Cover of X ) now__::_thesis:_for_P_being_Subset_of_X_st_P_in_R_holds_ P_is_open let P be Subset of X; ::_thesis: ( P in R implies P is open ) assume P in R ; ::_thesis: P is open 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 ; ::_thesis: verum end; hence R is open by TOPS_2:def_1; ::_thesis: R is Cover of X A4: union F = [#] [:Y,X:] by A1, SETFAM_1:45; [#] X c= union R proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in [#] X or k in union R ) assume k in [#] X ; ::_thesis: k in union R 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, COMPTS_1:def_4; set uR = union G; set Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } ; { x where x is Point of X : [:([#] Y),{x}:] c= union G } c= the carrier of X proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { x where x is Point of X : [:([#] Y),{x}:] c= union G } or k in the carrier of X ) assume k in { x where x is Point of X : [:([#] Y),{x}:] c= union G } ; ::_thesis: k in the carrier of X then ex x1 being Point of X st ( k = x1 & [:([#] Y),{x1}:] c= union G ) ; hence k in the carrier of X ; ::_thesis: verum end; then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } 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 ; ::_thesis: ( G c= F & G is finite & [:([#] Y),Q:] c= union G ) [:([#] Y),Q:] c= union G proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:([#] Y),Q:] or z in union G ) assume z in [:([#] Y),Q:] ; ::_thesis: z in union G then consider x1, x2 being set 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= union G by A11; x2 in {x29} by A13, TARSKI:def_1; then z in [:([#] Y),{x29}:] by A10, A12, ZFMISC_1:87; hence z in union G by A14; ::_thesis: verum end; hence ( G c= F & G is finite & [:([#] Y),Q:] c= union G ) by A5, A7; ::_thesis: verum end; union G is open by A2, A5, TOPS_2:11, TOPS_2: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 k in union R by A8, TARSKI:def_4; ::_thesis: verum end; hence R is Cover of X by SETFAM_1:def_11; ::_thesis: verum end; theorem Th19: :: BORSUK_3:19 for X, Y being non empty compact TopSpace for R being Subset-Family of X for 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 non empty compact TopSpace; ::_thesis: for R being Subset-Family of X for 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 ) let R be Subset-Family of X; ::_thesis: for 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 ) let F be Subset-Family of [:Y,X:]; ::_thesis: ( 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 ) } implies ex C being Subset-Family of X st ( C c= R & C is finite & C is Cover of 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 ) } ) ; ::_thesis: ex C being Subset-Family of X st ( C c= R & C is finite & C is Cover of X ) 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 ex C being Subset-Family of X st ( C c= R & C is finite & C is Cover of X ) ; ::_thesis: verum end; theorem Th20: :: BORSUK_3:20 for X, Y being non empty compact TopSpace for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open holds 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 non empty compact TopSpace; ::_thesis: for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open holds ex G being Subset-Family of [:Y,X:] st ( G c= F & G is Cover of [:Y,X:] & G is finite ) let F be Subset-Family of [:Y,X:]; ::_thesis: ( F is Cover of [:Y,X:] & F is open implies ex G being Subset-Family of [:Y,X:] st ( G c= F & G is Cover of [:Y,X:] & G is finite ) ) 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 ) } ; { 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 ) } c= bool the carrier of X proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s 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 ) } or s in bool the carrier of X ) assume s 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 ) } ; ::_thesis: s in bool the carrier of X 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 s in bool the carrier of X ; ::_thesis: verum end; then reconsider 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 ) } as Subset-Family of X ; reconsider R = R as Subset-Family of X ; defpred S1[ set , set ] means ex FQ being Subset-Family of [:Y,X:] st ( FQ c= F & FQ is finite & [:([#] Y),\$1:] c= union FQ & \$2 = FQ ); deffunc H1( set ) -> set = [:([#] Y),\$1:]; assume ( F is Cover of [:Y,X:] & F is open ) ; ::_thesis: ex G being Subset-Family of [:Y,X:] st ( G c= F & G is Cover of [:Y,X:] & G is finite ) 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 = { H1(f) where f is Subset of X : f in C } ; { H1(f) where f is Subset of X : f in C } c= bool the carrier of [:Y,X:] proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { H1(f) where f is Subset of X : f in C } or s in bool the carrier of [:Y,X:] ) assume s in { H1(f) where f is Subset of X : f in C } ; ::_thesis: s in bool the carrier of [:Y,X:] then consider f1 being Subset of X such that A4: s = H1(f1) and f1 in C ; [:([#] Y),f1:] c= the carrier of [:Y,X:] ; hence s in bool the carrier of [:Y,X:] by A4; ::_thesis: verum end; then reconsider CX = { H1(f) where f is Subset of X : f in C } as Subset-Family of [:Y,X:] ; reconsider CX = CX as Subset-Family of [:Y,X:] ; A5: for e being set st e in C holds ex u being set st S1[e,u] proof let e be set ; ::_thesis: ( e in C implies ex u being set st S1[e,u] ) assume e in C ; ::_thesis: ex u being set st S1[e,u] 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 ex u being set st S1[e,u] ; ::_thesis: verum end; consider t being Function such that A6: ( dom t = C & ( for s being set st s in C holds S1[s,t . s] ) ) from CLASSES1:sch_1(A5); set G = union (rng t); A7: union (rng t) c= F proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in union (rng t) or k in F ) assume k in union (rng t) ; ::_thesis: k in F then consider K being set such that A8: k in K and A9: K in rng t by TARSKI:def_4; consider x1 being set such that A10: ( x1 in dom t & K = t . x1 ) by A9, FUNCT_1:def_3; ex FQ being Subset-Family of [:Y,X:] st ( FQ c= F & FQ is finite & [:([#] Y),x1:] c= union FQ & K = FQ ) by A6, A10; hence k in F by A8; ::_thesis: verum end; union (rng t) c= bool the carrier of [:Y,X:] proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in union (rng t) or s in bool the carrier of [:Y,X:] ) assume s in union (rng t) ; ::_thesis: s in bool the carrier of [:Y,X:] then s in F by A7; hence s in bool the carrier of [:Y,X:] ; ::_thesis: verum end; then reconsider G = union (rng t) as Subset-Family of [:Y,X:] ; reconsider G = G as Subset-Family of [:Y,X:] ; take G ; ::_thesis: ( G c= F & G is Cover of [:Y,X:] & G is finite ) thus G c= F by A7; ::_thesis: ( G is Cover of [:Y,X:] & G is finite ) union CX = [:([#] Y),(union C):] proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [:([#] Y),(union C):] c= union CX let g be set ; ::_thesis: ( g in union CX implies g in [:([#] Y),(union C):] ) assume g in union CX ; ::_thesis: g in [:([#] Y),(union C):] 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 being set 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; ::_thesis: verum end; let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in [:([#] Y),(union C):] or g in union CX ) assume g in [:([#] Y),(union C):] ; ::_thesis: g in union CX then consider g1, g2 being set 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 g in union CX by A24, TARSKI:def_4; ::_thesis: verum 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not d in [#] [:Y,X:] or d in union (union (rng t)) ) assume d in [#] [:Y,X:] ; ::_thesis: d in union (union (rng t)) 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 ) ; 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 A6, A29, 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 d in union (union (rng t)) by A33, TARSKI:def_4; ::_thesis: verum end; hence G is Cover of [:Y,X:] by SETFAM_1:def_11; ::_thesis: G is finite A35: for X1 being set st X1 in rng t holds X1 is finite proof let X1 be set ; ::_thesis: ( X1 in rng t implies X1 is finite ) assume X1 in rng t ; ::_thesis: X1 is finite then consider x1 being set such that A36: x1 in dom t and A37: X1 = t . x1 by FUNCT_1:def_3; ex FQ being Subset-Family of [:Y,X:] st ( FQ c= F & FQ is finite & [:([#] Y),x1:] c= union FQ & t . x1 = FQ ) by A6, A36; hence X1 is finite by A37; ::_thesis: verum end; rng t is finite by A2, A6, FINSET_1:8; hence G is finite by A35, FINSET_1:7; ::_thesis: verum end; Lm5: for T1, T2 being non empty compact TopSpace holds [:T1,T2:] is compact proof let T1, T2 be non empty compact TopSpace; ::_thesis: [:T1,T2:] is compact set T = [:T1,T2:]; let F be Subset-Family of [:T1,T2:]; :: according to COMPTS_1:def_1 ::_thesis: ( not F is Cover of the carrier of [:T1,T2:] or not F is open or ex b1 being Element of bool (bool the carrier of [:T1,T2:]) st ( b1 c= F & b1 is Cover of the carrier of [:T1,T2:] & b1 is finite ) ) assume ( F is Cover of [:T1,T2:] & F is open ) ; ::_thesis: ex b1 being Element of bool (bool the carrier of [:T1,T2:]) st ( b1 c= F & b1 is Cover of the carrier of [:T1,T2:] & b1 is finite ) hence ex b1 being Element of bool (bool the carrier of [:T1,T2:]) st ( b1 c= F & b1 is Cover of the carrier of [:T1,T2:] & b1 is finite ) by Th20; ::_thesis: verum end; registration let T1, T2 be compact TopSpace; cluster[:T1,T2:] -> compact ; coherence [:T1,T2:] is compact proof percases ( ( not T1 is empty & not T2 is empty ) or ( T1 is empty & T2 is empty ) or ( T1 is empty & not T2 is empty ) or ( not T1 is empty & T2 is empty ) ) ; suppose ( not T1 is empty & not T2 is empty ) ; ::_thesis: [:T1,T2:] is compact hence [:T1,T2:] is compact by Lm5; ::_thesis: verum end; suppose ( T1 is empty & T2 is empty ) ; ::_thesis: [:T1,T2:] is compact hence [:T1,T2:] is compact ; ::_thesis: verum end; suppose ( T1 is empty & not T2 is empty ) ; ::_thesis: [:T1,T2:] is compact hence [:T1,T2:] is compact ; ::_thesis: verum end; suppose ( not T1 is empty & T2 is empty ) ; ::_thesis: [:T1,T2:] is compact hence [:T1,T2:] is compact ; ::_thesis: verum end; end; end; end; Lm6: for X, Y being TopSpace for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:] proof let X, Y be TopSpace; ::_thesis: for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:] let XV be SubSpace of X; ::_thesis: [:XV,Y:] is SubSpace of [:X,Y:] set S = [:XV,Y:]; set T = [:X,Y:]; A1: the carrier of [:XV,Y:] = [: 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, BORSUK_1:def_2; A3: for P being Subset of [:XV,Y:] holds ( P in the topology of [:XV,Y:] iff ex Q being Subset of [:X,Y:] st ( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) ) proof reconsider oS = [#] [:XV,Y:] as Subset of [:X,Y:] by A1, A2, ZFMISC_1:96; let P be Subset of [:XV,Y:]; ::_thesis: ( P in the topology of [:XV,Y:] iff ex Q being Subset of [:X,Y:] st ( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) ) reconsider P9 = P as Subset of [:XV,Y:] ; hereby ::_thesis: ( ex Q being Subset of [:X,Y:] st ( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) implies P in the topology of [:XV,Y:] ) assume P in the topology of [:XV,Y:] ; ::_thesis: ex Q being Subset of [:X,Y:] st ( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) then P9 is open by PRE_TOPC:def_2; then consider A being Subset-Family of [:XV,Y:] such that A4: P9 = union A and A5: for e being set st e in A holds ex X1 being Subset of XV ex 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 ) } ; { [: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 ) } c= bool the carrier of [:X,Y:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [: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 ) } or a in bool the carrier of [:X,Y:] ) assume a in { [: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 ) } ; ::_thesis: a in bool the carrier of [:X,Y:] then ex Xx1 being Subset of X ex 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 a in bool the carrier of [:X,Y:] ; ::_thesis: verum end; then reconsider 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 ) } as Subset-Family of [:X,Y:] ; reconsider AA = AA as Subset-Family of [:X,Y:] ; A6: P c= (union AA) /\ ([#] [:XV,Y:]) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in P or p in (union AA) /\ ([#] [:XV,Y:]) ) assume p in P ; ::_thesis: p in (union AA) /\ ([#] [:XV,Y:]) then consider A1 being set such that A7: p in A1 and A8: A1 in A by A4, TARSKI:def_4; reconsider A1 = A1 as Subset of [:XV,Y:] 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 set such that A14: p1 in X2 and A15: ( p2 in Y2 & p = [p1,p2] ) by A7, A9, ZFMISC_1:def_2; reconsider Q1 = Q1 as Subset of X ; set EX = [:Q1,Y2:]; p1 in Q1 by A14, A13, XBOOLE_0:def_4; then A16: p in [:Q1,Y2:] by A15, ZFMISC_1:87; Q1 is open by A12, PRE_TOPC:def_2; then [:Q1,Y2:] 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 p in (union AA) /\ ([#] [:XV,Y:]) by A7, A8, XBOOLE_0:def_4; ::_thesis: verum end; AA c= the topology of [:X,Y:] proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in AA or t in the topology of [:X,Y:] ) set A9 = {t}; assume t in AA ; ::_thesis: t in the topology of [:X,Y:] 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 ) ; {t} c= bool the carrier of [:X,Y:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {t} or a in bool the carrier of [:X,Y:] ) assume a in {t} ; ::_thesis: a in bool the carrier of [:X,Y:] then a = t by TARSKI:def_1; hence a in bool the carrier of [:X,Y:] by A17; ::_thesis: verum end; then reconsider A9 = {t} as Subset-Family of [:X,Y:] ; 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A9 or x in { [: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 ) } ) assume x in A9 ; ::_thesis: x in { [: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 ) } 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 x in { [: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 A20; ::_thesis: verum end; t = union A9 by ZFMISC_1:25; then t in { (union As) where As is Subset-Family of [:X,Y:] : 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 t in the topology of [:X,Y:] by BORSUK_1:def_2; ::_thesis: verum end; then A21: union AA in the topology of [:X,Y:] by PRE_TOPC:def_1; (union AA) /\ ([#] [:XV,Y:]) c= P proof let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in (union AA) /\ ([#] [:XV,Y:]) or h in P ) assume A22: h in (union AA) /\ ([#] [:XV,Y:]) ; ::_thesis: h in P 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 set 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 h in P by A4, A28, TARSKI:def_4; ::_thesis: verum end; then P = (union AA) /\ ([#] [:XV,Y:]) by A6, XBOOLE_0:def_10; hence ex Q being Subset of [:X,Y:] st ( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) by A21; ::_thesis: verum end; given Q being Subset of [:X,Y:] such that A32: Q in the topology of [:X,Y:] and A33: P = Q /\ ([#] [:XV,Y:]) ; ::_thesis: P in the topology of [:XV,Y:] reconsider Q9 = Q as Subset of [:X,Y:] ; Q9 is open by A32, PRE_TOPC:def_2; then consider A being Subset-Family of [:X,Y:] such that A34: Q9 = union A and A35: for e being set st e in A holds ex X1 being Subset of X ex Y1 being Subset of Y st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5; reconsider A = A as Subset-Family of [:X,Y:] ; reconsider AA = A | oS as Subset-Family of ([:X,Y:] | oS) ; reconsider AA = AA as Subset-Family of [:XV,Y:] by PRE_TOPC:8; reconsider AA = AA as Subset-Family of [:XV,Y:] ; A36: for e being set st e in AA holds ex X1 being Subset of XV ex Y1 being Subset of Y st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) proof let e be set ; ::_thesis: ( e in AA implies ex X1 being Subset of XV ex Y1 being Subset of Y st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) assume A37: e in AA ; ::_thesis: ex X1 being Subset of XV ex Y1 being Subset of Y st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) then reconsider e9 = e as Subset of ([:X,Y:] | oS) ; consider R being Subset of [:X,Y:] 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 ex X1 being Subset of XV ex Y1 being Subset of Y st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A42, A43; ::_thesis: verum end; A44: (union A) /\ oS c= union AA proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in (union A) /\ oS or s in union AA ) assume A45: s in (union A) /\ oS ; ::_thesis: s in union AA 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 = A1 as Subset of [:X,Y:] by A47; A1 /\ oS in AA by A47, TOPS_2:31; hence s in union AA by A48, TARSKI:def_4; ::_thesis: verum 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, XBOOLE_0:def_10; then P9 is open by A36, BORSUK_1:5; hence P in the topology of [:XV,Y:] by PRE_TOPC:def_2; ::_thesis: verum end; [#] [:XV,Y:] c= [#] [:X,Y:] by A1, A2, ZFMISC_1:96; hence [:XV,Y:] is SubSpace of [:X,Y:] by A3, PRE_TOPC:def_4; ::_thesis: verum end; theorem Th21: :: BORSUK_3:21 for X, Y being TopSpace for XV being SubSpace of X for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:] proof let X, Y be TopSpace; ::_thesis: for XV being SubSpace of X for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:] let XV be SubSpace of X; ::_thesis: for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:] let YV be SubSpace of Y; ::_thesis: [:XV,YV:] is SubSpace of [:X,Y:] ( [:XV,Y:] is SubSpace of [:X,Y:] & [:XV,YV:] is SubSpace of [:XV,Y:] ) by Lm6, Th15; hence [:XV,YV:] is SubSpace of [:X,Y:] by TSEP_1:7; ::_thesis: verum end; theorem Th22: :: BORSUK_3:22 for X, Y being TopSpace for Z being Subset of [:Y,X:] for V being Subset of X for W being Subset of Y st Z = [:W,V:] holds TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) proof let X, Y be TopSpace; ::_thesis: for Z being Subset of [:Y,X:] for V being Subset of X for W being Subset of Y st Z = [:W,V:] holds TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) let Z be Subset of [:Y,X:]; ::_thesis: for V being Subset of X for W being Subset of Y st Z = [:W,V:] holds TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) let V be Subset of X; ::_thesis: for W being Subset of Y st Z = [:W,V:] holds TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) let W be Subset of Y; ::_thesis: ( Z = [:W,V:] implies TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) ) reconsider A = [:(Y | W),(X | V):] as SubSpace of [:Y,X:] by Th21; assume A1: Z = [:W,V:] ; ::_thesis: TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) 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 TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) by TSEP_1:6; ::_thesis: verum end; registration let T be TopSpace; cluster empty for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is empty proof take {} T ; ::_thesis: {} T is empty thus {} T is empty ; ::_thesis: verum end; end; registration let T be TopSpace; let P be compact Subset of T; clusterT | P -> compact ; coherence T | P is compact proof percases ( not P is empty or P is empty ) ; suppose not P is empty ; ::_thesis: T | P is compact hence T | P is compact by COMPTS_1:3; ::_thesis: verum end; suppose P is empty ; ::_thesis: T | P is compact hence T | P is compact ; ::_thesis: verum end; end; end; end; theorem :: BORSUK_3:23 for T1, T2 being TopSpace for S1 being Subset of T1 for 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; ::_thesis: for S1 being Subset of T1 for S2 being Subset of T2 st S1 is compact & S2 is compact holds [:S1,S2:] is compact Subset of [:T1,T2:] let S1 be Subset of T1; ::_thesis: for S2 being Subset of T2 st S1 is compact & S2 is compact holds [:S1,S2:] is compact Subset of [:T1,T2:] let S2 be Subset of T2; ::_thesis: ( S1 is compact & S2 is compact implies [:S1,S2:] is compact Subset of [:T1,T2:] ) assume that A1: S1 is compact and A2: S2 is compact ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:] percases ( ( not S1 is empty & not S2 is empty ) or ( S1 is empty & not S2 is empty ) or ( not S1 is empty & S2 is empty ) or ( S1 is empty & S2 is empty ) ) ; supposeA3: ( not S1 is empty & not S2 is empty ) ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:] then ( ex x being set st x in S1 & ex y being set st y in S2 ) by XBOOLE_0:def_1; then reconsider T1 = T1, T2 = T2 as non empty TopSpace ; reconsider S2 = S2 as non empty compact Subset of T2 by A2, A3; reconsider S1 = S1 as non empty compact Subset of T1 by A1, A3; reconsider X = [:S1,S2:] as Subset of [:T1,T2:] ; TopStruct(# the carrier of [:(T1 | S1),(T2 | S2):], the topology of [:(T1 | S1),(T2 | S2):] #) = TopStruct(# the carrier of ([:T1,T2:] | X), the topology of ([:T1,T2:] | X) #) by Th22; hence [:S1,S2:] is compact Subset of [:T1,T2:] by COMPTS_1:3; ::_thesis: verum end; suppose ( S1 is empty & not S2 is empty ) ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:] then reconsider S1 = S1 as empty Subset of T1 ; [:S1,S2:] = {} [:T1,T2:] ; hence [:S1,S2:] is compact Subset of [:T1,T2:] ; ::_thesis: verum end; suppose ( not S1 is empty & S2 is empty ) ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:] then reconsider S2 = S2 as empty Subset of T2 ; [:S1,S2:] = {} [:T1,T2:] ; hence [:S1,S2:] is compact Subset of [:T1,T2:] ; ::_thesis: verum end; suppose ( S1 is empty & S2 is empty ) ; ::_thesis: [:S1,S2:] is compact Subset of [:T1,T2:] then reconsider S2 = S2 as empty Subset of T2 ; [:S1,S2:] = {} [:T1,T2:] ; hence [:S1,S2:] is compact Subset of [:T1,T2:] ; ::_thesis: verum end; end; end;