begin
scheme
ExFunc3CondD{
F1()
-> non
empty set ,
P1[
set ],
P2[
set ],
P3[
set ],
F2(
set )
-> set ,
F3(
set )
-> set ,
F4(
set )
-> set } :
ex
f being
Function st
(
dom f = F1() & ( for
c being
Element of
F1() holds
( (
P1[
c] implies
f . c = F2(
c) ) & (
P2[
c] implies
f . c = F3(
c) ) & (
P3[
c] implies
f . c = F4(
c) ) ) ) )
provided
A1:
for
c being
Element of
F1() holds
( (
P1[
c] implies not
P2[
c] ) & (
P1[
c] implies not
P3[
c] ) & (
P2[
c] implies not
P3[
c] ) )
and A2:
for
c being
Element of
F1() holds
(
P1[
c] or
P2[
c] or
P3[
c] )
begin
begin
begin
theorem Th28:
for
A,
B being
Subset of
[:I[01],I[01]:] st
A = [:[.0,(1 / 2).],[.0,1.]:] &
B = [:[.(1 / 2),1.],[.0,1.]:] holds
([#] ([:I[01],I[01]:] | A)) \/ ([#] ([:I[01],I[01]:] | B)) = [#] [:I[01],I[01]:]
theorem Th29:
for
A,
B being
Subset of
[:I[01],I[01]:] st
A = [:[.0,(1 / 2).],[.0,1.]:] &
B = [:[.(1 / 2),1.],[.0,1.]:] holds
([#] ([:I[01],I[01]:] | A)) /\ ([#] ([:I[01],I[01]:] | B)) = [:{(1 / 2)},[.0,1.]:]
begin
begin
definition
let a,
b,
c,
d be
real number ;
func L[01] (
a,
b,
c,
d)
-> Function of
(Closed-Interval-TSpace (a,b)),
(Closed-Interval-TSpace (c,d)) equals
(L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))));
correctness
coherence
(L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) is Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d));
;
end;
::
deftheorem defines
L[01] BORSUK_6:def 1 :
for a, b, c, d being real number holds L[01] (a,b,c,d) = (L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))));
begin
begin
begin
theorem Th52:
for
T being non
empty TopSpace for
a,
b,
c,
d being
Point of
T for
P being
Path of
a,
b for
Q being
Path of
b,
c for
R being
Path of
c,
d st
a,
b are_connected &
b,
c are_connected &
c,
d are_connected holds
RePar (
((P + Q) + R),
3RP)
= P + (Q + R)
begin
Lm1:
for x, y being Point of I[01] holds [x,y] in the carrier of [:I[01],I[01]:]
;
begin
theorem Th73:
for
T being non
empty TopSpace for
a,
b,
c,
d being
Point of
T for
P being
Path of
a,
b for
Q being
Path of
b,
c for
R being
Path of
c,
d st
a,
b are_connected &
b,
c are_connected &
c,
d are_connected holds
(P + Q) + R,
P + (Q + R) are_homotopic
theorem Th75:
for
T being non
empty TopSpace for
a,
b,
c being
Point of
T for
P1,
P2 being
Path of
a,
b for
Q1,
Q2 being
Path of
b,
c st
a,
b are_connected &
b,
c are_connected &
P1,
P2 are_homotopic &
Q1,
Q2 are_homotopic holds
P1 + Q1,
P2 + Q2 are_homotopic
definition
let T be non
empty TopSpace;
let a,
b be
Point of
T;
let P,
Q be
Path of
a,
b;
assume A1:
P,
Q are_homotopic
;
existence
ex b1 being Function of [:I[01],I[01]:],T st
( b1 is continuous & ( for t being Point of I[01] holds
( b1 . (t,0) = P . t & b1 . (t,1) = Q . t & b1 . (0,t) = a & b1 . (1,t) = b ) ) )
by A1, BORSUK_2:def 7;
end;
::
deftheorem defines
Homotopy BORSUK_6:def 11 :
for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b st P,Q are_homotopic holds
for b6 being Function of [:I[01],I[01]:],T holds
( b6 is Homotopy of P,Q iff ( b6 is continuous & ( for t being Point of I[01] holds
( b6 . (t,0) = P . t & b6 . (t,1) = Q . t & b6 . (0,t) = a & b6 . (1,t) = b ) ) ) );