let n be Element of NAT ; :: thesis: for w1, w2, w3 being Point of (TOP-REAL n)
for P being non empty Subset of (TOP-REAL n)
for h1, h2 being Function of I[01] ,((TOP-REAL n) | P) st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01] ,((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
let w1, w2, w3 be Point of (TOP-REAL n); :: thesis: for P being non empty Subset of (TOP-REAL n)
for h1, h2 being Function of I[01] ,((TOP-REAL n) | P) st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01] ,((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
let P be non empty Subset of (TOP-REAL n); :: thesis: for h1, h2 being Function of I[01] ,((TOP-REAL n) | P) st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01] ,((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
let h1, h2 be Function of I[01] ,((TOP-REAL n) | P); :: thesis: ( h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 implies ex h3 being Function of I[01] ,((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 ) )
assume A1:
( h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 )
; :: thesis: ex h3 being Function of I[01] ,((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
A2:
0 in [.0 ,1.]
by XXREAL_1:1;
1 in [.0 ,1.]
by XXREAL_1:1;
then reconsider p1 = w1, p2 = w2, p3 = w3 as Point of ((TOP-REAL n) | P) by A1, A2, BORSUK_1:83, FUNCT_2:7;
p1,p2 are_connected
by A1, BORSUK_2:def 1;
then reconsider P1 = h1 as Path of p1,p2 by A1, BORSUK_2:def 2;
p2,p3 are_connected
by A1, BORSUK_2:def 1;
then reconsider P2 = h2 as Path of p2,p3 by A1, BORSUK_2:def 2;
ex P0 being Path of p1,p3 st
( P0 is continuous & P0 . 0 = p1 & P0 . 1 = p3 & ( for t being Point of I[01]
for t' being Real st t = t' holds
( ( 0 <= t' & t' <= 1 / 2 implies P0 . t = P1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies P0 . t = P2 . ((2 * t') - 1) ) ) ) )
proof
set e1 =
P[01] 0 ,
(1 / 2),
((#) 0 ,1),
(0 ,1 (#) );
set e2 =
P[01] (1 / 2),1,
((#) 0 ,1),
(0 ,1 (#) );
set E1 =
P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ));
set E2 =
P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ));
set f =
(P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )));
A3:
dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) =
the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by FUNCT_2:def 1
.=
[.0 ,(1 / 2).]
by TOPMETR:25
;
A4:
dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) =
the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by FUNCT_2:def 1
.=
[.(1 / 2),1.]
by TOPMETR:25
;
A5:
(
dom P1 = the
carrier of
I[01] &
dom P2 = the
carrier of
I[01] )
by FUNCT_2:def 1;
then A6:
rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) c= dom P1
by TOPMETR:27;
rng (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) c= the
carrier of
(Closed-Interval-TSpace 0 ,1)
;
then A7:
dom (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) = dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))
by A5, RELAT_1:46, TOPMETR:27;
A8:
dom ((P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) =
(dom (P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )))) \/ (dom (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))))
by FUNCT_4:def 1
.=
[.0 ,(1 / 2).] \/ [.(1 / 2),1.]
by A3, A4, A6, A7, RELAT_1:46
.=
the
carrier of
I[01]
by BORSUK_1:83, XXREAL_1:174
;
A9:
for
t' being
Real st
0 <= t' &
t' <= 1
/ 2 holds
(P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = P1 . (2 * t')
proof
let t' be
Real;
:: thesis: ( 0 <= t' & t' <= 1 / 2 implies (P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = P1 . (2 * t') )
assume A10:
(
0 <= t' &
t' <= 1
/ 2 )
;
:: thesis: (P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = P1 . (2 * t')
dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by FUNCT_2:def 1;
then dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) =
[.0 ,(1 / 2).]
by TOPMETR:25
.=
{ r where r is Real : ( 0 <= r & r <= 1 / 2 ) }
by RCOMP_1:def 1
;
then A11:
t' in dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))
by A10;
then reconsider s =
t' as
Point of
(Closed-Interval-TSpace 0 ,(1 / 2)) ;
reconsider r1 =
(#) 0 ,1,
r2 =
0 ,1
(#) as
Real by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8;
(P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . s =
(((r2 - r1) / ((1 / 2) - 0 )) * t') + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0 ))
by TREAL_1:14
.=
2
* t'
by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8
;
hence
(P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = P1 . (2 * t')
by A11, FUNCT_1:23;
:: thesis: verum
end;
not
0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
then
not
0 in dom (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
by A4, A7, RCOMP_1:def 1;
then A12:
((P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) . 0 =
(P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . 0
by FUNCT_4:12
.=
P1 . (2 * 0 )
by A9
.=
p1
by A1
;
rng ((P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) c= (rng (P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )))) \/ (rng (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))))
by FUNCT_4:18;
then
rng ((P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) c= the
carrier of
((TOP-REAL n) | P)
by XBOOLE_1:1;
then reconsider f =
(P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) as
Function of
I[01] ,
((TOP-REAL n) | P) by A8, FUNCT_2:def 1, RELSET_1:11;
reconsider T1 =
Closed-Interval-TSpace 0 ,
(1 / 2),
T2 =
Closed-Interval-TSpace (1 / 2),1 as
SubSpace of
I[01] by TOPMETR:27, TREAL_1:6;
A13:
P[01] 0 ,
(1 / 2),
((#) 0 ,1),
(0 ,1 (#) ) is
continuous
by TREAL_1:15;
A14:
P[01] (1 / 2),1,
((#) 0 ,1),
(0 ,1 (#) ) is
continuous
by TREAL_1:15;
reconsider ff =
P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) as
Function of
T1,
((TOP-REAL n) | P) by TOPMETR:27;
A15:
P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) is
Function of the
carrier of
(Closed-Interval-TSpace (1 / 2),1),the
carrier of
((TOP-REAL n) | P)
by TOPMETR:27;
reconsider gg =
P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) as
Function of
T2,
((TOP-REAL n) | P) by TOPMETR:27;
1
/ 2
in { r where r is Real : ( 0 <= r & r <= 1 ) }
;
then reconsider pol = 1
/ 2 as
Point of
I[01] by BORSUK_1:83, RCOMP_1:def 1;
A16:
(
ff is
continuous &
gg is
continuous )
by A1, A13, A14, TOPMETR:27;
A17:
[#] T1 = [.0 ,(1 / 2).]
by TOPMETR:25;
A18:
[#] T2 = [.(1 / 2),1.]
by TOPMETR:25;
then A19:
([#] T1) \/ ([#] T2) = [#] I[01]
by A17, BORSUK_1:83, XXREAL_1:174;
A20:
for
t' being
Real st 1
/ 2
<= t' &
t' <= 1 holds
(P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = P2 . ((2 * t') - 1)
proof
let t' be
Real;
:: thesis: ( 1 / 2 <= t' & t' <= 1 implies (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = P2 . ((2 * t') - 1) )
assume A21:
( 1
/ 2
<= t' &
t' <= 1 )
;
:: thesis: (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = P2 . ((2 * t') - 1)
dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) = the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by FUNCT_2:def 1;
then dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) =
[.(1 / 2),1.]
by TOPMETR:25
.=
{ r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
by RCOMP_1:def 1
;
then A22:
t' in dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))
by A21;
then reconsider s =
t' as
Point of
(Closed-Interval-TSpace (1 / 2),1) ;
reconsider r1 =
(#) 0 ,1,
r2 =
0 ,1
(#) as
Real by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8;
(P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) . s =
(((r2 - r1) / (1 - (1 / 2))) * t') + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2)))
by TREAL_1:14
.=
(2 * t') - 1
by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8
;
hence
(P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = P2 . ((2 * t') - 1)
by A22, FUNCT_1:23;
:: thesis: verum
end;
A23:
ff . (1 / 2) =
P2 . ((2 * (1 / 2)) - 1)
by A1, A9
.=
gg . pol
by A20
;
A24:
([#] T1) /\ ([#] T2) = {pol}
by A17, A18, XXREAL_1:418;
(
T1 is
compact &
T2 is
compact &
I[01] is
T_2 &
ff . pol = gg . pol )
by A23, HEINE:11;
then reconsider f =
f as
continuous Function of
I[01] ,
((TOP-REAL n) | P) by A16, A19, A24, COMPTS_1:29;
1
in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
;
then
1
in dom (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
by A4, A7, RCOMP_1:def 1;
then A25:
f . 1 =
(P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . 1
by FUNCT_4:14
.=
P2 . ((2 * 1) - 1)
by A20
.=
p3
by A1
;
then
p1,
p3 are_connected
by A12, BORSUK_2:def 1;
then reconsider f =
f as
Path of
p1,
p3 by A12, A25, BORSUK_2:def 2;
for
t being
Point of
I[01] for
t' being
Real st
t = t' holds
( (
0 <= t' &
t' <= 1
/ 2 implies
f . t = P1 . (2 * t') ) & ( 1
/ 2
<= t' &
t' <= 1 implies
f . t = P2 . ((2 * t') - 1) ) )
proof
let t be
Point of
I[01] ;
:: thesis: for t' being Real st t = t' holds
( ( 0 <= t' & t' <= 1 / 2 implies f . t = P1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies f . t = P2 . ((2 * t') - 1) ) )let t' be
Real;
:: thesis: ( t = t' implies ( ( 0 <= t' & t' <= 1 / 2 implies f . t = P1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies f . t = P2 . ((2 * t') - 1) ) ) )
assume A26:
t = t'
;
:: thesis: ( ( 0 <= t' & t' <= 1 / 2 implies f . t = P1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies f . t = P2 . ((2 * t') - 1) ) )
thus
(
0 <= t' &
t' <= 1
/ 2 implies
f . t = P1 . (2 * t') )
:: thesis: ( 1 / 2 <= t' & t' <= 1 implies f . t = P2 . ((2 * t') - 1) )proof
assume A27:
(
0 <= t' &
t' <= 1
/ 2 )
;
:: thesis: f . t = P1 . (2 * t')
then
t' in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) }
;
then A28:
t' in [.0 ,(1 / 2).]
by RCOMP_1:def 1;
per cases
( t' <> 1 / 2 or t' = 1 / 2 )
;
suppose A29:
t' <> 1
/ 2
;
:: thesis: f . t = P1 . (2 * t')
not
t' in dom (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
proof
assume
t' in dom (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
;
:: thesis: contradiction
then
t' in [.0 ,(1 / 2).] /\ [.(1 / 2),1.]
by A4, A7, A28, XBOOLE_0:def 4;
then
t' in {(1 / 2)}
by XXREAL_1:418;
hence
contradiction
by A29, TARSKI:def 1;
:: thesis: verum
end; then f . t =
(P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t
by A26, FUNCT_4:12
.=
P1 . (2 * t')
by A9, A26, A27
;
hence
f . t = P1 . (2 * t')
;
:: thesis: verum suppose A30:
t' = 1
/ 2
;
:: thesis: f . t = P1 . (2 * t')
1
/ 2
in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
;
then
1
/ 2
in [.(1 / 2),1.]
by RCOMP_1:def 1;
then
1
/ 2
in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by TOPMETR:25;
then
t in dom (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
by A15, A26, A30, FUNCT_2:def 1;
then f . t =
(P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . (1 / 2)
by A26, A30, FUNCT_4:14
.=
P1 . (2 * t')
by A9, A23, A30
;
hence
f . t = P1 . (2 * t')
;
:: thesis: verum
end;
thus
( 1
/ 2
<= t' &
t' <= 1 implies
f . t = P2 . ((2 * t') - 1) )
:: thesis: verumproof
assume A31:
( 1
/ 2
<= t' &
t' <= 1 )
;
:: thesis: f . t = P2 . ((2 * t') - 1)
then
t' in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
;
then
t' in [.(1 / 2),1.]
by RCOMP_1:def 1;
then f . t =
(P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t
by A4, A7, A26, FUNCT_4:14
.=
P2 . ((2 * t') - 1)
by A20, A26, A31
;
hence
f . t = P2 . ((2 * t') - 1)
;
:: thesis: verum
end;
end;
hence
ex
P0 being
Path of
p1,
p3 st
(
P0 is
continuous &
P0 . 0 = p1 &
P0 . 1
= p3 & ( for
t being
Point of
I[01] for
t' being
Real st
t = t' holds
( (
0 <= t' &
t' <= 1
/ 2 implies
P0 . t = P1 . (2 * t') ) & ( 1
/ 2
<= t' &
t' <= 1 implies
P0 . t = P2 . ((2 * t') - 1) ) ) ) )
by A12, A25;
:: thesis: verum
end;
hence
ex h3 being Function of I[01] ,((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
; :: thesis: verum