:: BORSUK_3 semantic presentation

theorem Th1: :: BORSUK_3:1
for b1, b2 being TopSpace holds [#] [:b1,b2:] = [:([#] b1),([#] b2):]
proof end;

registration
let c1 be set ;
let c2 be empty set ;
cluster [:a1,a2:] -> empty ;
coherence
[:c1,c2:] is empty
by ZFMISC_1:113;
end;

registration
let c1 be empty set ;
let c2 be set ;
cluster [:a1,a2:] -> empty ;
coherence
[:c1,c2:] is empty
by ZFMISC_1:113;
end;

theorem Th2: :: BORSUK_3:2
for b1, b2 being non empty TopSpace
for b3 being Point of b1 holds b2 --> b3 is continuous Function of b2,(b1 | {b3})
proof end;

registration
let c1 be non empty TopStruct ;
cluster id a1 -> being_homeomorphism ;
coherence
id c1 is being_homeomorphism
by TOPGRP_1:20;
end;

Lemma3: for b1 being non empty TopStruct holds b1,b1 are_homeomorphic
proof end;

Lemma4: for b1, b2 being non empty TopStruct st b1,b2 are_homeomorphic holds
b2,b1 are_homeomorphic
proof end;

definition
let c1, c2 be non empty TopStruct ;
redefine pred are_homeomorphic as c1,c2 are_homeomorphic ;
reflexivity
for b1 being non empty TopStruct holds b1,b1 are_homeomorphic
by Lemma3;
symmetry
for b1, b2 being non empty TopStruct st b1,b2 are_homeomorphic holds
b2,b1 are_homeomorphic
by Lemma4;
end;

theorem Th3: :: BORSUK_3:3
for b1, b2, b3 being non empty TopSpace st b1,b2 are_homeomorphic & b2,b3 are_homeomorphic holds
b1,b3 are_homeomorphic
proof end;

registration
let c1 be TopStruct ;
let c2 be empty Subset of c1;
cluster a1 | a2 -> empty ;
coherence
c1 | c2 is empty
proof end;
end;

registration
cluster empty strict TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & b1 is empty )
proof end;
end;

theorem Th4: :: BORSUK_3:4
for b1 being TopSpace
for b2 being empty TopSpace holds
( [:b1,b2:] is empty & [:b2,b1:] is empty )
proof end;

theorem Th5: :: BORSUK_3:5
for b1 being empty TopSpace holds b1 is compact
proof end;

registration
cluster empty -> compact TopStruct ;
coherence
for b1 being TopSpace st b1 is empty holds
b1 is compact
by Th5;
end;

registration
let c1 be TopSpace;
let c2 be empty TopSpace;
cluster [:a1,a2:] -> empty compact ;
coherence
[:c1,c2:] is empty
by Th4;
end;

theorem Th6: :: BORSUK_3:6
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:b2,(b1 | {b3}):],b2 st b4 = pr1 the carrier of b2,{b3} holds
b4 is one-to-one
proof end;

theorem Th7: :: BORSUK_3:7
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:(b1 | {b3}),b2:],b2 st b4 = pr2 {b3},the carrier of b2 holds
b4 is one-to-one
proof end;

theorem Th8: :: BORSUK_3:8
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:b2,(b1 | {b3}):],b2 st b4 = pr1 the carrier of b2,{b3} holds
b4 " = <:(id b2),(b2 --> b3):>
proof end;

theorem Th9: :: BORSUK_3:9
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:(b1 | {b3}),b2:],b2 st b4 = pr2 {b3},the carrier of b2 holds
b4 " = <:(b2 --> b3),(id b2):>
proof end;

theorem Th10: :: BORSUK_3:10
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:b2,(b1 | {b3}):],b2 st b4 = pr1 the carrier of b2,{b3} holds
b4 is_homeomorphism
proof end;

theorem Th11: :: BORSUK_3:11
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of [:(b1 | {b3}),b2:],b2 st b4 = pr2 {b3},the carrier of b2 holds
b4 is_homeomorphism
proof end;

theorem Th12: :: BORSUK_3:12
for b1 being non empty TopSpace
for b2 being non empty compact TopSpace
for b3 being open Subset of [:b1,b2:]
for b4 being set st b4 in { b5 where B is Point of b1 : [:{b5},the carrier of b2:] c= b3 } holds
ex b5 being ManySortedSet of the carrier of b2 st
for b6 being set st b6 in the carrier of b2 holds
ex b7 being Subset of b1ex b8 being Subset of b2 st
( b5 . b6 = [b7,b8] & [b4,b6] in [:b7,b8:] & b7 is open & b8 is open & [:b7,b8:] c= b3 )
proof end;

