:: BORSUK_2 semantic presentation

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

proof end;

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

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

proof end;

theorem :: BORSUK_2:1

for T1, S, T2, T being non empty TopSpace
for f being Function of T1,S
for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is_T2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds
f . p = g . p ) holds
ex h being Function of T,S st
( h = f +* g & h is continuous )

proof end;

registration

let T be non empty TopStruct ;
cluster id T -> continuous open ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem :: BORSUK_2:2

canceled;

theorem :: BORSUK_2:3

for S, T being non empty TopSpace
for f being Function of S,T st f is_homeomorphism holds
f " is open

proof end;

registration

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

proof end;

end;

theorem Th4: :: BORSUK_2:4

for T being non empty TopSpace
for a being Point of T ex f being Function of I[01] ,T st
( f is continuous & f . 0 = a & f . 1 = a )

proof end;

definition

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

end;

:: deftheorem Def1 defines are_connected BORSUK_2:def 1 :

definition

let T be non empty TopSpace;
let a, b be Point of T;
:: original: are_connected
redefine pred a,b are_connected ;
reflexivity

proof end;

end;

definition

let T be TopStruct ;
let a, b be Point of T;
assume A1: a,b are_connected ;
mode Path of a,b -> Function of I[01] ,T means :Def2: :: BORSUK_2:def 2
( it is continuous & it . 0 = a & it . 1 = b );
existence by A1, Def1;

end;

:: deftheorem Def2 defines Path BORSUK_2:def 2 :

registration

let T be non empty TopSpace;
let a be Point of T;
cluster continuous Path of a,a;
existence

proof end;

end;

definition

let T be TopStruct ;
attr T is arcwise_connected means :Def3: :: BORSUK_2:def 3
for a, b being Point of T holds a,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 T be arcwise_connected TopStruct ;
let a, b be Point of T;
redefine mode Path of a,b means :Def4: :: BORSUK_2:def 4
( it is continuous & it . 0 = a & it . 1 = b );
compatibility

proof end;

end;

:: deftheorem Def4 defines Path BORSUK_2:def 4 :

registration

let T be arcwise_connected TopStruct ;
let a, b be Point of T;
cluster -> continuous Path of a,b;
coherence by Def4;

end;

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

proof end;

theorem Th5: :: BORSUK_2:5

for GX being non empty TopSpace st GX is arcwise_connected holds
GX is connected

proof end;

registration

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

end;

definition

let T be non empty TopSpace;
let a, b, c be Point of T;
let P be Path of a,b;
let Q be Path of b,c;
assume that
A1: a,b are_connected and
A2: b,c are_connected ;
func P + Q -> Path of a,c means :Def5: :: BORSUK_2:def 5
for t being Point of I[01] holds
( ( t <= 1 / 2 implies it . t = P . (2 * t) ) & ( 1 / 2 <= t implies it . t = Q . ((2 * t) - 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + BORSUK_2:def 5 :

registration

let T be non empty TopSpace;
let a be Point of T;
cluster constant Path of a,a;
existence

proof end;

end;

theorem :: BORSUK_2:6

for T being non empty TopSpace
for a being Point of T
for P being constant Path of a,a holds P = I[01] --> a

proof end;

theorem Th7: :: BORSUK_2:7

for T being non empty TopSpace
for a being Point of T
for P being constant Path of a,a holds P + P = P

proof end;

registration

let T be non empty TopSpace;
let a be Point of T;
let P be constant Path of a,a;
cluster P + P -> constant ;
coherence by Th7;

end;

definition

let T be non empty TopSpace;
let a, b be Point of T;
let P be Path of a,b;
assume A1: a,b are_connected ;
func - P -> Path of b,a means :Def6: :: BORSUK_2:def 6
for t being Point of I[01] holds it . t = P . (1 - t);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - BORSUK_2:def 6 :

Lm3: for r being Real st 0 <= r & r <= 1 holds
( 0 <= 1 - r & 1 - r <= 1 )

proof end;

Lm4: for r being Real st r in the carrier of I[01] holds
1 - r in the carrier of I[01]

proof end;

theorem Th8: :: BORSUK_2:8

for T being non empty TopSpace
for a being Point of T
for P being constant Path of a,a holds - P = P

proof end;

registration

let T be non empty TopSpace;
let a be Point of T;
let P be constant Path of a,a;
cluster - P -> constant ;
coherence by Th8;

end;

theorem Th9: :: BORSUK_2:9

for X, Y being non empty TopSpace
for A being Subset-Family of Y
for f being Function of X,Y holds f " (union A) = union (f " A)

proof end;

definition

let S1, S2, T1, T2 be non empty TopSpace;
let f be Function of S1,S2;
let g be Function of T1,T2;
:: original: [:
redefine func [:f,g:] -> Function of [:S1,T1:],[:S2,T2:];
coherence

proof end;

end;

theorem Th10: :: BORSUK_2:10

for S1, S2, T1, T2 being non empty TopSpace
for f being continuous Function of S1,T1
for g being continuous Function of S2,T2
for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds
[:f,g:] " P2 is open

proof end;

theorem Th11: :: BORSUK_2:11

for S1, S2, T1, T2 being non empty TopSpace
for f being continuous Function of S1,T1
for g being continuous Function of S2,T2
for P2 being Subset of [:T1,T2:] st P2 is open holds
[:f,g:] " P2 is open

proof end;

theorem Th12: :: BORSUK_2:12

for S1, S2, T1, T2 being non empty TopSpace
for f being continuous Function of S1,T1
for g being continuous Function of S2,T2 holds [:f,g:] is continuous

proof end;

registration

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

end;

registration

let T1, T2 be non empty discerning TopSpace;
cluster [:T1,T2:] -> discerning ;
coherence

proof end;

end;

theorem :: BORSUK_2:13

canceled;

theorem Th14: :: BORSUK_2:14

for T1, T2 being non empty TopSpace st T1 is_T1 & T2 is_T1 holds
[:T1,T2:] is_T1

proof end;

registration

let T1, T2 be non empty being_T1 TopSpace;
cluster [:T1,T2:] -> being_T1 ;
coherence by Th14;

end;

Lm5: for T1, T2 being non empty TopSpace st T1 is_T2 & T2 is_T2 holds
[:T1,T2:] is_T2

proof end;

registration

let T1, T2 be non empty being_T2 TopSpace;
cluster [:T1,T2:] -> discerning being_T2 ;
coherence by Lm5;

end;

registration

cluster I[01] -> compact being_T2 ;
coherence

proof end;

end;

definition

let T be non empty TopStruct ;
let a, b be Point of T;
let P, Q be Path of a,b;
pred P,Q are_homotopic means :: BORSUK_2:def 7
ex f being Function of [:I[01] ,I[01] :],T st
( f is continuous & ( for s being Point of I[01] holds
( f . s,0 = P . s & f . s,1 = Q . s & ( for t being Point of I[01] holds
( f . 0,t = a & f . 1,t = b ) ) ) ) );
symmetry

proof end;

end;

:: deftheorem defines are_homotopic BORSUK_2:def 7 :

theorem Th15: :: BORSUK_2:15

for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b st a,b are_connected holds
P,P are_homotopic

proof end;

definition

let T be non empty arcwise_connected TopSpace;
let a, b be Point of T;
let P, Q be Path of a,b;
:: original: are_homotopic
redefine pred P,Q are_homotopic ;
reflexivity

proof end;

end;