:: by Artur Korni{\l}owicz

::

:: Received April 20, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

registration

let n be Nat;

existence

ex b_{1} being Subset of (TOP-REAL n) st

( not b_{1} is empty & b_{1} is convex )

end;
existence

ex b

( not b

proof end;

:: deftheorem Def1 defines convex TOPALG_2:def 1 :

for n being Element of NAT

for T being SubSpace of TOP-REAL n holds

( T is convex iff [#] T is convex Subset of (TOP-REAL n) );

for n being Element of NAT

for T being SubSpace of TOP-REAL n holds

( T is convex iff [#] T is convex Subset of (TOP-REAL n) );

registration

let n be Element of NAT ;

coherence

for b_{1} being non empty SubSpace of TOP-REAL n st b_{1} is convex holds

b_{1} is pathwise_connected

end;
coherence

for b

b

proof end;

registration

let n be Element of NAT ;

existence

ex b_{1} being SubSpace of TOP-REAL n st

( b_{1} is strict & not b_{1} is empty & b_{1} is convex )

end;
existence

ex b

( b

proof end;

theorem :: TOPALG_2:1

for X being non empty TopSpace

for Y being non empty SubSpace of X

for x1, x2 being Point of X

for y1, y2 being Point of Y

for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds

f is Path of x1,x2

for Y being non empty SubSpace of X

for x1, x2 being Point of X

for y1, y2 being Point of Y

for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds

f is Path of x1,x2

proof end;

set I = the carrier of I[01];

Lm1: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:]

by BORSUK_1:def 2;

Lm2: the carrier of [:(TOP-REAL 1),I[01]:] = [: the carrier of (TOP-REAL 1), the carrier of I[01]:]

by BORSUK_1:def 2;

Lm3: the carrier of [:R^1,I[01]:] = [: the carrier of R^1, the carrier of I[01]:]

by BORSUK_1:def 2;

Lm4: dom (id I[01]) = the carrier of I[01]

by FUNCT_2:def 1;

definition

let n be Element of NAT ;

let T be non empty convex SubSpace of TOP-REAL n;

let P, Q be Function of I[01],T;

ex b_{1} being Function of [:I[01],I[01]:],T st

for s, t being Element of I[01]

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

b_{1} . (s,t) = ((1 - t) * a1) + (t * b1)

for b_{1}, b_{2} being Function of [:I[01],I[01]:],T st ( for s, t being Element of I[01]

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

b_{1} . (s,t) = ((1 - t) * a1) + (t * b1) ) & ( for s, t being Element of I[01]

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

b_{2} . (s,t) = ((1 - t) * a1) + (t * b1) ) holds

b_{1} = b_{2}

end;
let T be non empty convex SubSpace of TOP-REAL n;

let P, Q be Function of I[01],T;

func ConvexHomotopy (P,Q) -> Function of [:I[01],I[01]:],T means :Def2: :: TOPALG_2:def 2

for s, t being Element of I[01]

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

it . (s,t) = ((1 - t) * a1) + (t * b1);

existence for s, t being Element of I[01]

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

it . (s,t) = ((1 - t) * a1) + (t * b1);

ex b

for s, t being Element of I[01]

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

b

proof end;

uniqueness for b

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

b

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

b

b

proof end;

:: deftheorem Def2 defines ConvexHomotopy TOPALG_2:def 2 :

for n being Element of NAT

for T being non empty convex SubSpace of TOP-REAL n

for P, Q being Function of I[01],T

for b_{5} being Function of [:I[01],I[01]:],T holds

( b_{5} = ConvexHomotopy (P,Q) iff for s, t being Element of I[01]

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

b_{5} . (s,t) = ((1 - t) * a1) + (t * b1) );

for n being Element of NAT

for T being non empty convex SubSpace of TOP-REAL n

for P, Q being Function of I[01],T

for b

( b

for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds

b

Lm5: for n being Element of NAT

for T being non empty convex SubSpace of TOP-REAL n

for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous

proof end;

Lm6: for n being Element of NAT

for T being non empty convex SubSpace of TOP-REAL n

for a, b being Point of T

for P, Q being Path of a,b

for s being Point of I[01] holds

( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds

( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )

proof end;

theorem Th2: :: TOPALG_2:2

for n being Element of NAT

for T being non empty convex SubSpace of TOP-REAL n

for a, b being Point of T

for P, Q being Path of a,b holds P,Q are_homotopic

for T being non empty convex SubSpace of TOP-REAL n

for a, b being Point of T

for P, Q being Path of a,b holds P,Q are_homotopic

proof end;

registration

let n be Element of NAT ;

let T be non empty convex SubSpace of TOP-REAL n;

let a, b be Point of T;

let P, Q be Path of a,b;

coherence

for b_{1} being Homotopy of P,Q holds b_{1} is continuous

end;
let T be non empty convex SubSpace of TOP-REAL n;

let a, b be Point of T;

let P, Q be Path of a,b;

coherence

for b

proof end;

theorem Th3: :: TOPALG_2:3

for n being Element of NAT

for T being non empty convex SubSpace of TOP-REAL n

for a being Point of T

for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}

for T being non empty convex SubSpace of TOP-REAL n

for a being Point of T

for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}

proof end;

registration

let n be Element of NAT ;

let T be non empty convex SubSpace of TOP-REAL n;

let a be Point of T;

coherence

pi_1 (T,a) is trivial

end;
let T be non empty convex SubSpace of TOP-REAL n;

let a be Point of T;

coherence

pi_1 (T,a) is trivial

proof end;

theorem :: TOPALG_2:5

for a, b being Real st a <= b holds

[.a,b.] = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) }

[.a,b.] = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) }

proof end;

theorem Th6: :: TOPALG_2:6

for F being Function of [:R^1,I[01]:],R^1 st ( for x being Point of R^1

for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds

F is continuous

for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds

F is continuous

proof end;

theorem Th7: :: TOPALG_2:7

for F being Function of [:R^1,I[01]:],R^1 st ( for x being Point of R^1

for i being Point of I[01] holds F . (x,i) = i * x ) holds

F is continuous

for i being Point of I[01] holds F . (x,i) = i * x ) holds

F is continuous

proof end;

registration
end;

registration

let T be real-membered TopStruct ;

existence

ex b_{1} being Subset of T st b_{1} is interval

end;
existence

ex b

proof end;

:: deftheorem Def3 defines interval TOPALG_2:def 3 :

for T being real-membered TopStruct holds

( T is interval iff [#] T is interval );

for T being real-membered TopStruct holds

( T is interval iff [#] T is interval );

Lm7: for T being SubSpace of R^1 st T = R^1 holds

T is interval

by TOPMETR:17;

registration

existence

ex b_{1} being SubSpace of R^1 st

( b_{1} is strict & not b_{1} is empty & b_{1} is interval )

end;
ex b

( b

proof end;

definition

:: original: R^1

redefine func R^1 -> interval SubSpace of R^1 ;

coherence

R^1 is interval SubSpace of R^1 by Lm7, TSEP_1:2;

end;
redefine func R^1 -> interval SubSpace of R^1 ;

coherence

R^1 is interval SubSpace of R^1 by Lm7, TSEP_1:2;

theorem Th8: :: TOPALG_2:8

for T being non empty interval SubSpace of R^1

for a, b being Point of T holds [.a,b.] c= the carrier of T

for a, b being Point of T holds [.a,b.] c= the carrier of T

proof end;

registration

coherence

for b_{1} being non empty SubSpace of R^1 st b_{1} is interval holds

b_{1} is pathwise_connected

end;
for b

b

proof end;

definition

let T be non empty interval SubSpace of R^1 ;

let P, Q be Function of I[01],T;

ex b_{1} being Function of [:I[01],I[01]:],T st

for s, t being Element of I[01] holds b_{1} . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))

for b_{1}, b_{2} being Function of [:I[01],I[01]:],T st ( for s, t being Element of I[01] holds b_{1} . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b_{2} . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds

b_{1} = b_{2}

end;
let P, Q be Function of I[01],T;

func R1Homotopy (P,Q) -> Function of [:I[01],I[01]:],T means :Def4: :: TOPALG_2:def 4

for s, t being Element of I[01] holds it . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s));

existence for s, t being Element of I[01] holds it . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s));

ex b

for s, t being Element of I[01] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines R1Homotopy TOPALG_2:def 4 :

for T being non empty interval SubSpace of R^1

for P, Q being Function of I[01],T

for b_{4} being Function of [:I[01],I[01]:],T holds

( b_{4} = R1Homotopy (P,Q) iff for s, t being Element of I[01] holds b_{4} . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) );

