:: by Artur Korni{\l}owicz

::

:: Received February 22, 2005

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

set o = |[0,0]|;

set I = the carrier of I[01];

set R = the carrier of R^1;

Lm1: 0 in INT

by INT_1:def 1;

Lm2: 0 in the carrier of I[01]

by BORSUK_1:43;

then Lm3: {0} c= the carrier of I[01]

by ZFMISC_1:31;

Lm4: 0 in {0}

by TARSKI:def 1;

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

by BORSUK_1:def 2;

reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;

Lm6: [#] I[01] = the carrier of I[01]

;

Lm7: I[01] | ([#] I[01]) = I[01]

by TSEP_1:3;

Lm8: 1 - 0 <= 1

;

Lm9: (3 / 2) - (1 / 2) <= 1

;

theorem Th1: :: TOPALG_5:1

for a, r, s being Real st r <= s holds

for p being Point of (Closed-Interval-MSpace (r,s)) holds

( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )

for p being Point of (Closed-Interval-MSpace (r,s)) holds

( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )

proof end;

theorem Th2: :: TOPALG_5:2

for r, s being Real st r <= s holds

ex B being Basis of (Closed-Interval-TSpace (r,s)) st

( ex f being ManySortedSet of (Closed-Interval-TSpace (r,s)) st

for y being Point of (Closed-Interval-MSpace (r,s)) holds

( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds

X is connected ) )

ex B being Basis of (Closed-Interval-TSpace (r,s)) st

( ex f being ManySortedSet of (Closed-Interval-TSpace (r,s)) st

for y being Point of (Closed-Interval-MSpace (r,s)) holds

( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds

X is connected ) )

proof end;

theorem Th3: :: TOPALG_5:3

for T being TopStruct

for A being Subset of T

for t being Point of T st t in A holds

Component_of (t,A) c= A

for A being Subset of T

for t being Point of T st t in A holds

Component_of (t,A) c= A

proof end;

registration
end;

theorem Th4: :: TOPALG_5:4

for T being TopSpace

for S being SubSpace of T

for A being Subset of T

for B being Subset of S st A = B holds

T | A = S | B

for S being SubSpace of T

for A being Subset of T

for B being Subset of S st A = B holds

T | A = S | B

proof end;

theorem :: TOPALG_5:6

for S, T being TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is connected holds

T is connected

T is connected

proof end;

theorem Th7: :: TOPALG_5:7

for S, T being TopSpace

for A being Subset of S

for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected holds

B is connected

for A being Subset of S

for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected holds

B is connected

proof end;

theorem Th8: :: TOPALG_5:8

for S, T being non empty TopSpace

for s being Point of S

for t being Point of T

for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds

A is a_neighborhood of t

for s being Point of S

for t being Point of T

for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds

A is a_neighborhood of t

proof end;

theorem :: TOPALG_5:9

for S, T being non empty TopSpace

for A being Subset of S

for B being Subset of T

for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds

N is a_neighborhood of B

for A being Subset of S

for B being Subset of T

for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds

N is a_neighborhood of B

proof end;

theorem Th10: :: TOPALG_5:10

for S, T being non empty TopSpace

for A, B being Subset of T

for f being Function of S,T st f is being_homeomorphism & A is_a_component_of B holds

f " A is_a_component_of f " B

for A, B being Subset of T

for f being Function of S,T st f is being_homeomorphism & A is_a_component_of B holds

f " A is_a_component_of f " B

proof end;

theorem Th12: :: TOPALG_5:12

for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally_connected holds

T is locally_connected

T is locally_connected

proof end;

Lm10: for T being non empty TopSpace

for S being non empty open SubSpace of T st T is locally_connected holds

TopStruct(# the carrier of S, the topology of S #) is locally_connected

proof end;

theorem Th14: :: TOPALG_5:14

for T being non empty TopSpace

for S being non empty open SubSpace of T st T is locally_connected holds

S is locally_connected

for S being non empty open SubSpace of T st T is locally_connected holds

S is locally_connected

proof end;

theorem :: TOPALG_5:15

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

T is locally_connected

T is locally_connected

proof end;

theorem Th16: :: TOPALG_5:16

for T being non empty TopSpace st ex B being Basis of T st

for X being Subset of T st X in B holds

X is connected holds

T is locally_connected

for X being Subset of T st X in B holds

X is connected holds

T is locally_connected

proof end;

registration
end;

registration
end;

definition

let r be Real;

ex b_{1} being Function of I[01],R^1 st

for x being Point of I[01] holds b_{1} . x = r * x

for b_{1}, b_{2} being Function of I[01],R^1 st ( for x being Point of I[01] holds b_{1} . x = r * x ) & ( for x being Point of I[01] holds b_{2} . x = r * x ) holds

b_{1} = b_{2}

end;
func ExtendInt r -> Function of I[01],R^1 means :Def1: :: TOPALG_5:def 1

for x being Point of I[01] holds it . x = r * x;

existence for x being Point of I[01] holds it . x = r * x;

ex b

for x being Point of I[01] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines ExtendInt TOPALG_5:def 1 :

for r being Real

for b_{2} being Function of I[01],R^1 holds

( b_{2} = ExtendInt r iff for x being Point of I[01] holds b_{2} . x = r * x );

for r being Real

for b

( b

registration
end;

definition

let r be Real;

:: original: ExtendInt

redefine func ExtendInt r -> Path of R^1 0, R^1 r;

coherence

ExtendInt r is Path of R^1 0, R^1 r

end;
:: original: ExtendInt

redefine func ExtendInt r -> Path of R^1 0, R^1 r;

coherence

ExtendInt r is Path of R^1 0, R^1 r

proof end;

definition

let S, T, Y be non empty TopSpace;

let H be Function of [:S,T:],Y;

let t be Point of T;

ex b_{1} being Function of S,Y st

for s being Point of S holds b_{1} . s = H . (s,t)

for b_{1}, b_{2} being Function of S,Y st ( for s being Point of S holds b_{1} . s = H . (s,t) ) & ( for s being Point of S holds b_{2} . s = H . (s,t) ) holds

b_{1} = b_{2}

end;
let H be Function of [:S,T:],Y;

let t be Point of T;

func Prj1 (t,H) -> Function of S,Y means :Def2: :: TOPALG_5:def 2

for s being Point of S holds it . s = H . (s,t);

existence for s being Point of S holds it . s = H . (s,t);

ex b

for s being Point of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines Prj1 TOPALG_5:def 2 :

for S, T, Y being non empty TopSpace

for H being Function of [:S,T:],Y

for t being Point of T

for b_{6} being Function of S,Y holds

( b_{6} = Prj1 (t,H) iff for s being Point of S holds b_{6} . s = H . (s,t) );

for S, T, Y being non empty TopSpace

for H being Function of [:S,T:],Y

for t being Point of T

for b

( b

definition

let S, T, Y be non empty TopSpace;

let H be Function of [:S,T:],Y;

let s be Point of S;

ex b_{1} being Function of T,Y st

for t being Point of T holds b_{1} . t = H . (s,t)

for b_{1}, b_{2} being Function of T,Y st ( for t being Point of T holds b_{1} . t = H . (s,t) ) & ( for t being Point of T holds b_{2} . t = H . (s,t) ) holds

b_{1} = b_{2}

end;
let H be Function of [:S,T:],Y;

let s be Point of S;

func Prj2 (s,H) -> Function of T,Y means :Def3: :: TOPALG_5:def 3

for t being Point of T holds it . t = H . (s,t);

existence for t being Point of T holds it . t = H . (s,t);

ex b

for t being Point of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Prj2 TOPALG_5:def 3 :

for S, T, Y being non empty TopSpace

for H being Function of [:S,T:],Y

for s being Point of S

for b_{6} being Function of T,Y holds

( b_{6} = Prj2 (s,H) iff for t being Point of T holds b_{6} . t = H . (s,t) );

for S, T, Y being non empty TopSpace

for H being Function of [:S,T:],Y

for s being Point of S

for b

( b

registration

let S, T, Y be non empty TopSpace;

let H be continuous Function of [:S,T:],Y;

let t be Point of T;

coherence

Prj1 (t,H) is continuous

end;
let H be continuous Function of [:S,T:],Y;

let t be Point of T;

coherence

Prj1 (t,H) is continuous

proof end;

registration

let S, T, Y be non empty TopSpace;

let H be continuous Function of [:S,T:],Y;

let s be Point of S;

coherence

Prj2 (s,H) is continuous

end;
let H be continuous Function of [:S,T:],Y;

let s be Point of S;

coherence

Prj2 (s,H) is continuous

proof end;

theorem :: TOPALG_5:18

for T being non empty TopSpace

for a, b being Point of T

for P, Q being Path of a,b

for H being Homotopy of P,Q

for t being Point of I[01] st H is continuous holds

Prj1 (t,H) is continuous ;

for a, b being Point of T

for P, Q being Path of a,b

for H being Homotopy of P,Q

for t being Point of I[01] st H is continuous holds

Prj1 (t,H) is continuous ;

theorem :: TOPALG_5:19

for T being non empty TopSpace

for a, b being Point of T

for P, Q being Path of a,b

for H being Homotopy of P,Q

for s being Point of I[01] st H is continuous holds

Prj2 (s,H) is continuous ;

for a, b being Point of T

for P, Q being Path of a,b

for H being Homotopy of P,Q

for s being Point of I[01] st H is continuous holds

Prj2 (s,H) is continuous ;

set TUC = Tunit_circle 2;

set cS1 = the carrier of (Tunit_circle 2);

Lm11: now :: thesis: the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1)

Tunit_circle 2 = Tcircle ((0. (TOP-REAL 2)),1)
by TOPREALB:def 7;

hence the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1) by EUCLID:54, TOPREALB:9; :: thesis: verum

end;
hence the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1) by EUCLID:54, TOPREALB:9; :: thesis: verum

Lm12: dom CircleMap = REAL

by FUNCT_2:def 1, TOPMETR:17;

definition

let r be Real;

ex b_{1} being Function of I[01],(Tunit_circle 2) st

for x being Point of I[01] holds b_{1} . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|

for b_{1}, b_{2} being Function of I[01],(Tunit_circle 2) st ( for x being Point of I[01] holds b_{1} . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) & ( for x being Point of I[01] holds b_{2} . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) holds

b_{1} = b_{2}

end;
func cLoop r -> Function of I[01],(Tunit_circle 2) means :Def4: :: TOPALG_5:def 4

for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|;

existence for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|;

ex b

for x being Point of I[01] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines cLoop TOPALG_5:def 4 :

for r being Real

for b_{2} being Function of I[01],(Tunit_circle 2) holds

( b_{2} = cLoop r iff for x being Point of I[01] holds b_{2} . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| );

for r being Real

for b

( b

definition

let n be Integer;

:: original: cLoop

redefine func cLoop n -> Loop of c[10] ;

coherence

cLoop n is Loop of c[10]

end;
:: original: cLoop

redefine func cLoop n -> Loop of c[10] ;

coherence

cLoop n is Loop of c[10]

proof end;

Lm13: ex F being Subset-Family of (Tunit_circle 2) st

( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) st U in F holds

ex D being mutually-disjoint open Subset-Family of R^1 st

( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) )

proof end;

Lm14: [#] (Sspace 0[01]) = {0}

by TEX_2:def 2;

Lm15: for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F

for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

not G is empty

proof end;

theorem Th21: :: TOPALG_5:21

for UL being Subset-Family of (Tunit_circle 2) st UL is Cover of (Tunit_circle 2) & UL is open holds

for Y being non empty TopSpace

for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)

for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

for Y being non empty TopSpace

for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)

for y being Point of Y ex T being non empty FinSequence of REAL st

( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st

( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds

ex Ui being non empty Subset of (Tunit_circle 2) st

( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

proof end;

theorem Th22: :: TOPALG_5:22

for Y being non empty TopSpace

for F being Function of [:Y,I[01]:],(Tunit_circle 2)

for Ft being Function of [:Y,(Sspace 0[01]):],R^1 st F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft holds

ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

for F being Function of [:Y,I[01]:],(Tunit_circle 2)

for Ft being Function of [:Y,(Sspace 0[01]):],R^1 st F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft holds

ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

proof end;

theorem Th23: :: TOPALG_5:23

for x0, y0 being Point of (Tunit_circle 2)

for xt being Point of R^1

for f being Path of x0,y0 st xt in CircleMap " {x0} holds

ex ft being Function of I[01],R^1 st

( ft . 0 = xt & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds

ft = f1 ) )

for xt being Point of R^1

for f being Path of x0,y0 st xt in CircleMap " {x0} holds

ex ft being Function of I[01],R^1 st

( ft . 0 = xt & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds

ft = f1 ) )

proof end;

theorem Th24: :: TOPALG_5:24

for x0, y0 being Point of (Tunit_circle 2)

for P, Q being Path of x0,y0

for F being Homotopy of P,Q

for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds

ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st

( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds

Ft = F1 ) )

for P, Q being Path of x0,y0

for F being Homotopy of P,Q

for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds

ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st

( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds

Ft = F1 ) )

proof end;

definition

ex b_{1} being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st

for n being Integer holds b_{1} . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))

