:: A Borsuk Theorem on Homotopy Types
:: by Andrzej Trybulec
::
:: Received August 1, 1991
:: Copyright (c) 1991 Association of Mizar Users

:: BORSUK_1 semantic presentation

theorem :: BORSUK_1:1
canceled;

theorem :: BORSUK_1:2
canceled;

theorem :: BORSUK_1:3
canceled;

theorem :: BORSUK_1:4
canceled;

theorem Th5: :: BORSUK_1:5
for X, X1 being set
for F being Function st X c= F " X1 holds
F .: X c= X1
proof end;

theorem :: BORSUK_1:6
for X, u, X1 being set holds (X --> u) .: X1 c= {u} ;

theorem :: BORSUK_1:7
canceled;

theorem :: BORSUK_1:8
canceled;

theorem Th9: :: BORSUK_1:9
for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr1 X,Y)) . e = (pr1 X,Y) .: e
proof end;

theorem Th10: :: BORSUK_1:10
for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr2 X,Y)) . e = (pr2 X,Y) .: e
proof end;

theorem :: BORSUK_1:11
canceled;

theorem Th12: :: BORSUK_1:12
for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 X,Y) .: [:X1,Y1:] = X1 & (pr2 X,Y) .: [:X1,Y1:] = Y1 )
proof end;

theorem Th13: :: BORSUK_1:13
for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 X,Y)) . [:X1,Y1:] = X1 & (.: (pr2 X,Y)) . [:X1,Y1:] = Y1 )
proof end;

theorem Th14: :: BORSUK_1:14
for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 X,Y)) .: H)),(meet ((.: (pr2 X,Y)) .: H)):] c= A
proof end;

theorem :: BORSUK_1:15
for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 X,Y)) .: H)),(union ((.: (pr2 X,Y)) .: H)):] c= A
proof end;

theorem Th16: :: BORSUK_1:16
for X being set
for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
proof end;

theorem Th17: :: BORSUK_1:17
for X being set
for a being Subset-Family of X holds union (union a) = union { (union A) where A is Subset of X : A in a }
proof end;

theorem Th18: :: BORSUK_1:18
for X being set
for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A ` )
proof end;

theorem Th19: :: BORSUK_1:19
for X, Y, Z being non empty set
for F being Function of X,Y
for G being Function of X,Z st ( for x, x' being Element of X st F . x = F . x' holds
G . x = G . x' ) holds
ex H being Function of Y,Z st H * F = G
proof end;

theorem Th20: :: BORSUK_1:20
for X, Y, Z being non empty set
for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
proof end;

theorem Th21: :: BORSUK_1:21
for X, Y, Z being non empty set
for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . x,z = [(F . x),z]
proof end;

theorem :: BORSUK_1:22
canceled;

theorem Th23: :: BORSUK_1:23
for X, Y, Z being non empty set
for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
proof end;

theorem Th24: :: BORSUK_1:24
for X, Y, Z being non empty set
for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
proof end;

theorem Th25: :: BORSUK_1:25
for X being non empty set
for D being Subset-Family of X
for A being Subset of D holds union A is Subset of X
proof end;

theorem Th26: :: BORSUK_1:26
for X being set
for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
proof end;

theorem Th27: :: BORSUK_1:27
for X being non empty set
for D being a_partition of X
for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A ` )
proof end;

theorem :: BORSUK_1:28
for X being non empty set
for E being Equivalence_Relation of X holds not Class E is empty ;

registration
let X be non empty set ;
cluster non empty a_partition of X;
existence
not for b1 being a_partition of X holds b1 is empty
proof end;
end;

definition
let X be non empty set ;
let D be non empty a_partition of X;
func proj D -> Function of X,D means :Def1: :: BORSUK_1:def 1
for p being Element of X holds p in it . p;
existence
ex b1 being Function of X,D st
for p being Element of X holds p in b1 . p
proof end;
correctness
uniqueness
for b1, b2 being Function of X,D st ( for p being Element of X holds p in b1 . p ) & ( for p being Element of X holds p in b2 . p ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def1 defines proj BORSUK_1:def 1 :
for X being non empty set
for D being non empty a_partition of X
for b3 being Function of X,D holds
( b3 = proj D iff for p being Element of X holds p in b3 . p );

theorem Th29: :: BORSUK_1:29
for X being non empty set
for D being non empty a_partition of X
for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p
proof end;

theorem Th30: :: BORSUK_1:30
for X being non empty set
for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}
proof end;

