:: by Marco Riccardi and Artur Korni{\l}owicz

::

:: Received November 3, 2011

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

registration

let S be TopSpace;

let T be non empty TopSpace;

coherence

for b_{1} being Function of S,T st b_{1} is constant holds

b_{1} is continuous ;

end;
let T be non empty TopSpace;

cluster Function-like constant quasi_total -> continuous for Element of bool [: the carrier of S, the carrier of T:];

correctness coherence

for b

b

proof end;

theorem Th2: :: TOPALG_6:2

for r1, r2, r3, r4, r5, r6 being Real st r1 < r2 & r3 <= r4 & r5 < r6 holds

(L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2)) = L[01] (r5,r6,r3,r4)

(L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2)) = L[01] (r5,r6,r3,r4)

proof end;

registration

let n be positive Nat;

correctness

coherence

not TOP-REAL n is finite ;

coherence

for b_{1} being non empty TopSpace st b_{1} is n -locally_euclidean holds

b_{1} is infinite ;

end;
correctness

coherence

not TOP-REAL n is finite ;

proof end;

correctness coherence

for b

b

proof end;

theorem Th3: :: TOPALG_6:3

for n being Nat

for p being Point of (TOP-REAL n) st p in Sphere ((0. (TOP-REAL n)),1) holds

- p in (Sphere ((0. (TOP-REAL n)),1)) \ {p}

for p being Point of (TOP-REAL n) st p in Sphere ((0. (TOP-REAL n)),1) holds

- p in (Sphere ((0. (TOP-REAL n)),1)) \ {p}

proof end;

theorem Th4: :: TOPALG_6:4

for T being non empty TopStruct

for t1, t2 being Point of T

for p being Path of t1,t2 holds

( inf (dom p) = 0 & sup (dom p) = 1 )

for t1, t2 being Point of T

for p being Path of t1,t2 holds

( inf (dom p) = 0 & sup (dom p) = 1 )

proof end;

theorem Th5: :: TOPALG_6:5

for T being non empty TopSpace

for t being Point of T

for C1, C2 being constant Loop of t holds C1,C2 are_homotopic

for t being Point of T

for C1, C2 being constant Loop of t holds C1,C2 are_homotopic

proof end;

theorem Th6: :: TOPALG_6:6

for T being non empty TopSpace

for S being non empty SubSpace of T

for t1, t2 being Point of T

for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

for S being non empty SubSpace of T

for t1, t2 being Point of T

for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

proof end;

theorem :: TOPALG_6:7

for T being non empty TopSpace

for S being non empty SubSpace of T

for t1, t2 being Point of T

for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) holds

Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)

for S being non empty SubSpace of T

for t1, t2 being Point of T

for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) holds

Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)

proof end;

theorem Th8: :: TOPALG_6:8

for T being non empty trivial TopSpace

for t being Point of T

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

for t being Point of T

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

proof end;

theorem Th9: :: TOPALG_6:9

for n being Nat

for p being Point of (TOP-REAL n)

