environ
vocabularies HIDDEN, PRE_TOPC, FUNCT_1, EUCLID, RELAT_1, ARYTM_1, BORSUK_2, GRAPH_1, ALGSTR_1, WAYBEL20, EQREL_1, NAT_1, XBOOLE_0, ARYTM_3, TOPALG_1, TOPS_2, TOPREALB, T_0TOPSP, STRUCT_0, BORSUK_1, FUNCOP_1, SUBSET_1, TOPALG_3, TARSKI, XREAL_0, FUNCT_2, XXREAL_0, ZFMISC_1, NUMBERS, RCOMP_1, ORDINAL2, CARD_1, XXREAL_1, CONNSP_2, TOPMETR, MFOLD_2, PARTFUN1, METRIC_1, CONVEX1, INCSP_1, RLTOPSP1, RVSUM_1, REAL_1, COMPLEX1, FINSEQ_1, MEASURE5, XXREAL_2, FINSET_1, FINSEQ_2, MFOLD_1, VALUED_0, SERIES_1, CARD_3, ORDINAL4, MEMBERED, SUPINF_2, TREAL_1, TOPREAL1, FUNCT_4, TOPALG_6, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, RELAT_1, COMPLEX1, FUNCOP_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, RVSUM_1, REAL_1, BINOP_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, NAT_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_2, BORSUK_1, CONNSP_2, TOPMETR, EUCLID, BORSUK_2, TOPALG_1, TOPALG_3, TOPREALB, VALUED_0, METRIC_1, TOPREAL9, TOPALG_2, RLTOPSP1, COMPTS_1, FINSEQ_1, TBSP_1, FINSEQ_2, METRIZTS, RLVECT_1, XXREAL_1, XXREAL_2, NAT_D, BORSUK_6, MEMBERED, RCOMP_1, MFOLD_1, MFOLD_2, TOPREAL1, FUNCT_4;
definitions TARSKI, XBOOLE_0, STRUCT_0, T_0TOPSP, BORSUK_2, MEMBERED;
theorems FUNCT_2, XBOOLE_0, ZFMISC_1, TOPALG_1, TARSKI, EQREL_1, BORSUK_2, BORSUK_6, TOPALG_3, JORDAN, TOPS_2, KNASTER, TOPREALC, PRE_TOPC, TSEP_1, TOPREALA, XXREAL_1, XXREAL_0, TOPMETR, MFOLD_2, BINOP_1, BORSUK_1, NAT_D, FUNCOP_1, TOPREALB, T_0TOPSP, TOPALG_2, RLTOPSP1, EUCLID, EUCLID_2, TOPREAL9, XBOOLE_1, FUNCT_1, JORDAN16, JGRAPH_8, RELAT_1, FINSEQ_1, FINSEQ_2, NAT_1, XREAL_1, MFOLD_1, METRIZTS, CARD_1, ORDINAL1, EUCLID_7, PARTFUN1, TBSP_1, METRIC_1, COMPLEX1, JORDAN2C, SUBSET_1, RELSET_1, XXREAL_2, FINSEQ_3, FINSEQ_4, VALUED_0, RFUNCT_2, TREAL_1, SYSREL, TOPREAL1, RAMSEY_1, CHORD, XCMPLX_1, BORSUK_3, COMPTS_1, HEINE, FUNCT_4, FUNCT_3, XREAL_0, XTUPLE_0, NUMBERS, RLVECT_1;
schemes NAT_1, FUNCT_1, FINSEQ_1;
registrations RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, BORSUK_1, EUCLID, BORSUK_2, TOPALG_1, PRE_TOPC, ZFMISC_1, TOPGRP_1, TOPMETR, RCOMP_3, XXREAL_2, TEX_1, TOPALG_3, FUNCT_2, FUNCT_1, FUNCOP_1, MFOLD_2, XBOOLE_0, RELAT_1, PARTFUN1, NAT_1, MONOID_0, VALUED_0, FINSET_1, FINSEQ_1, FINSEQ_2, NUMBERS, TOPALG_2, TOPREAL9, TBSP_1, MFOLD_1, BORSUK_3, TOPREAL6, TOPREALB, ORDINAL1, CARD_1;
constructors HIDDEN, BORSUK_6, BORSUK_3, TOPALG_3, SEQ_4, TOPREAL9, TOPREALB, MFOLD_2, BINOP_2, FUNCSDOM, CONVEX1, MONOID_0, COMPTS_1, TBSP_1, MFOLD_1, METRIZTS, NAT_D, TREAL_1, TOPREAL1, WAYBEL23, REAL_1, NUMBERS;
requirements HIDDEN, REAL, ARITHM, BOOLE, SUBSET, NUMERALS;
equalities STRUCT_0, TOPALG_1, RLVECT_1;
expansions TARSKI, XBOOLE_0, STRUCT_0, T_0TOPSP, BORSUK_2;
theorem Th2:
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)
theorem Th6:
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
theorem
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)
theorem Th12:
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) ) ) )
Lm1:
for T being TopStruct
for f being PartFunc of R^1,T st f = {} holds
f is parametrized-curve
definition
let T be non
empty TopStruct ;
let c1,
c2 be
with_endpoints Curve of
T;
pred c1,
c2 are_homotopic means
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
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;
::
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 ) );
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)
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
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) )