theorem Th13: :: BORSUK_3:13
for b1 being non empty TopSpace
for b2 being non empty compact TopSpace
for b3 being open Subset of [:b2,b1:]
for b4 being set st b4 in { b5 where B is Point of b1 : [:([#] b2),{b5}:] c= b3 } holds
ex b5 being open Subset of b1 st
( b4 in b5 & b5 c= { b6 where B is Point of b1 : [:([#] b2),{b6}:] c= b3 } )
proof end;

theorem Th14: :: BORSUK_3:14
for b1 being non empty TopSpace
for b2 being non empty compact TopSpace
for b3 being open Subset of [:b2,b1:] holds { b4 where B is Point of b1 : [:([#] b2),{b4}:] c= b3 } in the topology of b1
proof end;

theorem Th15: :: BORSUK_3:15
for b1, b2 being non empty TopSpace
for b3 being Point of b1 holds [:(b1 | {b3}),b2:],b2 are_homeomorphic
proof end;

Lemma15: for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being non empty Subset of b1 st b4 = {b3} holds
[:b2,(b1 | b4):],b2 are_homeomorphic
proof end;

theorem Th16: :: BORSUK_3:16
for b1, b2 being non empty TopSpace st b1,b2 are_homeomorphic & b1 is compact holds
b2 is compact
proof end;

theorem Th17: :: BORSUK_3:17
for b1, b2 being TopSpace
for b3 being SubSpace of b1 holds [:b2,b3:] is SubSpace of [:b2,b1:]
proof end;

Lemma18: for b1, b2 being TopSpace
for b3 being Subset of [:b2,b1:]
for b4 being Subset of b1 st b3 = [:([#] b2),b4:] holds
TopStruct(# the carrier of [:b2,(b1 | b4):],the topology of [:b2,(b1 | b4):] #) = TopStruct(# the carrier of ([:b2,b1:] | b3),the topology of ([:b2,b1:] | b3) #)
proof end;

theorem Th18: :: BORSUK_3:18
for b1 being non empty TopSpace
for b2 being non empty compact TopSpace
for b3 being Point of b1
for b4 being Subset of [:b2,b1:] st b4 = [:([#] b2),{b3}:] holds
b4 is compact
proof end;

theorem Th19: :: BORSUK_3:19
for b1 being non empty TopSpace
for b2 being non empty compact TopSpace
for b3 being Point of b1 holds [:b2,(b1 | {b3}):] is compact
proof end;

theorem Th20: :: BORSUK_3:20
for b1, b2 being non empty compact TopSpace
for b3 being Subset-Family of b1 st b3 = { b4 where B is open Subset of b1 : [:([#] b2),b4:] c= union (Base-Appr ([#] [:b2,b1:])) } holds
( b3 is open & b3 is_a_cover_of [#] b1 )
proof end;

theorem Th21: :: BORSUK_3:21
for b1, b2 being non empty compact TopSpace
for b3 being Subset-Family of b1
for b4 being Subset-Family of [:b2,b1:] st b4 is_a_cover_of [:b2,b1:] & b4 is open & b3 = { b5 where B is open Subset of b1 : ex b1 being Subset-Family of [:b2,b1:] st
( b6 c= b4 & b6 is finite & [:([#] b2),b5:] c= union b6 )
}
holds
( b3 is open & b3 is_a_cover_of b1 )
proof end;

theorem Th22: :: BORSUK_3:22
for b1, b2 being non empty compact TopSpace
for b3 being Subset-Family of b1
for b4 being Subset-Family of [:b2,b1:] st b4 is_a_cover_of [:b2,b1:] & b4 is open & b3 = { b5 where B is open Subset of b1 : ex b1 being Subset-Family of [:b2,b1:] st
( b6 c= b4 & b6 is finite & [:([#] b2),b5:] c= union b6 )
}
holds
ex b5 being Subset-Family of b1 st
( b5 c= b3 & b5 is finite & b5 is_a_cover_of b1 )
proof end;

theorem Th23: :: BORSUK_3:23
for b1, b2 being non empty compact TopSpace
for b3 being Subset-Family of [:b2,b1:] st b3 is_a_cover_of [:b2,b1:] & b3 is open holds
ex b4 being Subset-Family of [:b2,b1:] st
( b4 c= b3 & b4 is_a_cover_of [:b2,b1:] & b4 is finite )
proof end;

Lemma23: for b1, b2 being non empty compact TopSpace holds [:b1,b2:] is compact
proof end;

theorem Th24: :: BORSUK_3:24
for b1, b2 being TopSpace st b1 is compact & b2 is compact holds
[:b1,b2:] is compact
proof end;

registration
let c1, c2 be compact TopSpace;
cluster [:a1,a2:] -> compact ;
coherence
[:c1,c2:] is compact
by Th24;
end;

Lemma25: for b1, b2 being TopSpace
for b3 being SubSpace of b1 holds [:b3,b2:] is SubSpace of [:b1,b2:]
proof end;

theorem Th25: :: BORSUK_3:25
for b1, b2 being TopSpace
for b3 being SubSpace of b1
for b4 being SubSpace of b2 holds [:b3,b4:] is SubSpace of [:b1,b2:]
proof end;

theorem Th26: :: BORSUK_3:26
for b1, b2 being TopSpace
for b3 being Subset of [:b2,b1:]
for b4 being Subset of b1
for b5 being Subset of b2 st b3 = [:b5,b4:] holds
TopStruct(# the carrier of [:(b2 | b5),(b1 | b4):],the topology of [:(b2 | b5),(b1 | b4):] #) = TopStruct(# the carrier of ([:b2,b1:] | b3),the topology of ([:b2,b1:] | b3) #)
proof end;

registration
let c1 be TopStruct ;
cluster compact Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st b1 is compact
proof end;
end;

registration
let c1 be TopSpace;
let c2 be compact Subset of c1;
cluster a1 | a2 -> compact ;
coherence
c1 | c2 is compact
proof end;
end;

theorem Th27: :: BORSUK_3:27
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 is compact & b4 is compact holds
[:b3,b4:] is compact Subset of [:b1,b2:]
proof end;