:: BORSUK_3 semantic presentation

theorem Th1: :: BORSUK_3:1

for b₁, b₂ being TopSpace holds [#] [:b₁,b₂:] = [:([#] b₁),([#] b₂):]

proof end;

registration

let c₁ be set ;
let c₂ be empty set ;
cluster [:a₁,a₂:] -> empty ;
coherence by ZFMISC_1:113;

end;

registration

let c₁ be empty set ;
let c₂ be set ;
cluster [:a₁,a₂:] -> empty ;
coherence by ZFMISC_1:113;

end;

theorem Th2: :: BORSUK_3:2

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁ holds b₂ --> b₃ is continuous Function of b₂,(b₁ | {b₃})

proof end;

registration

let c₁ be non empty TopStruct ;
cluster id a₁ -> being_homeomorphism ;
coherence by TOPGRP_1:20;

end;

Lemma3: for b₁ being non empty TopStruct holds b₁,b₁ are_homeomorphic

proof end;

Lemma4: for b₁, b₂ being non empty TopStruct st b₁,b₂ are_homeomorphic holds
b₂,b₁ are_homeomorphic

proof end;

definition

let c₁, c₂ be non empty TopStruct ;
redefine pred are_homeomorphic as c₁,c₂ are_homeomorphic ;
reflexivity by Lemma3;
symmetry by Lemma4;

end;

theorem Th3: :: BORSUK_3:3

for b₁, b₂, b₃ being non empty TopSpace st b₁,b₂ are_homeomorphic & b₂,b₃ are_homeomorphic holds
b₁,b₃ are_homeomorphic

proof end;

registration

let c₁ be TopStruct ;
let c₂ be empty Subset of c₁;
cluster a₁ | a₂ -> empty ;
coherence

proof end;

end;

registration

cluster empty strict TopStruct ;
existence

proof end;

end;

theorem Th4: :: BORSUK_3:4

for b₁ being TopSpace
for b₂ being empty TopSpace holds
( [:b₁,b₂:] is empty & [:b₂,b₁:] is empty )

proof end;

theorem Th5: :: BORSUK_3:5

for b₁ being empty TopSpace holds b₁ is compact

proof end;

registration

cluster empty -> compact TopStruct ;
coherence by Th5;

end;

registration

let c₁ be TopSpace;
let c₂ be empty TopSpace;
cluster [:a₁,a₂:] -> empty compact ;
coherence by Th4;

end;

theorem Th6: :: BORSUK_3:6

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Function of [:b₂,(b₁ | {b₃}):],b₂ st b₄ = pr1 the carrier of b₂,{b₃} holds
b₄ is one-to-one

proof end;

theorem Th7: :: BORSUK_3:7

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Function of [:(b₁ | {b₃}),b₂:],b₂ st b₄ = pr2 {b₃},the carrier of b₂ holds
b₄ is one-to-one

proof end;

theorem Th8: :: BORSUK_3:8

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Function of [:b₂,(b₁ | {b₃}):],b₂ st b₄ = pr1 the carrier of b₂,{b₃} holds
b₄ " = <:(id b₂),(b₂ --> b₃):>

proof end;

theorem Th9: :: BORSUK_3:9

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Function of [:(b₁ | {b₃}),b₂:],b₂ st b₄ = pr2 {b₃},the carrier of b₂ holds
b₄ " = <:(b₂ --> b₃),(id b₂):>

proof end;

theorem Th10: :: BORSUK_3:10

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Function of [:b₂,(b₁ | {b₃}):],b₂ st b₄ = pr1 the carrier of b₂,{b₃} holds
b₄ is_homeomorphism

proof end;

theorem Th11: :: BORSUK_3:11

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Function of [:(b₁ | {b₃}),b₂:],b₂ st b₄ = pr2 {b₃},the carrier of b₂ holds
b₄ is_homeomorphism

proof end;

theorem Th12: :: BORSUK_3:12

for b₁ being non empty TopSpace
for b₂ being non empty compact TopSpace
for b₃ being open Subset of [:b₁,b₂:]
for b₄ being set st b₄ in { b₅ where B is Point of b₁ : [:{b₅},the carrier of b₂:] c= b₃ } holds
ex b₅ being ManySortedSet of the carrier of b₂ st
for b₆ being set st b₆ in the carrier of b₂ holds
ex b₇ being Subset of b₁ex b₈ being Subset of b₂ st
( b₅ . b₆ = [b₇,b₈] & [b₄,b₆] in [:b₇,b₈:] & b₇ is open & b₈ is open & [:b₇,b₈:] c= b₃ )

proof end;

theorem Th13: :: BORSUK_3:13

for b₁ being non empty TopSpace
for b₂ being non empty compact TopSpace
for b₃ being open Subset of [:b₂,b₁:]
for b₄ being set st b₄ in { b₅ where B is Point of b₁ : [:([#] b₂),{b₅}:] c= b₃ } holds
ex b₅ being open Subset of b₁ st
( b₄ in b₅ & b₅ c= { b₆ where B is Point of b₁ : [:([#] b₂),{b₆}:] c= b₃ } )

proof end;

theorem Th14: :: BORSUK_3:14

for b₁ being non empty TopSpace
for b₂ being non empty compact TopSpace
for b₃ being open Subset of [:b₂,b₁:] holds { b₄ where B is Point of b₁ : [:([#] b₂),{b₄}:] c= b₃ } in the topology of b₁

proof end;

theorem Th15: :: BORSUK_3:15

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁ holds [:(b₁ | {b₃}),b₂:],b₂ are_homeomorphic

proof end;

Lemma15: for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being non empty Subset of b₁ st b₄ = {b₃} holds
[:b₂,(b₁ | b₄):],b₂ are_homeomorphic

proof end;

theorem Th16: :: BORSUK_3:16

for b₁, b₂ being non empty TopSpace st b₁,b₂ are_homeomorphic & b₁ is compact holds
b₂ is compact

proof end;

theorem Th17: :: BORSUK_3:17

for b₁, b₂ being TopSpace
for b₃ being SubSpace of b₁ holds [:b₂,b₃:] is SubSpace of [:b₂,b₁:]

proof end;

Lemma18: for b₁, b₂ being TopSpace
for b₃ being Subset of [:b₂,b₁:]
for b₄ being Subset of b₁ st b₃ = [:([#] b₂),b₄:] holds
TopStruct(# the carrier of [:b₂,(b₁ | b₄):],the topology of [:b₂,(b₁ | b₄):] #) = TopStruct(# the carrier of ([:b₂,b₁:] | b₃),the topology of ([:b₂,b₁:] | b₃) #)

proof end;

theorem Th18: :: BORSUK_3:18

for b₁ being non empty TopSpace
for b₂ being non empty compact TopSpace
for b₃ being Point of b₁
for b₄ being Subset of [:b₂,b₁:] st b₄ = [:([#] b₂),{b₃}:] holds
b₄ is compact

proof end;

theorem Th19: :: BORSUK_3:19

for b₁ being non empty TopSpace
for b₂ being non empty compact TopSpace
for b₃ being Point of b₁ holds [:b₂,(b₁ | {b₃}):] is compact

proof end;

theorem Th20: :: BORSUK_3:20

for b₁, b₂ being non empty compact TopSpace
for b₃ being Subset-Family of b₁ st b₃ = { b₄ where B is open Subset of b₁ : [:([#] b₂),b₄:] c= union (Base-Appr ([#] [:b₂,b₁:])) } holds
( b₃ is open & b₃ is_a_cover_of [#] b₁ )

proof end;

theorem Th21: :: BORSUK_3:21

for b₁, b₂ being non empty compact TopSpace
for b₃ being Subset-Family of b₁
for b₄ being Subset-Family of [:b₂,b₁:] st b₄ is_a_cover_of [:b₂,b₁:] & b₄ is open & b₃ = { b₅ where B is open Subset of b₁ : ex b₁ being Subset-Family of [:b₂,b₁:] st
( b₆ c= b₄ & b₆ is finite & [:([#] b₂),b₅:] c= union b₆ ) } holds
( b₃ is open & b₃ is_a_cover_of b₁ )

proof end;

theorem Th22: :: BORSUK_3:22

proof end;

theorem Th23: :: BORSUK_3:23

for b₁, b₂ being non empty compact TopSpace
for b₃ being Subset-Family of [:b₂,b₁:] st b₃ is_a_cover_of [:b₂,b₁:] & b₃ is open holds
ex b₄ being Subset-Family of [:b₂,b₁:] st
( b₄ c= b₃ & b₄ is_a_cover_of [:b₂,b₁:] & b₄ is finite )

proof end;

Lemma23: for b₁, b₂ being non empty compact TopSpace holds [:b₁,b₂:] is compact

proof end;

theorem Th24: :: BORSUK_3:24

for b₁, b₂ being TopSpace st b₁ is compact & b₂ is compact holds
[:b₁,b₂:] is compact

proof end;

registration

let c₁, c₂ be compact TopSpace;
cluster [:a₁,a₂:] -> compact ;
coherence by Th24;

end;

Lemma25: for b₁, b₂ being TopSpace
for b₃ being SubSpace of b₁ holds [:b₃,b₂:] is SubSpace of [:b₁,b₂:]

proof end;

theorem Th25: :: BORSUK_3:25

for b₁, b₂ being TopSpace
for b₃ being SubSpace of b₁
for b₄ being SubSpace of b₂ holds [:b₃,b₄:] is SubSpace of [:b₁,b₂:]

proof end;

theorem Th26: :: BORSUK_3:26

for b₁, b₂ being TopSpace
for b₃ being Subset of [:b₂,b₁:]
for b₄ being Subset of b₁
for b₅ being Subset of b₂ st b₃ = [:b₅,b₄:] holds
TopStruct(# the carrier of [:(b₂ | b₅),(b₁ | b₄):],the topology of [:(b₂ | b₅),(b₁ | b₄):] #) = TopStruct(# the carrier of ([:b₂,b₁:] | b₃),the topology of ([:b₂,b₁:] | b₃) #)

proof end;

registration

let c₁ be TopStruct ;
cluster compact Element of bool the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be TopSpace;
let c₂ be compact Subset of c₁;
cluster a₁ | a₂ -> compact ;
coherence

proof end;

end;

theorem Th27: :: BORSUK_3:27

for b₁, b₂ being TopSpace
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ is compact & b₄ is compact holds
[:b₃,b₄:] is compact Subset of [:b₁,b₂:]

proof end;