for T being non empty interval SubSpace of R^1

for P, Q being Function of I[01],T

for b

( b

Lm8: for T being non empty interval SubSpace of R^1

for P, Q being continuous Function of I[01],T holds R1Homotopy (P,Q) is continuous

proof end;

Lm9: for T being non empty interval SubSpace of R^1

for a, b being Point of T

for P, Q being Path of a,b

for s being Point of I[01] holds

( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds

( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) )

proof end;

theorem Th12: :: TOPALG_2:12

for T being non empty interval SubSpace of R^1

for a, b being Point of T

for P, Q being Path of a,b holds P,Q are_homotopic

for a, b being Point of T

for P, Q being Path of a,b holds P,Q are_homotopic

proof end;

registration

let T be non empty interval SubSpace of R^1 ;

let a, b be Point of T;

let P, Q be Path of a,b;

coherence

for b_{1} being Homotopy of P,Q holds b_{1} is continuous

end;
let a, b be Point of T;

let P, Q be Path of a,b;

coherence

for b

proof end;

theorem Th13: :: TOPALG_2:13

for T being non empty interval SubSpace of R^1

for a being Point of T

for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}

for a being Point of T

for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}

proof end;

registration

let T be non empty interval SubSpace of R^1 ;

let a be Point of T;

coherence

