:: TOPALG_5 semantic presentation

set c₁ = |[0,0]|;

set c₂ = the carrier of I[01] ;

set c₃ = the carrier of R^1 ;

Lemma1: 0 in INT
by INT_1:def 1;

Lemma2: 0 in the carrier of I[01]
by JORDAN5A:2;

then Lemma3: {0} c= the carrier of I[01]
by ZFMISC_1:37;

Lemma4: 0 in {0}
by TARSKI:def 1;

Lemma5: the carrier of [:I[01] ,I[01] :] = [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;

reconsider c₄ = 0, c₅ = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;

Lemma6: [#] I[01] = the carrier of I[01]
;

Lemma7: I[01] | ([#] I[01] ) = I[01]
by TSEP_1:3;

Lemma8: 1 - 0 <= 1
;

Lemma9: (3 / 2) - (1 / 2) <= 1
;

registration

cluster -> integer Element of the carrier of INT.Group ;
coherence by INT_1:def 2, GR_CY_1:def 4;

end;

registration

cluster INT.Group -> infinite ;
coherence

proof end;

end;

registration

let c₆ be infinite 1-sorted ;
cluster the carrier of a₁ -> infinite ;
coherence by GROUP_1:def 14;

end;

theorem Th1: :: TOPALG_5:1

for b₁, b₂, b₃ being real number st b₁ <= b₂ & 0 < b₃ holds
for b₄ being Point of (Closed-Interval-MSpace b₁,b₂) holds
( Ball b₄,b₃ = [.b₁,b₂.] or Ball b₄,b₃ = [.b₁,(b₄ + b₃).[ or Ball b₄,b₃ = ].(b₄ - b₃),b₂.] or Ball b₄,b₃ = ].(b₄ - b₃),(b₄ + b₃).[ )

proof end;

theorem Th2: :: TOPALG_5:2

for b₁, b₂ being real number st b₁ <= b₂ holds
ex b₃ being Basis of Closed-Interval-TSpace b₁,b₂ st
( ex b₄ being ManySortedSet of (Closed-Interval-TSpace b₁,b₂) st
for b₅ being Point of (Closed-Interval-MSpace b₁,b₂) holds
( b₄ . b₅ = { (Ball b₅,(1 / b₆)) where B is Nat : b₆ <> 0 } & b₃ = Union b₄ ) & ( for b₄ being Subset of (Closed-Interval-TSpace b₁,b₂) st b₄ in b₃ holds
b₄ is connected ) )

proof end;

theorem Th3: :: TOPALG_5:3

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₃ in b₂ holds
skl b₃,b₂ c= b₂

proof end;

registration

let c₆ be TopSpace;
let c₇ be open Subset of c₆;
cluster a₁ | a₂ -> open ;
coherence

proof end;

end;

theorem Th4: :: TOPALG_5:4

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
b₁ | b₃ = b₂ | b₄

proof end;

theorem Th5: :: TOPALG_5:5

for b₁, b₂ being TopSpace
for b₃, b₄ being Subset of b₂
for b₅, b₆ being Subset of b₁ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ = b₅ & b₄ = b₆ & b₃,b₄ are_separated holds
b₅,b₆ are_separated

proof end;

theorem Th6: :: TOPALG_5:6

for b₁, b₂ being TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is connected holds
b₂ is connected

proof end;

theorem Th7: :: TOPALG_5:7

for b₁, b₂ being TopSpace
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ = b₄ & b₃ is connected holds
b₄ is connected

proof end;

theorem Th8: :: TOPALG_5:8

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Point of b₂
for b₅ being a_neighborhood of b₃ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ = b₄ holds
b₅ is a_neighborhood of b₄

proof end;

theorem Th9: :: TOPALG_5:9

for b₁, b₂ being non empty TopSpace
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being a_neighborhood of b₃ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ = b₄ holds
b₅ is a_neighborhood of b₄

proof end;

theorem Th10: :: TOPALG_5:10

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Subset of b₂
for b₅ being Function of b₁,b₂ st b₅ is_homeomorphism & b₃ is_a_component_of b₄ holds
b₅ " b₃ is_a_component_of b₅ " b₄

proof end;

theorem Th11: :: TOPALG_5:11

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st b₃ = b₄ & b₃ is locally_connected holds
b₄ is locally_connected

proof end;

theorem Th12: :: TOPALG_5:12

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

proof end;

theorem Th13: :: TOPALG_5:13

for b₁ being non empty TopSpace holds
( b₁ is locally_connected iff [#] b₁ is locally_connected )

proof end;

Lemma21: for b₁ being non empty TopSpace
for b₂ being non empty open SubSpace of b₁ st b₁ is locally_connected holds
TopStruct(# the carrier of b₂,the topology of b₂ #) is locally_connected

proof end;

theorem Th14: :: TOPALG_5:14

for b₁ being non empty TopSpace
for b₂ being non empty open SubSpace of b₁ st b₁ is locally_connected holds
b₂ is locally_connected

proof end;

theorem Th15: :: TOPALG_5:15

for b₁, b₂ being non empty TopSpace st b₁,b₂ are_homeomorphic & b₁ is locally_connected holds
b₂ is locally_connected

proof end;

theorem Th16: :: TOPALG_5:16

for b₁ being non empty TopSpace st ex b₂ being Basis of b₁ st
for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is connected holds
b₁ is locally_connected

proof end;

theorem Th17: :: TOPALG_5:17

for b₁, b₂ being real number st b₁ <= b₂ holds
Closed-Interval-TSpace b₁,b₂ is locally_connected

proof end;

registration

cluster I[01] -> locally_connected ;
coherence by Th17, TOPMETR:27;

end;

registration

let c₆ be non empty open Subset of I[01] ;
cluster I[01] | a₁ -> locally_connected open ;
coherence by Th14;

end;

definition

let c₆ be real number ;
func ExtendInt c₁ -> Function of I[01] ,R^1 means :Def1: :: TOPALG_5:def 1
for b₁ being Point of I[01] holds a₂ . b₁ = a₁ * b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines ExtendInt TOPALG_5:def 1 :

registration

let c₆ be real number ;
cluster ExtendInt a₁ -> continuous ;
coherence

proof end;

end;

definition

let c₆ be real number ;
redefine func ExtendInt as ExtendInt c₁ -> Path of R^1 0, R^1 a₁;
coherence

proof end;

end;

definition

let c₆, c₇, c₈ be non empty TopSpace;
let c₉ be Function of [:c₆,c₇:],c₈;
let c₁₀ be Point of c₇;
func Prj1 c₅,c₄ -> Function of a₁,a₃ means :Def2: :: TOPALG_5:def 2
for b₁ being Point of a₁ holds a₆ . b₁ = a₄ . b₁,a₅;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Prj1 TOPALG_5:def 2 :

definition

let c₆, c₇, c₈ be non empty TopSpace;
let c₉ be Function of [:c₆,c₇:],c₈;
let c₁₀ be Point of c₆;
func Prj2 c₅,c₄ -> Function of a₂,a₃ means :Def3: :: TOPALG_5:def 3
for b₁ being Point of a₂ holds a₆ . b₁ = a₄ . a₅,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Prj2 TOPALG_5:def 3 :

registration

let c₆, c₇, c₈ be non empty TopSpace;
let c₉ be continuous Function of [:c₆,c₇:],c₈;
let c₁₀ be Point of c₇;
cluster Prj1 a₅,a₄ -> continuous ;
coherence

proof end;

end;

registration

let c₆, c₇, c₈ be non empty TopSpace;
let c₉ be continuous Function of [:c₆,c₇:],c₈;
let c₁₀ be Point of c₆;
cluster Prj2 a₅,a₄ -> continuous ;
coherence

proof end;

end;

theorem Th18: :: TOPALG_5:18

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being Path of b₂,b₃
for b₆ being Homotopy of b₄,b₅
for b₇ being Point of I[01] st b₆ is continuous holds
Prj1 b₇,b₆ is continuous

proof end;

theorem Th19: :: TOPALG_5:19

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being Path of b₂,b₃
for b₆ being Homotopy of b₄,b₅
for b₇ being Point of I[01] st b₆ is continuous holds
Prj2 b₇,b₆ is continuous

proof end;

set c₆ = Tunit_circle 2;

set c₇ = the carrier of (Tunit_circle 2);

E28: now

Tunit_circle 2 = Tcircle (0.REAL 2),1 by TOPREALB:def 7;
hence the carrier of (Tunit_circle 2) = Sphere |[0,0]|,1 by TOPREALB:9, EUCLID:58;

end;

Lemma29: dom CircleMap = REAL
by FUNCT_2:def 1, TOPMETR:24;

definition

let c₈ be real number ;
func cLoop c₁ -> Function of I[01] ,(Tunit_circle 2) means :Def4: :: TOPALG_5:def 4
for b₁ being Point of I[01] holds a₂ . b₁ = |[(cos (((2 * PI ) * a₁) * b₁)),(sin (((2 * PI ) * a₁) * b₁))]|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines cLoop TOPALG_5:def 4 :

theorem Th20: :: TOPALG_5:20

for b₁ being real number holds cLoop b₁ = CircleMap * (ExtendInt b₁)

proof end;

definition

let c₈ be Integer;
redefine func cLoop as cLoop c₁ -> Loop of c[10] ;
coherence

proof end;

end;

Lemma32: ex b₁ being Subset-Family of (Tunit_circle 2) st
( b₁ is_a_cover_of Tunit_circle 2 & b₁ is open & ( for b₂ being Subset of (Tunit_circle 2) st b₂ in b₁ holds
ex b₃ being mutually-disjoint open Subset-Family of R^1 st
( union b₃ = CircleMap " b₂ & ( for b₄ being Subset of R^1 st b₄ in b₃ holds
for b₅ being Function of (R^1 | b₄),((Tunit_circle 2) | b₂) st b₅ = CircleMap | b₄ holds
b₅ is_homeomorphism ) ) ) )

proof end;

Lemma33: the carrier of (Sspace 0[01] ) = {0}
by BORSUK_1:def 17, TEX_2:def 4;

then Lemma34: [#] (Sspace 0[01] ) = {0}
;

Lemma35: for b₁, b₂ being real number
for b₃ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₄ being IntervalCover of b₃
for b₅ being IntervalCoverPts of b₄ st b₃ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₃ is open & b₃ is connected & b₁ <= b₂ holds
not b₅ is empty

proof end;

theorem Th21: :: TOPALG_5:21

for b₁ being Subset-Family of (Tunit_circle 2) st b₁ is_a_cover_of Tunit_circle 2 & b₁ is open holds
for b₂ being non empty TopSpace
for b₃ being continuous Function of [:b₂,I[01] :],(Tunit_circle 2)
for b₄ being Point of b₂ ex b₅ being non empty FinSequence of REAL st
( b₅ . 1 = 0 & b₅ . (len b₅) = 1 & b₅ is increasing & ex b₆ being open Subset of b₂ st
( b₄ in b₆ & ( for b₇ being natural number st b₇ in dom b₅ & b₇ + 1 in dom b₅ holds
ex b₈ being non empty Subset of (Tunit_circle 2) st
( b₈ in b₁ & b₃ .: [:b₆,[.(b₅ . b₇),(b₅ . (b₇ + 1)).]:] c= b₈ ) ) ) )

proof end;

theorem Th22: :: TOPALG_5:22

for b₁ being non empty TopSpace
for b₂ being Function of [:b₁,I[01] :],(Tunit_circle 2)
for b₃ being Function of [:b₁,(Sspace 0[01] ):],R^1 st b₂ is continuous & b₃ is continuous & b₂ | [:the carrier of b₁,{0}:] = CircleMap * b₃ holds
ex b₄ being Function of [:b₁,I[01] :],R^1 st
( b₄ is continuous & b₂ = CircleMap * b₄ & b₄ | [:the carrier of b₁,{0}:] = b₃ & ( for b₅ being Function of [:b₁,I[01] :],R^1 st b₅ is continuous & b₂ = CircleMap * b₅ & b₅ | [:the carrier of b₁,{0}:] = b₃ holds
b₄ = b₅ ) )

proof end;

theorem Th23: :: TOPALG_5:23

for b₁, b₂ being Point of (Tunit_circle 2)
for b₃ being Point of R^1
for b₄ being Path of b₁,b₂ st b₃ in CircleMap " {b₁} holds
ex b₅ being Function of I[01] ,R^1 st
( b₅ . 0 = b₃ & b₄ = CircleMap * b₅ & b₅ is continuous & ( for b₆ being Function of I[01] ,R^1 st b₆ is continuous & b₄ = CircleMap * b₆ & b₆ . 0 = b₃ holds
b₅ = b₆ ) )

proof end;

theorem Th24: :: TOPALG_5:24

for b₁, b₂ being Point of (Tunit_circle 2)
for b₃, b₄ being Path of b₁,b₂
for b₅ being Homotopy of b₃,b₄
for b₆ being Point of R^1 st b₃,b₄ are_homotopic & b₆ in CircleMap " {b₁} holds
ex b₇ being Point of R^1 ex b₈, b₉ being Path of b₆,b₇ex b₁₀ being Homotopy of b₈,b₉ st
( b₈,b₉ are_homotopic & b₅ = CircleMap * b₁₀ & b₇ in CircleMap " {b₂} & ( for b₁₁ being Homotopy of b₈,b₉ st b₅ = CircleMap * b₁₁ holds
b₁₀ = b₁₁ ) )

proof end;

definition

func Ciso -> Function of INT.Group ,(pi_1 (Tunit_circle 2),c[10] ) means :Def5: :: TOPALG_5:def 5
for b₁ being Integer holds a₁ . b₁ = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Ciso TOPALG_5:def 5 :

theorem Th25: :: TOPALG_5:25

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

proof end;

definition

redefine func Ciso as Ciso -> Homomorphism of INT.Group ,(pi_1 (Tunit_circle 2),c[10] );
coherence

proof end;

end;

registration

cluster Ciso -> one-to-one onto ;
coherence

proof end;

end;

theorem Th26: :: TOPALG_5:26

Ciso is being_isomorphism

proof end;

Lemma43: for b₁ being real positive number
for b₂ being Point of (TOP-REAL 2)
for b₃ being Point of (Tcircle b₂,b₁) holds INT.Group , pi_1 (Tcircle b₂,b₁),b₃ are_isomorphic

proof end;

theorem Th27: :: TOPALG_5:27

for b₁ being being_simple_closed_curve SubSpace of TOP-REAL 2
for b₂ being Point of b₁ holds INT.Group , pi_1 b₁,b₂ are_isomorphic

proof end;

registration

let c₈ be being_simple_closed_curve SubSpace of TOP-REAL 2;
let c₉ be Point of c₈;
cluster FundamentalGroup a₁,a₂ -> infinite ;
coherence

proof end;

end;