for S being Subset of (TOP-REAL n) st n >= 2 & S = ([#] (TOP-REAL n)) \ {p} holds

(TOP-REAL n) | S is pathwise_connected

for p being Point of (TOP-REAL n)

for S being Subset of (TOP-REAL n) st n >= 2 & S = ([#] (TOP-REAL n)) \ {p} holds

(TOP-REAL n) | S is pathwise_connected

proof end;

theorem Th10: :: TOPALG_6:10

for T being non empty TopSpace

for t being Point of T

for n being Nat

for S being non empty Subset of T st n >= 2 & S = ([#] T) \ {t} & TOP-REAL n,T are_homeomorphic holds

T | S is pathwise_connected

for t being Point of T

for n being Nat

for S being non empty Subset of T st n >= 2 & S = ([#] T) \ {t} & TOP-REAL n,T are_homeomorphic holds

T | S is pathwise_connected

proof end;

registration

let n be Element of NAT ;

let p, q be Point of (TOP-REAL n);

correctness

coherence

TPlane (p,q) is convex ;

end;
let p, q be Point of (TOP-REAL n);

correctness

coherence

TPlane (p,q) is convex ;

proof end;

definition

let T be non empty TopSpace;

end;
attr T is having_trivial_Fundamental_Group means :Def1: :: TOPALG_6:def 1

for t being Point of T holds pi_1 (T,t) is trivial ;

for t being Point of T holds pi_1 (T,t) is trivial ;

:: deftheorem Def1 defines having_trivial_Fundamental_Group TOPALG_6:def 1 :

for T being non empty TopSpace holds

( T is having_trivial_Fundamental_Group iff for t being Point of T holds pi_1 (T,t) is trivial );

for T being non empty TopSpace holds

( T is having_trivial_Fundamental_Group iff for t being Point of T holds pi_1 (T,t) is trivial );

definition

let T be non empty TopSpace;

end;
attr T is simply_connected means :: TOPALG_6:def 2

( T is having_trivial_Fundamental_Group & T is pathwise_connected );

( T is having_trivial_Fundamental_Group & T is pathwise_connected );

:: deftheorem defines simply_connected TOPALG_6:def 2 :

for T being non empty TopSpace holds

( T is simply_connected iff ( T is having_trivial_Fundamental_Group & T is pathwise_connected ) );

for T being non empty TopSpace holds

( T is simply_connected iff ( T is having_trivial_Fundamental_Group & T is pathwise_connected ) );

registration

for b_{1} being non empty TopSpace st b_{1} is simply_connected holds

( b_{1} is having_trivial_Fundamental_Group & b_{1} is pathwise_connected )
;

for b_{1} being non empty TopSpace st b_{1} is having_trivial_Fundamental_Group & b_{1} is pathwise_connected holds

b_{1} is simply_connected
;

end;

cluster non empty TopSpace-like simply_connected -> non empty pathwise_connected having_trivial_Fundamental_Group for TopStruct ;

coherence for b

( b

cluster non empty TopSpace-like pathwise_connected having_trivial_Fundamental_Group -> non empty simply_connected for TopStruct ;

coherence for b

b

theorem Th11: :: TOPALG_6:11

for T being non empty TopSpace st T is having_trivial_Fundamental_Group holds

for t being Point of T

for P, Q being Loop of t holds P,Q are_homotopic

for t being Point of T

for P, Q being Loop of t holds P,Q are_homotopic

proof end;

registration

for b_{1} being non empty TopSpace st b_{1} is trivial holds

b_{1} is having_trivial_Fundamental_Group
end;

cluster non empty trivial TopSpace-like -> non empty having_trivial_Fundamental_Group for TopStruct ;

coherence for b

b

proof end;

theorem Th12: :: TOPALG_6:12

for T being non empty TopSpace holds

( T is simply_connected iff for t1, t2 being Point of T holds

( t1,t2 are_connected & ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) ) )

( T is simply_connected iff for t1, t2 being Point of T holds

( t1,t2 are_connected & ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) ) )

proof end;

registration

let T be non empty having_trivial_Fundamental_Group TopSpace;

let t be Point of T;

coherence

pi_1 (T,t) is trivial by Def1;

end;
let t be Point of T;

coherence

pi_1 (T,t) is trivial by Def1;

theorem Th13: :: TOPALG_6:13

for S, T being non empty TopSpace st S,T are_homeomorphic & S is having_trivial_Fundamental_Group holds

T is having_trivial_Fundamental_Group

T is having_trivial_Fundamental_Group

proof end;

theorem Th14: :: TOPALG_6:14

for S, T being non empty TopSpace st S,T are_homeomorphic & S is simply_connected holds

T is simply_connected by Th13, TOPALG_3:9;

T is simply_connected by Th13, TOPALG_3:9;

theorem Th15: :: TOPALG_6:15

for T being non empty having_trivial_Fundamental_Group TopSpace

for t being Point of T

for P1, P2 being Loop of t holds P1,P2 are_homotopic

for t being Point of T

for P1, P2 being Loop of t holds P1,P2 are_homotopic

proof end;

definition

let T be non empty TopSpace;

let t be Point of T;

let l be Loop of t;

end;
let t be Point of T;

let l be Loop of t;

attr l is nullhomotopic means :: TOPALG_6:def 3

ex c being constant Loop of t st l,c are_homotopic ;

ex c being constant Loop of t st l,c are_homotopic ;

:: deftheorem defines nullhomotopic TOPALG_6:def 3 :

for T being non empty TopSpace

for t being Point of T

for l being Loop of t holds

( l is nullhomotopic iff ex c being constant Loop of t st l,c are_homotopic );

for T being non empty TopSpace

for t being Point of T

for l being Loop of t holds

( l is nullhomotopic iff ex c being constant Loop of t st l,c are_homotopic );

registration

let T be non empty TopSpace;

let t be Point of T;

coherence

for b_{1} being Loop of t st b_{1} is constant holds

b_{1} is nullhomotopic
by BORSUK_6:88;

end;
let t be Point of T;

coherence

for b

b

registration

let T be non empty TopSpace;

let t be Point of T;

ex b_{1} being Loop of t st b_{1} is constant

end;
let t be Point of T;

cluster Relation-like the carrier of I[01] -defined the carrier of T -valued non empty Function-like constant total quasi_total continuous for Path of t,t;

existence ex b

proof end;

theorem Th16: :: TOPALG_6:16

for T, U being non empty TopSpace

for t being Point of T

for f being Loop of t

for g being continuous Function of T,U st f is nullhomotopic holds

g * f is nullhomotopic

for t being Point of T

for f being Loop of t

for g being continuous Function of T,U st f is nullhomotopic holds

g * f is nullhomotopic

proof end;

registration

let T, U be non empty TopSpace;

let t be Point of T;

let f be nullhomotopic Loop of t;

let g be continuous Function of T,U;

coherence

for b_{1} being Loop of g . t st b_{1} = g * f holds

b_{1} is nullhomotopic
by Th16;

end;
let t be Point of T;

let f be nullhomotopic Loop of t;

let g be continuous Function of T,U;

coherence

for b

b

registration

let T be non empty having_trivial_Fundamental_Group TopSpace;

let t be Point of T;

coherence

for b_{1} being Loop of t holds b_{1} is nullhomotopic

end;
let t be Point of T;

coherence

for b

proof end;

theorem Th17: :: TOPALG_6:17

for T being non empty TopSpace st ( for t being Point of T

for f being Loop of t holds f is nullhomotopic ) holds

T is having_trivial_Fundamental_Group

for f being Loop of t holds f is nullhomotopic ) holds

T is having_trivial_Fundamental_Group

proof end;

registration

let n be Element of NAT ;

let p, q be Point of (TOP-REAL n);

correctness

coherence

TPlane (p,q) is having_trivial_Fundamental_Group ;

;

end;
let p, q be Point of (TOP-REAL n);

correctness

coherence

TPlane (p,q) is having_trivial_Fundamental_Group ;

;

theorem Th18: :: TOPALG_6:18

for T being non empty TopSpace

for t being Point of T

for S being non empty SubSpace of T

for s being Point of S

for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

for t being Point of T

for S being non empty SubSpace of T

for s being Point of S

for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

proof end;

:: deftheorem Def4 defines parametrized-curve TOPALG_6:def 4 :

for T being TopStruct

for f being PartFunc of R^1,T holds

( f is parametrized-curve iff ( dom f is interval Subset of REAL & ex S being SubSpace of R^1 ex g being Function of S,T st

( f = g & S = R^1 | (dom f) & g is continuous ) ) );

for T being TopStruct

for f being PartFunc of R^1,T holds

( f is parametrized-curve iff ( dom f is interval Subset of REAL & ex S being SubSpace of R^1 ex g being Function of S,T st

( f = g & S = R^1 | (dom f) & g is continuous ) ) );

Lm1: for T being TopStruct

for f being PartFunc of R^1,T st f = {} holds

f is parametrized-curve

proof end;

registration

let T be TopStruct ;

existence

ex b_{1} being PartFunc of R^1,T st b_{1} is parametrized-curve ;

end;
cluster Relation-like the carrier of R^1 -defined the carrier of T -valued Function-like parametrized-curve for Element of bool [: the carrier of R^1, the carrier of T:];

correctness existence

ex b

proof end;

theorem :: TOPALG_6:19

definition

let T be TopStruct ;

{ f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } is Subset of (PFuncs (REAL,([#] T)))

end;
func Curves T -> Subset of (PFuncs (REAL,([#] T))) equals :: TOPALG_6:def 5

{ f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } ;

coherence { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } ;

{ f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } is Subset of (PFuncs (REAL,([#] T)))

proof end;

:: deftheorem defines Curves TOPALG_6:def 5 :

for T being TopStruct holds Curves T = { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } ;

for T being TopStruct holds Curves T = { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } ;

registration
end;

theorem Th22: :: TOPALG_6:22

for T being TopStruct

for t1, t2 being Point of T

for p being Path of t1,t2 st t1,t2 are_connected holds

p is Curve of T

for t1, t2 being Point of T

for p being Path of t1,t2 st t1,t2 are_connected holds

p is Curve of T

proof end;

registration
end;

:: deftheorem Def6 defines with_first_point TOPALG_6:def 6 :

for T being TopStruct

for c being Curve of T holds

( c is with_first_point iff dom c is left_end );

for T being TopStruct

for c being Curve of T holds

( c is with_first_point iff dom c is left_end );

:: deftheorem Def7 defines with_last_point TOPALG_6:def 7 :

for T being TopStruct

for c being Curve of T holds

( c is with_last_point iff dom c is right_end );

for T being TopStruct

for c being Curve of T holds

( c is with_last_point iff dom c is right_end );

:: deftheorem defines with_endpoints TOPALG_6:def 8 :

for T being TopStruct

for c being Curve of T holds

( c is with_endpoints iff ( c is with_first_point & c is with_last_point ) );

for T being TopStruct

for c being Curve of T holds

( c is with_endpoints iff ( c is with_first_point & c is with_last_point ) );

registration

let T be TopStruct ;

correctness

coherence

for b_{1} being Curve of T st b_{1} is with_first_point & b_{1} is with_last_point holds

b_{1} is with_endpoints ;

;

correctness

coherence

for b_{1} being Curve of T st b_{1} is with_endpoints holds

( b_{1} is with_first_point & b_{1} is with_last_point );

;

end;
correctness

coherence

for b

b

;

correctness

coherence

for b

( b

;

registration

let T be non empty TopStruct ;

correctness

existence

ex b_{1} being Curve of T st b_{1} is with_endpoints ;

end;
correctness

existence

ex b

proof end;

registration

let T be non empty TopStruct ;

let c be with_first_point Curve of T;

correctness

coherence

not dom c is empty ;

coherence

inf (dom c) is real ;

end;
let c be with_first_point Curve of T;

correctness

coherence

not dom c is empty ;

proof end;

correctness coherence

inf (dom c) is real ;

proof end;

registration

let T be non empty TopStruct ;

let c be with_last_point Curve of T;

correctness

coherence

not dom c is empty ;

coherence

sup (dom c) is real ;

end;
let c be with_last_point Curve of T;

correctness

coherence

not dom c is empty ;

proof end;

correctness coherence

sup (dom c) is real ;

proof end;

registration

let T be non empty TopStruct ;

coherence

for b_{1} being Curve of T st b_{1} is with_first_point holds

not b_{1} is empty
;

coherence

for b_{1} being Curve of T st b_{1} is with_last_point holds

not b_{1} is empty
;

end;
coherence

for b

not b

coherence

for b

not b

definition

let T be non empty TopStruct ;

let c be with_first_point Curve of T;

correctness

coherence

c . (inf (dom c)) is Point of T;

end;
let c be with_first_point Curve of T;

correctness

coherence

c . (inf (dom c)) is Point of T;

proof end;

:: deftheorem defines the_first_point_of TOPALG_6:def 9 :

for T being non empty TopStruct

for c being with_first_point Curve of T holds the_first_point_of c = c . (inf (dom c));

for T being non empty TopStruct

for c being with_first_point Curve of T holds the_first_point_of c = c . (inf (dom c));

definition

let T be non empty TopStruct ;

let c be with_last_point Curve of T;

correctness

coherence

c . (sup (dom c)) is Point of T;

end;
let c be with_last_point Curve of T;

correctness

coherence

c . (sup (dom c)) is Point of T;

proof end;

:: deftheorem defines the_last_point_of TOPALG_6:def 10 :

for T being non empty TopStruct

for c being with_last_point Curve of T holds the_last_point_of c = c . (sup (dom c));

for T being non empty TopStruct

for c being with_last_point Curve of T holds the_last_point_of c = c . (sup (dom c));

theorem Th25: :: TOPALG_6:25

for T being non empty TopStruct

for t1, t2 being Point of T

for p being Path of t1,t2 st t1,t2 are_connected holds

p is with_endpoints Curve of T

for t1, t2 being Point of T

for p being Path of t1,t2 st t1,t2 are_connected holds

p is with_endpoints Curve of T

proof end;

theorem Th26: :: TOPALG_6:26

for T being non empty TopStruct

for c being Curve of T

for r1, r2 being Real holds c | [.r1,r2.] is Curve of T

for c being Curve of T

for r1, r2 being Real holds c | [.r1,r2.] is Curve of T

proof end;

theorem Th27: :: TOPALG_6:27

for T being non empty TopStruct

for c being with_endpoints Curve of T holds dom c = [.(inf (dom c)),(sup (dom c)).]

for c being with_endpoints Curve of T holds dom c = [.(inf (dom c)),(sup (dom c)).]

proof end;

theorem Th28: :: TOPALG_6:28

for T being non empty TopStruct

for c being with_endpoints Curve of T st dom c = [.0,1.] holds

c is Path of the_first_point_of c, the_last_point_of c

for c being with_endpoints Curve of T st dom c = [.0,1.] holds

c is Path of the_first_point_of c, the_last_point_of c

proof end;

theorem Th29: :: TOPALG_6:29

for T being non empty TopStruct

for c being with_endpoints Curve of T holds c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c

for c being with_endpoints Curve of T holds c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c

proof end;

theorem :: TOPALG_6:30

for T being non empty TopStruct

for c being with_endpoints Curve of T

for t1, t2 being Point of T st c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of t1,t2 & t1,t2 are_connected holds

( t1 = the_first_point_of c & t2 = the_last_point_of c )

for c being with_endpoints Curve of T

for t1, t2 being Point of T st c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of t1,t2 & t1,t2 are_connected holds

( t1 = the_first_point_of c & t2 = the_last_point_of c )

proof end;

theorem Th31: :: TOPALG_6:31

for T being non empty TopStruct

for c being with_endpoints Curve of T holds

( the_first_point_of c in rng c & the_last_point_of c in rng c )

for c being with_endpoints Curve of T holds

( the_first_point_of c in rng c & the_last_point_of c in rng c )

proof end;

theorem Th32: :: TOPALG_6:32

for T being non empty TopStruct

for r1, r2 being Real

for t1, t2 being Point of T

for p1 being Path of t1,t2 st t1,t2 are_connected & r1 < r2 holds

p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T

for r1, r2 being Real

for t1, t2 being Point of T

for p1 being Path of t1,t2 st t1,t2 are_connected & r1 < r2 holds

p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T

proof end;

theorem Th33: :: TOPALG_6:33

for T being non empty TopStruct

for c being with_endpoints Curve of T holds the_first_point_of c, the_last_point_of c are_connected

for c being with_endpoints Curve of T holds the_first_point_of c, the_last_point_of c are_connected

proof end;

definition

let T be non empty TopStruct ;

let c1, c2 be with_endpoints Curve of T;

for c1, c2 being with_endpoints Curve of T st ex a, b being Point of T ex p1, p2 being Path of a,b st

( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic ) holds

ex a, b being Point of T ex p1, p2 being Path of a,b st

( p1 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p2 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p1,p2 are_homotopic ) ;

end;
let c1, c2 be with_endpoints Curve of T;

pred c1,c2 are_homotopic means :: TOPALG_6:def 11

ex a, b being Point of T ex p1, p2 being Path of a,b st

( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic );

symmetry ex a, b being Point of T ex p1, p2 being Path of a,b st

( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic );

for c1, c2 being with_endpoints Curve of T st ex a, b being Point of T ex p1, p2 being Path of a,b st

( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic ) holds

ex a, b being Point of T ex p1, p2 being Path of a,b st

( p1 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p2 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p1,p2 are_homotopic ) ;

:: deftheorem defines are_homotopic TOPALG_6:def 11 :

for T being non empty TopStruct

for c1, c2 being with_endpoints Curve of T holds

( c1,c2 are_homotopic iff ex a, b being Point of T ex p1, p2 being Path of a,b st

( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic ) );

for T being non empty TopStruct

for c1, c2 being with_endpoints Curve of T holds

( c1,c2 are_homotopic iff ex a, b being Point of T ex p1, p2 being Path of a,b st

( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic ) );

definition

let T be non empty TopSpace;

let c1, c2 be with_endpoints Curve of T;

:: original: are_homotopic

redefine pred c1,c2 are_homotopic ;

reflexivity

for c1 being with_endpoints Curve of T holds (T,b_{1},b_{1})

for c1, c2 being with_endpoints Curve of T st (T,b_{1},b_{2}) holds

(T,b_{2},b_{1})
;

end;
let c1, c2 be with_endpoints Curve of T;

:: original: are_homotopic

redefine pred c1,c2 are_homotopic ;

reflexivity

for c1 being with_endpoints Curve of T holds (T,b

proof end;

symmetry for c1, c2 being with_endpoints Curve of T st (T,b

(T,b

theorem Th34: :: TOPALG_6:34

for T being non empty TopStruct

for c1, c2 being with_endpoints Curve of T

for a, b being Point of T

for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds

( c1,c2 are_homotopic iff p1,p2 are_homotopic )

for c1, c2 being with_endpoints Curve of T

for a, b being Point of T

for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds

( c1,c2 are_homotopic iff p1,p2 are_homotopic )

proof end;

theorem Th35: :: TOPALG_6:35

for T being non empty TopStruct

for c1, c2 being with_endpoints Curve of T st c1,c2 are_homotopic holds

( the_first_point_of c1 = the_first_point_of c2 & the_last_point_of c1 = the_last_point_of c2 )

for c1, c2 being with_endpoints Curve of T st c1,c2 are_homotopic holds

( the_first_point_of c1 = the_first_point_of c2 & the_last_point_of c1 = the_last_point_of c2 )

proof end;

theorem Th36: :: TOPALG_6:36

for T being non empty TopSpace

for c1, c2 being with_endpoints Curve of T

for S being Subset of R^1 st dom c1 = dom c2 & S = dom c1 holds

( c1,c2 are_homotopic iff ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st

( f is continuous & ( for t being Point of (R^1 | S) holds

( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds

( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) )

for c1, c2 being with_endpoints Curve of T

for S being Subset of R^1 st dom c1 = dom c2 & S = dom c1 holds

( c1,c2 are_homotopic iff ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st

( f is continuous & ( for t being Point of (R^1 | S) holds

( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds

( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) )

proof end;

definition

let T be TopStruct ;

let c1, c2 be Curve of T;

coherence

( ( c1 \/ c2 is Curve of T implies c1 \/ c2 is Curve of T ) & ( c1 \/ c2 is not Curve of T implies {} is Curve of T ) );

consistency

for b_{1} being Curve of T holds verum;

end;
let c1, c2 be Curve of T;

func c1 + c2 -> Curve of T equals :Def12: :: TOPALG_6:def 12

c1 \/ c2 if c1 \/ c2 is Curve of T

otherwise {} ;

correctness c1 \/ c2 if c1 \/ c2 is Curve of T

otherwise {} ;

coherence

( ( c1 \/ c2 is Curve of T implies c1 \/ c2 is Curve of T ) & ( c1 \/ c2 is not Curve of T implies {} is Curve of T ) );

consistency

for b

proof end;

:: deftheorem Def12 defines + TOPALG_6:def 12 :

for T being TopStruct

for c1, c2 being Curve of T holds

( ( c1 \/ c2 is Curve of T implies c1 + c2 = c1 \/ c2 ) & ( c1 \/ c2 is not Curve of T implies c1 + c2 = {} ) );

for T being TopStruct

for c1, c2 being Curve of T holds

( ( c1 \/ c2 is Curve of T implies c1 + c2 = c1 \/ c2 ) & ( c1 \/ c2 is not Curve of T implies c1 + c2 = {} ) );

theorem Th37: :: TOPALG_6:37

for T being non empty TopStruct

for c being with_endpoints Curve of T

for r being Real ex c1, c2 being Element of Curves T st

( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )

for c being with_endpoints Curve of T

for r being Real ex c1, c2 being Element of Curves T st

( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )

proof end;

theorem Th38: :: TOPALG_6:38

for T being non empty TopSpace

for c1, c2 being with_endpoints Curve of T st sup (dom c1) = inf (dom c2) & the_last_point_of c1 = the_first_point_of c2 holds

( c1 + c2 is with_endpoints & dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] & (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 & (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 )

for c1, c2 being with_endpoints Curve of T st sup (dom c1) = inf (dom c2) & the_last_point_of c1 = the_first_point_of c2 holds

( c1 + c2 is with_endpoints & dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] & (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 & (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 )

proof end;

theorem Th39: :: TOPALG_6:39

for T being non empty TopSpace

for c1, c2, c3, c4, c5, c6 being with_endpoints Curve of T st c1,c2 are_homotopic & dom c1 = dom c2 & c3,c4 are_homotopic & dom c3 = dom c4 & c5 = c1 + c3 & c6 = c2 + c4 & the_last_point_of c1 = the_first_point_of c3 & sup (dom c1) = inf (dom c3) holds

c5,c6 are_homotopic

for c1, c2, c3, c4, c5, c6 being with_endpoints Curve of T st c1,c2 are_homotopic & dom c1 = dom c2 & c3,c4 are_homotopic & dom c3 = dom c4 & c5 = c1 + c3 & c6 = c2 + c4 & the_last_point_of c1 = the_first_point_of c3 & sup (dom c1) = inf (dom c3) holds

c5,c6 are_homotopic

proof end;

definition

let T be TopStruct ;

let f be FinSequence of Curves T;

ex b_{1} being FinSequence of Curves T st

( len f = len b_{1} & f . 1 = b_{1} . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{1} . (i + 1) = (b_{1} /. i) + (f /. (i + 1)) ) )

for b_{1}, b_{2} being FinSequence of Curves T st len f = len b_{1} & f . 1 = b_{1} . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{1} . (i + 1) = (b_{1} /. i) + (f /. (i + 1)) ) & len f = len b_{2} & f . 1 = b_{2} . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{2} . (i + 1) = (b_{2} /. i) + (f /. (i + 1)) ) holds

b_{1} = b_{2}

end;
let f be FinSequence of Curves T;

func Partial_Sums f -> FinSequence of Curves T means :Def13: :: TOPALG_6:def 13

( len f = len it & f . 1 = it . 1 & ( for i being Nat st 1 <= i & i < len f holds

it . (i + 1) = (it /. i) + (f /. (i + 1)) ) );

existence ( len f = len it & f . 1 = it . 1 & ( for i being Nat st 1 <= i & i < len f holds

it . (i + 1) = (it /. i) + (f /. (i + 1)) ) );

ex b

( len f = len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines Partial_Sums TOPALG_6:def 13 :

for T being TopStruct

for f, b_{3} being FinSequence of Curves T holds

( b_{3} = Partial_Sums f iff ( len f = len b_{3} & f . 1 = b_{3} . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{3} . (i + 1) = (b_{3} /. i) + (f /. (i + 1)) ) ) );

for T being TopStruct

for f, b

( b

b

definition

let T be TopStruct ;

let f be FinSequence of Curves T;

( ( len f > 0 implies (Partial_Sums f) . (len f) is Curve of T ) & ( not len f > 0 implies {} is Curve of T ) )

for b_{1} being Curve of T holds verum
;

end;
let f be FinSequence of Curves T;

func Sum f -> Curve of T equals :Def14: :: TOPALG_6:def 14

(Partial_Sums f) . (len f) if len f > 0

otherwise {} ;

coherence (Partial_Sums f) . (len f) if len f > 0

otherwise {} ;

( ( len f > 0 implies (Partial_Sums f) . (len f) is Curve of T ) & ( not len f > 0 implies {} is Curve of T ) )

proof end;

consistency for b

:: deftheorem Def14 defines Sum TOPALG_6:def 14 :

for T being TopStruct

for f being FinSequence of Curves T holds

( ( len f > 0 implies Sum f = (Partial_Sums f) . (len f) ) & ( not len f > 0 implies Sum f = {} ) );

for T being TopStruct

for f being FinSequence of Curves T holds

( ( len f > 0 implies Sum f = (Partial_Sums f) . (len f) ) & ( not len f > 0 implies Sum f = {} ) );

Lm2: for T being non empty TopStruct

for f1, f2 being FinSequence of Curves T holds (Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1)

proof end;

theorem Th41: :: TOPALG_6:41

for T being non empty TopStruct

for c being Curve of T

for f being FinSequence of Curves T holds Sum (f ^ <*c*>) = (Sum f) + c

for c being Curve of T

for f being FinSequence of Curves T holds Sum (f ^ <*c*>) = (Sum f) + c

proof end;

theorem Th42: :: TOPALG_6:42

for T being non empty TopStruct

for X being set

for f being FinSequence of Curves T st ( for i being Nat st 1 <= i & i <= len f holds

rng (f /. i) c= X ) holds

rng (Sum f) c= X

for X being set

for f being FinSequence of Curves T st ( for i being Nat st 1 <= i & i <= len f holds

rng (f /. i) c= X ) holds

rng (Sum f) c= X

proof end;

theorem Th43: :: TOPALG_6:43

for T being non empty TopSpace

for f being FinSequence of Curves T st len f > 0 & ( for i being Nat st 1 <= i & i < len f holds

( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) & sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f holds

f /. i is with_endpoints ) holds

ex c being with_endpoints Curve of T st

( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )

for f being FinSequence of Curves T st len f > 0 & ( for i being Nat st 1 <= i & i < len f holds

( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) & sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f holds

f /. i is with_endpoints ) holds

ex c being with_endpoints Curve of T st

( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )

proof end;

theorem Th44: :: TOPALG_6:44

for T being non empty TopSpace

for f1, f2 being FinSequence of Curves T

for c1, c2 being with_endpoints Curve of T st len f1 > 0 & len f1 = len f2 & Sum f1 = c1 & Sum f2 = c2 & ( for i being Nat st 1 <= i & i < len f1 holds

( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i < len f2 holds

( (f2 /. i) . (sup (dom (f2 /. i))) = (f2 /. (i + 1)) . (inf (dom (f2 /. (i + 1)))) & sup (dom (f2 /. i)) = inf (dom (f2 /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f1 holds

ex c3, c4 being with_endpoints Curve of T st

( c3 = f1 /. i & c4 = f2 /. i & c3,c4 are_homotopic & dom c3 = dom c4 ) ) holds

c1,c2 are_homotopic

for f1, f2 being FinSequence of Curves T

for c1, c2 being with_endpoints Curve of T st len f1 > 0 & len f1 = len f2 & Sum f1 = c1 & Sum f2 = c2 & ( for i being Nat st 1 <= i & i < len f1 holds

( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i < len f2 holds

( (f2 /. i) . (sup (dom (f2 /. i))) = (f2 /. (i + 1)) . (inf (dom (f2 /. (i + 1)))) & sup (dom (f2 /. i)) = inf (dom (f2 /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f1 holds

ex c3, c4 being with_endpoints Curve of T st

( c3 = f1 /. i & c4 = f2 /. i & c3,c4 are_homotopic & dom c3 = dom c4 ) ) holds

c1,c2 are_homotopic

proof end;

theorem Th45: :: TOPALG_6:45

for T being non empty TopStruct

for c being with_endpoints Curve of T

for h being FinSequence of REAL st len h >= 2 & h . 1 = inf (dom c) & h . (len h) = sup (dom c) & h is increasing holds

ex f being FinSequence of Curves T st

( len f = (len h) - 1 & c = Sum f & ( for i being Nat st 1 <= i & i <= len f holds

f /. i = c | [.(h /. i),(h /. (i + 1)).] ) )

for c being with_endpoints Curve of T

for h being FinSequence of REAL st len h >= 2 & h . 1 = inf (dom c) & h . (len h) = sup (dom c) & h is increasing holds

ex f being FinSequence of Curves T st

( len f = (len h) - 1 & c = Sum f & ( for i being Nat st 1 <= i & i <= len f holds

f /. i = c | [.(h /. i),(h /. (i + 1)).] ) )

proof end;

Lm3: for n being Nat

for t being Point of (TUnitSphere n)

for f being Loop of t st rng f <> the carrier of (TUnitSphere n) holds

f is nullhomotopic

proof end;

Lm4: for n being Nat

for t being Point of (TUnitSphere n)

for f being Loop of t st n >= 2 & rng f = the carrier of (TUnitSphere n) holds

ex g being Loop of t st

( g,f are_homotopic & rng g <> the carrier of (TUnitSphere n) )

proof end;

theorem :: TOPALG_6:47

for n being non zero Nat

for r being positive Real

for x being Point of (TOP-REAL n) st n >= 3 holds

Tcircle (x,r) is having_trivial_Fundamental_Group

for r being positive Real

for x being Point of (TOP-REAL n) st n >= 3 holds

Tcircle (x,r) is having_trivial_Fundamental_Group

proof end;