pi_1 (T,a) is trivial

end;
let a be Point of T;

coherence

pi_1 (T,a) is trivial

proof end;

theorem :: TOPALG_2:14

for a, b being Real st a <= b holds

for x, y being Point of (Closed-Interval-TSpace (a,b))

for P, Q being Path of x,y holds P,Q are_homotopic

for x, y being Point of (Closed-Interval-TSpace (a,b))

for P, Q being Path of x,y holds P,Q are_homotopic

proof end;

theorem :: TOPALG_2:15

for a, b being Real st a <= b holds

for x being Point of (Closed-Interval-TSpace (a,b))

for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}

for x being Point of (Closed-Interval-TSpace (a,b))

for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))}

proof end;

theorem :: TOPALG_2:16

theorem :: TOPALG_2:17

registration

let n be Element of NAT ;

let T be non empty convex SubSpace of TOP-REAL n;

let P, Q be continuous Function of I[01],T;

coherence

ConvexHomotopy (P,Q) is continuous by Lm5;

end;
let T be non empty convex SubSpace of TOP-REAL n;

let P, Q be continuous Function of I[01],T;

coherence

ConvexHomotopy (P,Q) is continuous by Lm5;

theorem :: TOPALG_2:18

for n being Element of NAT

for T being non empty convex SubSpace of TOP-REAL n

for a, b being Point of T

for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q

for T being non empty convex SubSpace of TOP-REAL n

for a, b being Point of T

for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q

proof end;

registration

let T be non empty interval SubSpace of R^1 ;

let P, Q be continuous Function of I[01],T;

coherence

R1Homotopy (P,Q) is continuous by Lm8;

end;
let P, Q be continuous Function of I[01],T;

coherence

R1Homotopy (P,Q) is continuous by Lm8;

theorem :: TOPALG_2:19

for T being non empty interval SubSpace of R^1

for a, b being Point of T

for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q

for a, b being Point of T

for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q

proof end;