for b_{1}, b_{2} being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st ( for n being Integer holds b_{1} . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) & ( for n being Integer holds b_{2} . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) holds

b_{1} = b_{2}
end;

func Ciso -> Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) means :Def5: :: TOPALG_5:def 5

for n being Integer holds it . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n));

existence for n being Integer holds it . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n));

ex b

for n being Integer holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines Ciso TOPALG_5:def 5 :

for b_{1} being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) holds

( b_{1} = Ciso iff for n being Integer holds b_{1} . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) );

for b

( b

theorem Th25: :: TOPALG_5:25

for i being Integer

for f being Path of R^1 0, R^1 i holds Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f))

for f being Path of R^1 0, R^1 i holds Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f))

proof end;

registration
end;

Lm16: for r being positive Real

for o being Point of (TOP-REAL 2)

for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic

proof end;

theorem Th27: :: TOPALG_5:27

for S being being_simple_closed_curve SubSpace of TOP-REAL 2

for x being Point of S holds INT.Group , pi_1 (S,x) are_isomorphic

for x being Point of S holds INT.Group , pi_1 (S,x) are_isomorphic

proof end;

registration

let S be being_simple_closed_curve SubSpace of TOP-REAL 2;

let x be Point of S;

coherence

not pi_1 (S,x) is finite

end;
let x be Point of S;

coherence

not pi_1 (S,x) is finite

proof end;