:: BORSUK_2 semantic presentation

Lemma1: for b₁ being real number holds
( ( 0 <= b₁ & b₁ <= 1 ) iff b₁ in the carrier of I[01] )

proof end;

scheme :: BORSUK_2:sch 1
s1{ F₁() -> non empty set , F₂() -> set , F₃( set ) -> set , P₁[ set ] } :

Card { F₃(b₁) where B is Element of F₁() : ( b₁ in F₂() & P₁[b₁] ) } <=` Card F₂()

proof end;

theorem Th1: :: BORSUK_2:1

for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₂ st b₁ is SubSpace of b₄ & b₃ is SubSpace of b₄ & ([#] b₁) \/ ([#] b₃) = [#] b₄ & b₁ is compact & b₃ is compact & b₄ is_T2 & b₅ is continuous & b₆ is continuous & ( for b₇ being set st b₇ in ([#] b₁) /\ ([#] b₃) holds
b₅ . b₇ = b₆ . b₇ ) holds
ex b₇ being Function of b₄,b₂ st
( b₇ = b₅ +* b₆ & b₇ is continuous )

proof end;

registration

let c₁ be non empty TopStruct ;
cluster id a₁ -> continuous open ;
coherence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
cluster one-to-one continuous M5(the carrier of a₁,the carrier of a₁);
existence

proof end;

end;

theorem Th2: :: BORSUK_2:2

canceled;

theorem Th3: :: BORSUK_2:3

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is_homeomorphism holds
b₃ " is open

proof end;

registration

cluster -> real Element of the carrier of I[01] ;
coherence

proof end;

end;

theorem Th4: :: BORSUK_2:4

for b₁ being non empty TopSpace
for b₂ being Point of b₁ ex b₃ being Function of I[01] ,b₁ st
( b₃ is continuous & b₃ . 0 = b₂ & b₃ . 1 = b₂ )

proof end;

definition

let c₁ be TopStruct ;
let c₂, c₃ be Point of c₁;
pred c₂,c₃ are_connected means :Def1: :: BORSUK_2:def 1
ex b₁ being Function of I[01] ,a₁ st
( b₁ is continuous & b₁ . 0 = a₂ & b₁ . 1 = a₃ );

end;

:: deftheorem Def1 defines are_connected BORSUK_2:def 1 :

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Point of c₁;
redefine pred are_connected as c₂,c₃ are_connected ;
reflexivity

proof end;

end;

definition

let c₁ be TopStruct ;
let c₂, c₃ be Point of c₁;
assume E4: c₂,c₃ are_connected ;
mode Path of c₂,c₃ -> Function of I[01] ,a₁ means :Def2: :: BORSUK_2:def 2
( a₄ is continuous & a₄ . 0 = a₂ & a₄ . 1 = a₃ );
existence by E4, Def1;

end;

:: deftheorem Def2 defines Path BORSUK_2:def 2 :

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster continuous Path of a₂,a₂;
existence

proof end;

end;

definition

let c₁ be TopStruct ;
attr a₁ is arcwise_connected means :Def3: :: BORSUK_2:def 3
for b₁, b₂ being Point of a₁ holds b₁,b₂ are_connected ;
correctness ;

end;

:: deftheorem Def3 defines arcwise_connected BORSUK_2:def 3 :

registration

cluster non empty arcwise_connected TopStruct ;
existence

proof end;

end;

definition

let c₁ be arcwise_connected TopStruct ;
let c₂, c₃ be Point of c₁;
redefine mode Path of c₂,c₃ -> Function of I[01] ,a₁ means :Def4: :: BORSUK_2:def 4
( a₄ is continuous & a₄ . 0 = a₂ & a₄ . 1 = a₃ );
compatibility

proof end;

end;

:: deftheorem Def4 defines Path BORSUK_2:def 4 :

registration

let c₁ be arcwise_connected TopStruct ;
let c₂, c₃ be Point of c₁;
cluster -> continuous Path of a₂,a₃;
coherence by Def4;

end;

Lemma7: ( 0 in [.0,1.] & 1 in [.0,1.] )

proof end;

theorem Th5: :: BORSUK_2:5

for b₁ being non empty TopSpace st b₁ is arcwise_connected holds
b₁ is connected

proof end;

registration

cluster non empty arcwise_connected -> non empty connected TopStruct ;
coherence by Th5;

end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃, c₄ be Point of c₁;
let c₅ be Path of c₂,c₃;
let c₆ be Path of c₃,c₄;
assume that
E9: c₂,c₃ are_connected and
E10: c₃,c₄ are_connected ;
func c₅ + c₆ -> Path of a₂,a₄ means :Def5: :: BORSUK_2:def 5
for b₁ being Point of I[01] holds
( ( b₁ <= 1 / 2 implies a₇ . b₁ = a₅ . (2 * b₁) ) & ( 1 / 2 <= b₁ implies a₇ . b₁ = a₆ . ((2 * b₁) - 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + BORSUK_2:def 5 :

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster constant Path of a₂,a₂;
existence

proof end;

end;

theorem Th6: :: BORSUK_2:6

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being constant Path of b₂,b₂ holds b₃ = I[01] --> b₂

proof end;

theorem Th7: :: BORSUK_2:7

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being constant Path of b₂,b₂ holds b₃ + b₃ = b₃

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
let c₃ be constant Path of c₂,c₂;
cluster a₃ + a₃ -> constant ;
coherence by Th7;

end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Point of c₁;
let c₄ be Path of c₂,c₃;
assume E11: c₂,c₃ are_connected ;
func - c₄ -> Path of a₃,a₂ means :Def6: :: BORSUK_2:def 6
for b₁ being Point of I[01] holds a₅ . b₁ = a₄ . (1 - b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - BORSUK_2:def 6 :

Lemma12: for b₁ being Real st 0 <= b₁ & b₁ <= 1 holds
( 0 <= 1 - b₁ & 1 - b₁ <= 1 )

proof end;

Lemma13: for b₁ being Real st b₁ in the carrier of I[01] holds
1 - b₁ in the carrier of I[01]

proof end;

theorem Th8: :: BORSUK_2:8

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being constant Path of b₂,b₂ holds - b₃ = b₃

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
let c₃ be constant Path of c₂,c₂;
cluster - a₃ -> constant ;
coherence by Th8;

end;

theorem Th9: :: BORSUK_2:9

for b₁, b₂ being non empty TopSpace
for b₃ being Subset-Family of b₂
for b₄ being Function of b₁,b₂ holds b₄ " (union b₃) = union (b₄ " b₃)

proof end;

definition

let c₁, c₂, c₃, c₄ be non empty TopSpace;
let c₅ be Function of c₁,c₂;
let c₆ be Function of c₃,c₄;
redefine func [: as [:c₅,c₆:] -> Function of [:a₁,a₃:],[:a₂,a₄:];
coherence

proof end;

end;

theorem Th10: :: BORSUK_2:10

for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being continuous Function of b₁,b₃
for b₆ being continuous Function of b₂,b₄
for b₇, b₈ being Subset of [:b₃,b₄:] st b₈ in Base-Appr b₇ holds
[:b₅,b₆:] " b₈ is open

proof end;

theorem Th11: :: BORSUK_2:11

for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being continuous Function of b₁,b₃
for b₆ being continuous Function of b₂,b₄
for b₇ being Subset of [:b₃,b₄:] st b₇ is open holds
[:b₅,b₆:] " b₇ is open

proof end;

theorem Th12: :: BORSUK_2:12

for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being continuous Function of b₁,b₃
for b₆ being continuous Function of b₂,b₄ holds [:b₅,b₆:] is continuous

proof end;

registration

cluster empty -> T_0 TopStruct ;
coherence by T_0TOPSP:def 7;

end;

registration

let c₁, c₂ be non empty discerning TopSpace;
cluster [:a₁,a₂:] -> discerning ;
coherence

proof end;

end;

theorem Th13: :: BORSUK_2:13

canceled;

theorem Th14: :: BORSUK_2:14

for b₁, b₂ being non empty TopSpace st b₁ is_T1 & b₂ is_T1 holds
[:b₁,b₂:] is_T1

proof end;

registration

let c₁, c₂ be non empty being_T1 TopSpace;
cluster [:a₁,a₂:] -> being_T1 ;
coherence by Th14;

end;

Lemma20: for b₁, b₂ being non empty TopSpace st b₁ is_T2 & b₂ is_T2 holds
[:b₁,b₂:] is_T2

proof end;

registration

let c₁, c₂ be non empty being_T2 TopSpace;
cluster [:a₁,a₂:] -> discerning being_T2 ;
coherence by Lemma20;

end;

registration

cluster I[01] -> compact being_T2 ;
coherence

proof end;

end;

definition

let c₁ be non empty TopStruct ;
let c₂, c₃ be Point of c₁;
let c₄, c₅ be Path of c₂,c₃;
pred c₄,c₅ are_homotopic means :: BORSUK_2:def 7
ex b₁ being Function of [:I[01] ,I[01] :],a₁ st
( b₁ is continuous & ( for b₂ being Point of I[01] holds
( b₁ . b₂,0 = a₄ . b₂ & b₁ . b₂,1 = a₅ . b₂ & ( for b₃ being Point of I[01] holds
( b₁ . 0,b₃ = a₂ & b₁ . 1,b₃ = a₃ ) ) ) ) );
symmetry

proof end;

end;

:: deftheorem Def7 defines are_homotopic BORSUK_2:def 7 :

theorem Th15: :: BORSUK_2:15

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Path of b₂,b₃ st b₂,b₃ are_connected holds
b₄,b₄ are_homotopic

proof end;

definition

let c₁ be non empty arcwise_connected TopSpace;
let c₂, c₃ be Point of c₁;
let c₄, c₅ be Path of c₂,c₃;
redefine pred are_homotopic as c₄,c₅ are_homotopic ;
reflexivity

proof end;

end;