:: TOPALG_2 semantic presentation

registration

let c₁ be Nat;
cluster non empty convex Element of bool the carrier of (TOP-REAL a₁);
existence

proof end;

end;

definition

let c₁ be Nat;
let c₂ be SubSpace of TOP-REAL c₁;
attr a₂ is convex means :Def1: :: TOPALG_2:def 1
[#] a₂ is convex Subset of (TOP-REAL a₁);

end;

:: deftheorem Def1 defines convex TOPALG_2:def 1 :

registration

let c₁ be Nat;
cluster non empty convex -> non empty arcwise_connected SubSpace of TOP-REAL a₁;
coherence

proof end;

end;

registration

let c₁ be Nat;
cluster non empty strict arcwise_connected convex SubSpace of TOP-REAL a₁;
existence

proof end;

end;

theorem Th1: :: TOPALG_2:1

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

proof end;

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

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

Lemma4: the carrier of [:(TOP-REAL 1),I[01] :] = [:the carrier of (TOP-REAL 1),the carrier of I[01] :]
by BORSUK_1:def 5;

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

Lemma6: dom (id I[01] ) = the carrier of I[01]
by FUNCT_2:def 1;

definition

let c₂ be Nat;
let c₃ be non empty convex SubSpace of TOP-REAL c₂;
let c₄, c₅ be Point of c₃;
let c₆, c₇ be Path of c₄,c₅;
func ConvexHomotopy c₅,c₆ -> Function of [:I[01] ,I[01] :],a₂ means :Def2: :: TOPALG_2:def 2
for b₁, b₂ being Element of I[01]
for b₃, b₄ being Point of (TOP-REAL a₁) st b₃ = a₅ . b₁ & b₄ = a₆ . b₁ holds
a₇ . b₁,b₂ = ((1 - b₂) * b₃) + (b₂ * b₄);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ConvexHomotopy TOPALG_2:def 2 :

Lemma8: for b₁ being Nat
for b₂ being non empty convex SubSpace of TOP-REAL b₁
for b₃, b₄ being Point of b₂
for b₅, b₆ being Path of b₃,b₄ holds ConvexHomotopy b₅,b₆ is continuous

proof end;

Lemma9: for b₁ being Nat
for b₂ being non empty convex SubSpace of TOP-REAL b₁
for b₃, b₄ being Point of b₂
for b₅, b₆ being Path of b₃,b₄
for b₇ being Point of I[01] holds
( (ConvexHomotopy b₅,b₆) . b₇,0 = b₅ . b₇ & (ConvexHomotopy b₅,b₆) . b₇,1 = b₆ . b₇ & ( for b₈ being Point of I[01] holds
( (ConvexHomotopy b₅,b₆) . 0,b₈ = b₃ & (ConvexHomotopy b₅,b₆) . 1,b₈ = b₄ ) ) )

proof end;

theorem Th2: :: TOPALG_2:2

for b₁ being Nat
for b₂ being non empty convex SubSpace of TOP-REAL b₁
for b₃, b₄ being Point of b₂
for b₅, b₆ being Path of b₃,b₄ holds b₅,b₆ are_homotopic

proof end;

definition

let c₂ be Nat;
let c₃ be non empty convex SubSpace of TOP-REAL c₂;
let c₄, c₅ be Point of c₃;
let c₆, c₇ be Path of c₄,c₅;
redefine func ConvexHomotopy as ConvexHomotopy c₅,c₆ -> Homotopy of a₅,a₆;
coherence

proof end;

end;

registration

let c₂ be Nat;
let c₃ be non empty convex SubSpace of TOP-REAL c₂;
let c₄, c₅ be Point of c₃;
let c₆, c₇ be Path of c₄,c₅;
cluster -> continuous Homotopy of a₅,a₆;
coherence

proof end;

end;

theorem Th3: :: TOPALG_2:3

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

proof end;

registration

let c₂ be Nat;
let c₃ be non empty convex SubSpace of TOP-REAL c₂;
let c₄ be Point of c₃;
cluster FundamentalGroup a₂,a₃ -> trivial ;
coherence

proof end;

end;

theorem Th4: :: TOPALG_2:4

for b₁ being real number holds Proj |[b₁]|,1 = b₁

proof end;

registration

cluster -> real-membered SubSpace of R^1 ;
coherence ;

end;

theorem Th5: :: TOPALG_2:5

for b₁, b₂ being real number st b₁ <= b₂ holds
[.b₁,b₂.] = { (((1 - b₃) * b₁) + (b₃ * b₂)) where B is Real : ( 0 <= b₃ & b₃ <= 1 ) }

proof end;

theorem Th6: :: TOPALG_2:6

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

proof end;

theorem Th7: :: TOPALG_2:7

for b₁ being Function of [:R^1 ,I[01] :],R^1 st ( for b₂ being Point of R^1
for b₃ being Point of I[01] holds b₁ . b₂,b₃ = b₃ * b₂ ) holds
b₁ is continuous

proof end;

definition

let c₂ be Subset of R^1 ;
attr a₁ is convex means :Def3: :: TOPALG_2:def 3
for b₁, b₂ being Point of R^1 st b₁ in a₁ & b₂ in a₁ holds
[.b₁,b₂.] c= a₁;

end;

:: deftheorem Def3 defines convex TOPALG_2:def 3 :

registration

cluster non empty convex Element of bool the carrier of R^1 ;
existence

proof end;

cluster empty -> convex Element of bool the carrier of R^1 ;
coherence

proof end;

end;

theorem Th8: :: TOPALG_2:8

for b₁, b₂ being real number holds [.b₁,b₂.] is convex Subset of R^1

proof end;

theorem Th9: :: TOPALG_2:9

for b₁, b₂ being real number holds ].b₁,b₂.[ is convex Subset of R^1

proof end;

theorem Th10: :: TOPALG_2:10

for b₁, b₂ being real number holds [.b₁,b₂.[ is convex Subset of R^1

proof end;

theorem Th11: :: TOPALG_2:11

for b₁, b₂ being real number holds ].b₁,b₂.] is convex Subset of R^1

proof end;

definition

let c₂ be SubSpace of R^1 ;
attr a₁ is convex means :Def4: :: TOPALG_2:def 4
[#] a₁ is convex Subset of R^1 ;

end;

:: deftheorem Def4 defines convex TOPALG_2:def 4 :

Lemma18: for b₁ being SubSpace of R^1 st b₁ = R^1 holds
b₁ is convex

proof end;

registration

cluster non empty strict real-membered convex SubSpace of R^1 ;
existence

proof end;

end;

definition

redefine func R^1 as R^1 -> strict convex SubSpace of R^1 ;
coherence by Lemma18, TSEP_1:2;

end;

theorem Th12: :: TOPALG_2:12

for b₁ being non empty convex SubSpace of R^1
for b₂, b₃ being Point of b₁ holds [.b₂,b₃.] c= the carrier of b₁

proof end;

registration

cluster non empty convex -> non empty arcwise_connected real-membered SubSpace of R^1 ;
coherence

proof end;

end;

theorem Th13: :: TOPALG_2:13

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

proof end;

theorem Th14: :: TOPALG_2:14

I[01] is convex by Th13, TOPMETR:27;

theorem Th15: :: TOPALG_2:15

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

proof end;

definition

let c₂ be non empty convex SubSpace of R^1 ;
let c₃, c₄ be Point of c₂;
let c₅, c₆ be Path of c₃,c₄;
func R1Homotopy c₄,c₅ -> Function of [:I[01] ,I[01] :],a₁ means :Def5: :: TOPALG_2: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 R1Homotopy TOPALG_2:def 5 :

Lemma23: for b₁ being non empty convex SubSpace of R^1
for b₂, b₃ being Point of b₁
for b₄, b₅ being Path of b₂,b₃ holds R1Homotopy b₄,b₅ is continuous

proof end;

Lemma24: for b₁ being non empty convex SubSpace of R^1
for b₂, b₃ being Point of b₁
for b₄, b₅ being Path of b₂,b₃
for b₆ being Point of I[01] holds
( (R1Homotopy b₄,b₅) . b₆,0 = b₄ . b₆ & (R1Homotopy b₄,b₅) . b₆,1 = b₅ . b₆ & ( for b₇ being Point of I[01] holds
( (R1Homotopy b₄,b₅) . 0,b₇ = b₂ & (R1Homotopy b₄,b₅) . 1,b₇ = b₃ ) ) )

proof end;

theorem Th16: :: TOPALG_2:16

for b₁ being non empty convex SubSpace of R^1
for b₂, b₃ being Point of b₁
for b₄, b₅ being Path of b₂,b₃ holds b₄,b₅ are_homotopic

proof end;

definition

let c₂ be non empty convex SubSpace of R^1 ;
let c₃, c₄ be Point of c₂;
let c₅, c₆ be Path of c₃,c₄;
redefine func R1Homotopy as R1Homotopy c₄,c₅ -> Homotopy of a₄,a₅;
coherence

proof end;

end;

registration

let c₂ be non empty convex SubSpace of R^1 ;
let c₃, c₄ be Point of c₂;
let c₅, c₆ be Path of c₃,c₄;
cluster -> continuous Homotopy of a₄,a₅;
coherence

proof end;

end;

theorem Th17: :: TOPALG_2:17

for b₁ being non empty convex SubSpace of R^1
for b₂ being Point of b₁
for b₃ being Loop of b₂ holds the carrier of (pi_1 b₁,b₂) = {(Class (EqRel b₁,b₂),b₃)}

proof end;

registration

let c₂ be non empty convex SubSpace of R^1 ;
let c₃ be Point of c₂;
cluster FundamentalGroup a₁,a₂ -> trivial ;
coherence

proof end;

end;

theorem Th18: :: TOPALG_2:18

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃, b₄ being Point of (Closed-Interval-TSpace b₁,b₂)
for b₅, b₆ being Path of b₃,b₄ holds b₅,b₆ are_homotopic

proof end;

theorem Th19: :: TOPALG_2:19

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃ being Point of (Closed-Interval-TSpace b₁,b₂)
for b₄ being Loop of b₃ holds the carrier of (pi_1 (Closed-Interval-TSpace b₁,b₂),b₃) = {(Class (EqRel (Closed-Interval-TSpace b₁,b₂),b₃),b₄)}

proof end;

theorem Th20: :: TOPALG_2:20

for b₁, b₂ being Point of I[01]
for b₃, b₄ being Path of b₁,b₂ holds b₃,b₄ are_homotopic by Th14, Th16;

theorem Th21: :: TOPALG_2:21

for b₁ being Point of I[01]
for b₂ being Loop of b₁ holds the carrier of (pi_1 I[01] ,b₁) = {(Class (EqRel I[01] ,b₁),b₂)} by Th14, Th17;

registration

let c₂ be Point of I[01] ;
cluster FundamentalGroup I[01] ,a₁ -> trivial ;
coherence

proof end;

end;