:: TOPALG_1 semantic presentation

theorem Th1: :: TOPALG_1:1

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ st b₃ * (b₃ " ) = id b₂ & (b₃ " ) * b₃ = id b₁ holds
b₃ is_isomorphism

proof end;

theorem Th2: :: TOPALG_1:2

for b₁ being Subset of I[01]
for b₂ being Point of I[01] st b₁ = ].b₂,1.] holds
b₁ ` = [.0,b₂.]

proof end;

theorem Th3: :: TOPALG_1:3

for b₁ being Subset of I[01]
for b₂ being Point of I[01] st b₁ = [.0,b₂.[ holds
b₁ ` = [.b₂,1.]

proof end;

theorem Th4: :: TOPALG_1:4

for b₁ being Subset of I[01]
for b₂ being Point of I[01] st b₁ = ].b₂,1.] holds
b₁ is open

proof end;

theorem Th5: :: TOPALG_1:5

for b₁ being Subset of I[01]
for b₂ being Point of I[01] st b₁ = [.0,b₂.[ holds
b₁ is open

proof end;

theorem Th6: :: TOPALG_1:6

for b₁ being real number
for b₂ being Nat
for b₃ being Element of b₂ -tuples_on REAL holds b₁ * (- b₃) = - (b₁ * b₃)

proof end;

theorem Th7: :: TOPALG_1:7

for b₁ being real number
for b₂ being Nat
for b₃, b₄ being Element of b₂ -tuples_on REAL holds b₁ * (b₃ - b₄) = (b₁ * b₃) - (b₁ * b₄)

proof end;

theorem Th8: :: TOPALG_1:8

for b₁, b₂ being real number
for b₃ being Nat
for b₄ being Element of b₃ -tuples_on REAL holds (b₁ - b₂) * b₄ = (b₁ * b₄) - (b₂ * b₄)

proof end;

theorem Th9: :: TOPALG_1:9

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of b₁ -tuples_on REAL holds (b₂ + b₃) - (b₄ + b₅) = (b₂ - b₄) + (b₃ - b₅)

proof end;

theorem Th10: :: TOPALG_1:10

for b₁ being real number
for b₂ being Nat
for b₃ being Element of REAL b₂ st 0 <= b₁ & b₁ <= 1 holds
|.(b₁ * b₃).| <= |.b₃.|

proof end;

theorem Th11: :: TOPALG_1:11

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Point of I[01] holds |.(b₃ * b₂).| <= |.b₂.|

proof end;

theorem Th12: :: TOPALG_1:12

for b₁, b₂ being real number
for b₃ being Nat
for b₄, b₅, b₆, b₇, b₈, b₉ being Point of (Euclid b₃)
for b₁₀, b₁₁, b₁₂, b₁₃ being Point of (TOP-REAL b₃) st b₄ = b₁₀ & b₅ = b₁₁ & b₆ = b₁₂ & b₇ = b₁₃ & b₈ = b₁₀ + b₁₂ & b₉ = b₁₁ + b₁₃ & dist b₄,b₅ < b₁ & dist b₆,b₇ < b₂ holds
dist b₈,b₉ < b₁ + b₂

proof end;

theorem Th13: :: TOPALG_1:13

for b₁, b₂ being real number
for b₃ being Nat
for b₄, b₅, b₆, b₇ being Point of (Euclid b₃)
for b₈, b₉ being Point of (TOP-REAL b₃) st b₄ = b₈ & b₅ = b₉ & b₆ = b₁ * b₈ & b₇ = b₁ * b₉ & dist b₄,b₅ < b₂ & b₁ <> 0 holds
dist b₆,b₇ < (abs b₁) * b₂

proof end;

theorem Th14: :: TOPALG_1:14

for b₁, b₂, b₃, b₄ being real number
for b₅ being Nat
for b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Point of (Euclid b₅)
for b₁₂, b₁₃, b₁₄, b₁₅ being Point of (TOP-REAL b₅) st b₆ = b₁₂ & b₇ = b₁₃ & b₈ = b₁₄ & b₉ = b₁₅ & b₁₀ = (b₁ * b₁₂) + (b₂ * b₁₄) & b₁₁ = (b₁ * b₁₃) + (b₂ * b₁₅) & dist b₆,b₇ < b₃ & dist b₈,b₉ < b₄ & b₁ <> 0 & b₂ <> 0 holds
dist b₁₀,b₁₁ < ((abs b₁) * b₃) + ((abs b₂) * b₄)

proof end;

Lemma12: for b₁ being Nat
for b₂ being non empty TopSpace
for b₃, b₄, b₅ being Function of b₂,(TOP-REAL b₁) st b₃ is continuous & b₄ is continuous & ( for b₆ being Point of b₂ holds b₅ . b₆ = (b₃ . b₆) + (b₄ . b₆) ) holds
b₅ is continuous

proof end;

theorem Th15: :: TOPALG_1:15

canceled;

theorem Th16: :: TOPALG_1:16

for b₁ being real number
for b₂ being Nat
for b₃ being non empty TopSpace
for b₄, b₅ being Function of b₃,(TOP-REAL b₂) st b₄ is continuous & ( for b₆ being Point of b₃ holds b₅ . b₆ = b₁ * (b₄ . b₆) ) holds
b₅ is continuous

proof end;

theorem Th17: :: TOPALG_1:17

for b₁, b₂ being real number
for b₃ being Nat
for b₄ being non empty TopSpace
for b₅, b₆, b₇ being Function of b₄,(TOP-REAL b₃) st b₅ is continuous & b₆ is continuous & ( for b₈ being Point of b₄ holds b₇ . b₈ = (b₁ * (b₅ . b₈)) + (b₂ * (b₆ . b₈)) ) holds
b₇ is continuous

proof end;

theorem Th18: :: TOPALG_1:18

for b₁ being Nat
for b₂ being Function of [:(TOP-REAL b₁),I[01] :],(TOP-REAL b₁) st ( for b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of I[01] holds b₂ . b₃,b₄ = (1 - b₄) * b₃ ) holds
b₂ is continuous

proof end;

theorem Th19: :: TOPALG_1:19

for b₁ being Nat
for b₂ being Function of [:(TOP-REAL b₁),I[01] :],(TOP-REAL b₁) st ( for b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of I[01] holds b₂ . b₃,b₄ = b₄ * b₃ ) holds
b₂ is continuous

proof end;

theorem Th20: :: TOPALG_1:20

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Point of b₁ st b₂,b₃ are_connected & b₃,b₄ are_connected holds
for b₅ being Path of b₂,b₃
for b₆ being Path of b₃,b₄ holds b₅,(b₅ + b₆) + (- b₆) are_homotopic

proof end;

theorem Th21: :: TOPALG_1:21

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Path of b₂,b₃
for b₆ being Path of b₃,b₄ holds b₅,(b₅ + b₆) + (- b₆) are_homotopic

proof end;

theorem Th22: :: TOPALG_1:22

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Point of b₁ st b₂,b₃ are_connected & b₄,b₃ are_connected holds
for b₅ being Path of b₂,b₃
for b₆ being Path of b₄,b₃ holds b₅,(b₅ + (- b₆)) + b₆ are_homotopic

proof end;

theorem Th23: :: TOPALG_1:23

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Path of b₂,b₃
for b₆ being Path of b₄,b₃ holds b₅,(b₅ + (- b₆)) + b₆ are_homotopic

proof end;

theorem Th24: :: TOPALG_1:24

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Point of b₁ st b₂,b₃ are_connected & b₄,b₂ are_connected holds
for b₅ being Path of b₂,b₃
for b₆ being Path of b₄,b₂ holds b₅,((- b₆) + b₆) + b₅ are_homotopic

proof end;

theorem Th25: :: TOPALG_1:25

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Path of b₂,b₃
for b₆ being Path of b₄,b₂ holds b₅,((- b₆) + b₆) + b₅ are_homotopic

proof end;

theorem Th26: :: TOPALG_1:26

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Point of b₁ st b₂,b₃ are_connected & b₂,b₄ are_connected holds
for b₅ being Path of b₂,b₃
for b₆ being Path of b₂,b₄ holds b₅,(b₆ + (- b₆)) + b₅ are_homotopic

proof end;

theorem Th27: :: TOPALG_1:27

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Path of b₂,b₃
for b₆ being Path of b₂,b₄ holds b₅,(b₆ + (- b₆)) + b₅ are_homotopic

proof end;

theorem Th28: :: TOPALG_1:28

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Point of b₁ st b₂,b₃ are_connected & b₄,b₃ are_connected holds
for b₅, b₆ being Path of b₂,b₃
for b₇ being Path of b₃,b₄ st b₅ + b₇,b₆ + b₇ are_homotopic holds
b₅,b₆ are_homotopic

proof end;

theorem Th29: :: TOPALG_1:29

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄ being Point of b₁
for b₅, b₆ being Path of b₂,b₃
for b₇ being Path of b₃,b₄ st b₅ + b₇,b₆ + b₇ are_homotopic holds
b₅,b₆ are_homotopic

proof end;

theorem Th30: :: TOPALG_1:30

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Point of b₁ st b₂,b₃ are_connected & b₂,b₄ are_connected holds
for b₅, b₆ being Path of b₂,b₃
for b₇ being Path of b₄,b₂ st b₇ + b₅,b₇ + b₆ are_homotopic holds
b₅,b₆ are_homotopic

proof end;

theorem Th31: :: TOPALG_1:31

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄ being Point of b₁
for b₅, b₆ being Path of b₂,b₃
for b₇ being Path of b₄,b₂ st b₇ + b₅,b₇ + b₆ are_homotopic holds
b₅,b₆ are_homotopic

proof end;

theorem Th32: :: TOPALG_1:32

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅, b₆ being Point of b₁ st b₂,b₃ are_connected & b₃,b₄ are_connected & b₄,b₅ are_connected & b₅,b₆ are_connected holds
for b₇ being Path of b₂,b₃
for b₈ being Path of b₃,b₄
for b₉ being Path of b₄,b₅
for b₁₀ being Path of b₅,b₆ holds ((b₇ + b₈) + b₉) + b₁₀,(b₇ + (b₈ + b₉)) + b₁₀ are_homotopic

proof end;

theorem Th33: :: TOPALG_1:33

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄, b₅, b₆ being Point of b₁
for b₇ being Path of b₂,b₃
for b₈ being Path of b₃,b₄
for b₉ being Path of b₄,b₅
for b₁₀ being Path of b₅,b₆ holds ((b₇ + b₈) + b₉) + b₁₀,(b₇ + (b₈ + b₉)) + b₁₀ are_homotopic

proof end;

theorem Th34: :: TOPALG_1:34

proof end;

theorem Th35: :: TOPALG_1:35

proof end;

theorem Th36: :: TOPALG_1:36

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅, b₆ being Point of b₁ st b₂,b₃ are_connected & b₃,b₄ are_connected & b₄,b₅ are_connected & b₅,b₆ are_connected holds
for b₇ being Path of b₂,b₃
for b₈ being Path of b₃,b₄
for b₉ being Path of b₄,b₅
for b₁₀ being Path of b₅,b₆ holds (b₇ + (b₈ + b₉)) + b₁₀,(b₇ + b₈) + (b₉ + b₁₀) are_homotopic

proof end;

theorem Th37: :: TOPALG_1:37

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄, b₅, b₆ being Point of b₁
for b₇ being Path of b₂,b₃
for b₈ being Path of b₃,b₄
for b₉ being Path of b₄,b₅
for b₁₀ being Path of b₅,b₆ holds (b₇ + (b₈ + b₉)) + b₁₀,(b₇ + b₈) + (b₉ + b₁₀) are_homotopic

proof end;

theorem Th38: :: TOPALG_1:38

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Point of b₁ st b₂,b₃ are_connected & b₃,b₄ are_connected & b₃,b₅ are_connected holds
for b₆ being Path of b₂,b₃
for b₇ being Path of b₅,b₃
for b₈ being Path of b₃,b₄ holds ((b₆ + (- b₇)) + b₇) + b₈,b₆ + b₈ are_homotopic

proof end;

theorem Th39: :: TOPALG_1:39

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄, b₅ being Point of b₁
for b₆ being Path of b₂,b₃
for b₇ being Path of b₄,b₃
for b₈ being Path of b₃,b₅ holds ((b₆ + (- b₇)) + b₇) + b₈,b₆ + b₈ are_homotopic

proof end;

theorem Th40: :: TOPALG_1:40

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Point of b₁ st b₂,b₃ are_connected & b₂,b₄ are_connected & b₄,b₅ are_connected holds
for b₆ being Path of b₂,b₃
for b₇ being Path of b₄,b₅
for b₈ being Path of b₂,b₄ holds (((b₆ + (- b₆)) + b₈) + b₇) + (- b₇),b₈ are_homotopic

proof end;

theorem Th41: :: TOPALG_1:41

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄, b₅ being Point of b₁
for b₆ being Path of b₂,b₃
for b₇ being Path of b₄,b₅
for b₈ being Path of b₂,b₄ holds (((b₆ + (- b₆)) + b₈) + b₇) + (- b₇),b₈ are_homotopic

proof end;

theorem Th42: :: TOPALG_1:42

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Point of b₁ st b₂,b₃ are_connected & b₂,b₄ are_connected & b₅,b₄ are_connected holds
for b₆ being Path of b₂,b₃
for b₇ being Path of b₄,b₅
for b₈ being Path of b₂,b₄ holds (b₆ + (((- b₆) + b₈) + b₇)) + (- b₇),b₈ are_homotopic

proof end;

theorem Th43: :: TOPALG_1:43

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄, b₅ being Point of b₁
for b₆ being Path of b₂,b₃
for b₇ being Path of b₄,b₅
for b₈ being Path of b₂,b₄ holds (b₆ + (((- b₆) + b₈) + b₇)) + (- b₇),b₈ are_homotopic

proof end;

theorem Th44: :: TOPALG_1:44

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Point of b₁ st b₂,b₃ are_connected & b₃,b₄ are_connected & b₄,b₅ are_connected & b₅,b₆ are_connected & b₂,b₇ are_connected holds
for b₈ being Path of b₂,b₃
for b₉ being Path of b₃,b₄
for b₁₀ being Path of b₄,b₅
for b₁₁ being Path of b₅,b₆
for b₁₂ being Path of b₇,b₄ holds (b₈ + (b₉ + b₁₀)) + b₁₁,((b₈ + b₉) + (- b₁₂)) + ((b₁₂ + b₁₀) + b₁₁) are_homotopic

proof end;

theorem Th45: :: TOPALG_1:45

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Point of b₁
for b₈ being Path of b₂,b₃
for b₉ being Path of b₃,b₄
for b₁₀ being Path of b₄,b₅
for b₁₁ being Path of b₅,b₆
for b₁₂ being Path of b₇,b₄ holds (b₈ + (b₉ + b₁₀)) + b₁₁,((b₈ + b₉) + (- b₁₂)) + ((b₁₂ + b₁₀) + b₁₁) are_homotopic

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Point of c₁;
mode Loop of a₂ is Path of a₂,a₂;

end;

definition

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
func Loops c₂ -> set means :Def1: :: TOPALG_1:def 1
for b₁ being set holds
( b₁ in a₃ iff b₁ is Loop of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Loops TOPALG_1:def 1 :

registration

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
cluster Loops a₂ -> non empty ;
coherence

proof end;

end;

Lemma30: for b₁ being non empty TopSpace
for b₂ being Point of b₁ ex b₃ being Equivalence_Relation of Loops b₂ st
for b₄, b₅ being set holds
( [b₄,b₅] in b₃ iff ( b₄ in Loops b₂ & b₅ in Loops b₂ & ex b₆, b₇ being Loop of b₂ st
( b₆ = b₄ & b₇ = b₅ & b₆,b₇ are_homotopic ) ) )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
func EqRel c₁,c₂ -> Relation of Loops a₂ means :Def2: :: TOPALG_1:def 2
for b₁, b₂ being Loop of a₂ holds
( [b₁,b₂] in a₃ iff b₁,b₂ are_homotopic );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines EqRel TOPALG_1:def 2 :

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster EqRel a₁,a₂ -> non empty symmetric transitive total ;
coherence

proof end;

end;

theorem Th46: :: TOPALG_1:46

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃, b₄ being Loop of b₂ holds
( b₄ in Class (EqRel b₁,b₂),b₃ iff b₃,b₄ are_homotopic )

proof end;

theorem Th47: :: TOPALG_1:47

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃, b₄ being Loop of b₂ holds
( Class (EqRel b₁,b₂),b₃ = Class (EqRel b₁,b₂),b₄ iff b₃,b₄ are_homotopic )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
func FundamentalGroup c₁,c₂ -> strict HGrStr means :Def3: :: TOPALG_1:def 3
( the carrier of a₃ = Class (EqRel a₁,a₂) & ( for b₁, b₂ being Element of a₃ ex b₃, b₄ being Loop of a₂ st
( b₁ = Class (EqRel a₁,a₂),b₃ & b₂ = Class (EqRel a₁,a₂),b₄ & the mult of a₃ . b₁,b₂ = Class (EqRel a₁,a₂),(b₃ + b₄) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines FundamentalGroup TOPALG_1:def 3 :

notation

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
synonym pi_1 c₁,c₂ for FundamentalGroup c₁,c₂;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster FundamentalGroup a₁,a₂ -> non empty strict ;
coherence

proof end;

end;

theorem Th48: :: TOPALG_1:48

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being set holds
( b₃ in the carrier of (pi_1 b₁,b₂) iff ex b₄ being Loop of b₂ st b₃ = Class (EqRel b₁,b₂),b₄ )

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster FundamentalGroup a₁,a₂ -> non empty strict Group-like associative ;
coherence

proof end;

end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Point of c₁;
let c₄ be Path of c₂,c₃;
assume E36: c₂,c₃ are_connected ;
func pi_1-iso c₄ -> Function of (pi_1 a₁,a₃),(pi_1 a₁,a₂) means :Def4: :: TOPALG_1:def 4
for b₁ being Loop of a₃ holds a₅ . (Class (EqRel a₁,a₃),b₁) = Class (EqRel a₁,a₂),((a₄ + b₁) + (- a₄));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines pi_1-iso TOPALG_1:def 4 :

theorem Th49: :: TOPALG_1:49

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being Path of b₂,b₃ st b₂,b₃ are_connected & b₄,b₅ are_homotopic holds
pi_1-iso b₄ = pi_1-iso b₅

proof end;

theorem Th50: :: TOPALG_1:50

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being Path of b₂,b₃ st b₄,b₅ are_homotopic holds
pi_1-iso b₄ = pi_1-iso b₅

proof end;

theorem Th51: :: TOPALG_1:51

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Path of b₂,b₃ st b₂,b₃ are_connected holds
pi_1-iso b₄ is Homomorphism of (pi_1 b₁,b₃),(pi_1 b₁,b₂)

proof end;

definition

let c₁ be non empty arcwise_connected TopSpace;
let c₂, c₃ be Point of c₁;
let c₄ be Path of c₂,c₃;
redefine func pi_1-iso as pi_1-iso c₄ -> Homomorphism of (pi_1 a₁,a₃),(pi_1 a₁,a₂);
coherence

proof end;

end;

theorem Th52: :: TOPALG_1:52

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Path of b₂,b₃ st b₂,b₃ are_connected holds
pi_1-iso b₄ is one-to-one

proof end;

theorem Th53: :: TOPALG_1:53

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Path of b₂,b₃ st b₂,b₃ are_connected holds
pi_1-iso b₄ is onto

proof end;

registration

let c₁ be non empty arcwise_connected TopSpace;
let c₂, c₃ be Point of c₁;
let c₄ be Path of c₂,c₃;
cluster pi_1-iso a₄ -> one-to-one onto ;
coherence

proof end;

end;

theorem Th54: :: TOPALG_1:54

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Path of b₂,b₃ st b₂,b₃ are_connected holds
(pi_1-iso b₄) " = pi_1-iso (- b₄)

proof end;

theorem Th55: :: TOPALG_1:55

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Path of b₂,b₃ holds (pi_1-iso b₄) " = pi_1-iso (- b₄)

proof end;

theorem Th56: :: TOPALG_1:56

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Path of b₂,b₃ st b₂,b₃ are_connected holds
for b₅ being Homomorphism of (pi_1 b₁,b₃),(pi_1 b₁,b₂) st b₅ = pi_1-iso b₄ holds
b₅ is_isomorphism

proof end;

theorem Th57: :: TOPALG_1:57

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Path of b₂,b₃ holds pi_1-iso b₄ is_isomorphism

proof end;

theorem Th58: :: TOPALG_1:58

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_connected holds
pi_1 b₁,b₂, pi_1 b₁,b₃ are_isomorphic

proof end;

theorem Th59: :: TOPALG_1:59

for b₁ being non empty arcwise_connected TopSpace
for b₂, b₃ being Point of b₁ holds pi_1 b₁,b₂, pi_1 b₁,b₃ are_isomorphic

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
let c₄, c₅ be Path of c₂,c₃;
func RealHomotopy c₄,c₅ -> Function of [:I[01] ,I[01] :],(TOP-REAL a₁) means :Def5: :: TOPALG_1:def 5
for b₁, b₂ being Element of I[01] holds a₆ . b₁,b₂ = ((1 - b₂) * (a₄ . b₁)) + (b₂ * (a₅ . b₁));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines RealHomotopy TOPALG_1:def 5 :

Lemma45: for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄, b₅ being Path of b₂,b₃ holds RealHomotopy b₄,b₅ is continuous

proof end;

Lemma46: for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄, b₅ being Path of b₂,b₃
for b₆ being Point of I[01] holds
( (RealHomotopy b₄,b₅) . b₆,0 = b₄ . b₆ & (RealHomotopy b₄,b₅) . b₆,1 = b₅ . b₆ & ( for b₇ being Point of I[01] holds
( (RealHomotopy b₄,b₅) . 0,b₇ = b₂ & (RealHomotopy b₄,b₅) . 1,b₇ = b₃ ) ) )

proof end;

theorem Th60: :: TOPALG_1:60

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄, b₅ being Path of b₂,b₃ holds b₄,b₅ are_homotopic

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
let c₄, c₅ be Path of c₂,c₃;
redefine func RealHomotopy as RealHomotopy c₄,c₅ -> Homotopy of a₄,a₅;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
let c₄, c₅ be Path of c₂,c₃;
cluster -> continuous Homotopy of a₄,a₅;
coherence

proof end;

end;

theorem Th61: :: TOPALG_1:61

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being Loop of b₂ holds the carrier of (pi_1 (TOP-REAL b₁),b₂) = {(Class (EqRel (TOP-REAL b₁),b₂),b₃)}

proof end;

registration

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
cluster FundamentalGroup (TOP-REAL a₁),a₂ -> non empty strict Group-like associative trivial ;
coherence

proof end;

end;