:: by Adam Grabowski

::

:: Received February 13, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: BORSUK_3:1

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})

for x being Point of X holds Y --> x is continuous Function of Y,(X | {x})

proof end;

Lm1: for S being TopStruct holds S,S are_homeomorphic

proof end;

Lm2: for S, T being non empty TopStruct st S,T are_homeomorphic holds

T,S are_homeomorphic

proof end;

definition

let S, T be TopStruct ;

:: original: are_homeomorphic

redefine pred S,T are_homeomorphic ;

reflexivity

for S being TopStruct holds R37(b_{1},b_{1})
by Lm1;

end;
:: original: are_homeomorphic

redefine pred S,T are_homeomorphic ;

reflexivity

for S being TopStruct holds R37(b

definition

let S, T be non empty TopStruct ;

:: original: are_homeomorphic

redefine pred S,T are_homeomorphic ;

reflexivity

for S being non empty TopStruct holds R37(b_{1},b_{1})
by Lm1;

symmetry

for S, T being non empty TopStruct st R37(b_{1},b_{2}) holds

R37(b_{2},b_{1})
by Lm2;

end;
:: original: are_homeomorphic

redefine pred S,T are_homeomorphic ;

reflexivity

for S being non empty TopStruct holds R37(b

symmetry

for S, T being non empty TopStruct st R37(b

R37(b

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

S,V are_homeomorphic

proof end;

registration
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

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 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

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 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):>

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 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):>

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 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

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 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

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 end;

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 object 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 )

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 object 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 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 } )

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 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

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 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 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 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

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 end;

registration

let X be non empty TopSpace;

let Y be non empty compact TopSpace;

let x be Point of X;

coherence

[:Y,(X | {x}):] is compact

end;
let Y be non empty compact TopSpace;

let x be Point of X;

coherence

[:Y,(X | {x}):] is compact

proof 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 )

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 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 )

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 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 )

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 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 )

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 end;

Lm5: for T1, T2 being non empty compact TopSpace holds [:T1,T2:] is compact

by Th20;

Lm6: for X, Y being TopSpace

for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:]

proof 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:]

for XV being SubSpace of X

for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:]

proof 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) #)

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 end;

registration
end;

registration
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:]

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 end;