theorem Th31: :: BORSUK_1:31
for X being non empty set
for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A
proof end;

theorem Th32: :: BORSUK_1:32
for X being non empty set
for D being non empty a_partition of X
for W being Element of D ex W' being Element of X st (proj D) . W' = W
proof end;

theorem Th33: :: BORSUK_1:33
for X being non empty set
for D being non empty a_partition of X
for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)
proof end;

theorem :: BORSUK_1:34
canceled;

theorem Th35: :: BORSUK_1:35
for X being TopStruct
for Y being SubSpace of X holds the carrier of Y c= the carrier of X
proof end;

definition
let X be 1-sorted ;
let Y be non empty 1-sorted ;
let y be Element of Y;
func X --> y -> Function of X,Y equals :: BORSUK_1:def 2
the carrier of X --> y;
coherence
the carrier of X --> y is Function of X,Y ;
end;

:: deftheorem defines --> BORSUK_1:def 2 :
for X being 1-sorted
for Y being non empty 1-sorted
for y being Element of Y holds X --> y = the carrier of X --> y;

theorem Th36: :: BORSUK_1:36
for X being TopSpace
for Y being non empty TopSpace
for y being Point of Y holds X --> y is continuous
proof end;

registration
let X be TopSpace;
let Y be non empty TopSpace;
let y be Point of Y;
cluster X --> y -> continuous ;
coherence
X --> y is continuous by Th36;
end;

definition
let X, Y be non empty TopSpace;
let F be Function of X,Y;
redefine attr F is continuous means :: BORSUK_1:def 3
for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G;
compatibility
( F is continuous iff for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G )
proof end;
end;

:: deftheorem defines continuous BORSUK_1:def 3 :
for X, Y being non empty TopSpace
for F being Function of X,Y holds
( F is continuous iff for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G );

registration
let S be TopSpace;
let T be non empty TopSpace;
cluster continuous Relation of the carrier of S,the carrier of T;
existence
ex b1 being Function of S,T st b1 is continuous
proof end;
end;

registration
let X, Y, Z be non empty TopSpace;
let F be continuous Function of X,Y;
let G be continuous Function of Y,Z;
cluster F * G -> continuous Function of X,Z;
coherence
G * F is continuous Function of X,Z by TOPS_2:58;
end;

theorem Th37: :: BORSUK_1:37
for X, Y being non empty TopSpace
for A being continuous Function of X,Y
for G being Subset of Y holds A " (Int G) c= Int (A " G)
proof end;

theorem Th38: :: BORSUK_1:38
for Y, X being non empty TopSpace
for W being Point of Y
for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
proof end;

definition
let X, Y be non empty TopSpace;
let W be Point of Y;
let A be continuous Function of X,Y;
let G be a_neighborhood of W;
:: original: "
redefine func A " G -> a_neighborhood of A " {W};
correctness
coherence
A " G is a_neighborhood of A " {W};
by Th38;
end;

theorem Th39: :: BORSUK_1:39
for X being non empty TopSpace
for A, B being Subset of X
for U being a_neighborhood of B st A c= B holds
U is a_neighborhood of A
proof end;

theorem :: BORSUK_1:40
canceled;

theorem Th41: :: BORSUK_1:41
for X being non empty TopSpace
for x being Point of X holds {x} is compact
proof end;

theorem Th42: :: BORSUK_1:42
for X being TopStruct
for Y being SubSpace of X
for A being Subset of X
for B being Subset of Y st A = B holds
( A is compact iff B is compact )
proof end;

definition
let X, Y be TopSpace;
canceled;
func [:X,Y:] -> strict TopSpace means :Def5: :: BORSUK_1:def 5
( the carrier of it = [:the carrier of X,the carrier of Y:] & the topology of it = { (union A) where A is Subset-Family of it : A 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 ) } } );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = [:the carrier of X,the carrier of Y:] & the topology of b1 = { (union A) where A is Subset-Family of b1 : A 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 end;
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = [:the carrier of X,the carrier of Y:] & the topology of b1 = { (union A) where A is Subset-Family of b1 : A 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 ) } } & the carrier of b2 = [:the carrier of X,the carrier of Y:] & the topology of b2 = { (union A) where A is Subset-Family of b2 : A 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 ) } } holds
b1 = b2 ;
end;

:: deftheorem BORSUK_1:def 4 :
canceled;

:: deftheorem Def5 defines [: BORSUK_1:def 5 :
for X, Y being TopSpace
for b3 being strict TopSpace holds
( b3 = [:X,Y:] iff ( the carrier of b3 = [:the carrier of X,the carrier of Y:] & the topology of b3 = { (union A) where A is Subset-Family of b3 : A 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 ) } } ) );

registration
let X, Y be non empty TopSpace;
cluster [:X,Y:] -> non empty strict ;
coherence
not [:X,Y:] is empty
proof end;
end;

theorem :: BORSUK_1:43
canceled;

theorem :: BORSUK_1:44
canceled;

theorem Th45: :: BORSUK_1:45
for X, Y being TopSpace
for B being Subset of [:X,Y:] holds
( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( 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 ) ) ) )
proof end;

definition
let X, Y be TopSpace;
let A be Subset of X;
let B be Subset of Y;
:: original: [:
redefine func [:A,B:] -> Subset of [:X,Y:];
correctness
coherence
[:A,B:] is Subset of [:X,Y:];
proof end;
end;

definition
let X, Y be non empty TopSpace;
let x be Point of X;
let y be Point of Y;
:: original: [
redefine func [x,y] -> Point of [:X,Y:];
correctness
coherence
[x,y] is Point of [:X,Y:];
proof end;
end;

theorem Th46: :: BORSUK_1:46
for X, Y being TopSpace
for V being Subset of X
for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
proof end;

theorem Th47: :: BORSUK_1:47
for X, Y being TopSpace
for V being Subset of X
for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
proof end;

theorem Th48: :: BORSUK_1:48
for X, Y being non empty TopSpace
for x being Point of X
for y being Point of Y
for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
proof end;

theorem Th49: :: BORSUK_1:49
for X, Y being non empty TopSpace
for A being Subset of X
for B being Subset of Y
for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
proof end;

definition
let X, Y be non empty TopSpace;
let x be Point of X;
let y be Point of Y;
let V be a_neighborhood of x;
let W be a_neighborhood of y;
:: original: [:
redefine func [:V,W:] -> a_neighborhood of [x,y];
correctness
coherence
[:V,W:] is a_neighborhood of [x,y];
by Th48;
end;

theorem Th50: :: BORSUK_1:50
for X, Y being non empty TopSpace
for XT being Point of [:X,Y:] ex W being Point of X ex T being Point of Y st XT = [W,T]
proof end;

definition
let X, Y be non empty TopSpace;
let A be Subset of X;
let t be Point of Y;
let V be a_neighborhood of A;
let W be a_neighborhood of t;
:: original: [:
redefine func [:V,W:] -> a_neighborhood of [:A,{t}:];
correctness
coherence
[:V,W:] is a_neighborhood of [:A,{t}:];
proof end;
end;

definition
let X, Y be TopSpace;
let A be Subset of [:X,Y:];
func Base-Appr A -> Subset-Family of [:X,Y:] equals :: BORSUK_1:def 6
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ;
coherence
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } is Subset-Family of [:X,Y:]
proof end;
end;

:: deftheorem defines Base-Appr BORSUK_1:def 6 :
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Base-Appr A = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ;

theorem Th51: :: BORSUK_1:51
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Base-Appr A is open
proof end;

theorem Th52: :: BORSUK_1:52
for X, Y being TopSpace
for A, B being Subset of [:X,Y:] st A c= B holds
Base-Appr A c= Base-Appr B
proof end;

theorem Th53: :: BORSUK_1:53
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds union (Base-Appr A) c= A
proof end;

theorem Th54: :: BORSUK_1:54
for X, Y being TopSpace
for A being Subset of [:X,Y:] st A is open holds
A = union (Base-Appr A)
proof end;

theorem Th55: :: BORSUK_1:55
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Int A = union (Base-Appr A)
proof end;

definition
let X, Y be non empty TopSpace;
func Pr1 X,Y -> Function of bool the carrier of [:X,Y:], bool the carrier of X equals :: BORSUK_1:def 7
 .: (pr1 the carrier of X,the carrier of Y);
coherence
.: (pr1 the carrier of X,the carrier of Y) is Function of bool the carrier of [:X,Y