let n be 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
let t be Point of (TUnitSphere n); for f being Loop of t st rng f <> the carrier of (TUnitSphere n) holds
f is nullhomotopic
let f be Loop of t; ( rng f <> the carrier of (TUnitSphere n) implies f is nullhomotopic )
assume A1:
rng f <> the carrier of (TUnitSphere n)
; f is nullhomotopic
for x being object st x in rng f holds
x in the carrier of (TUnitSphere n)
;
then consider x being object such that
A2:
x in the carrier of (TUnitSphere n)
and
A3:
not x in rng f
by A1, TARSKI:2;
reconsider n1 = n + 1 as Nat ;
A4:
[#] (Tunit_circle n1) c= [#] (TOP-REAL n1)
by PRE_TOPC:def 4;
A5:
x in the carrier of (Tunit_circle n1)
by A2, MFOLD_2:def 4;
then reconsider p = x as Point of (TOP-REAL n1) by A4;
p in the carrier of (Tcircle ((0. (TOP-REAL n1)),1))
by A5, TOPREALB:def 7;
then A6:
p in Sphere ((0. (TOP-REAL n1)),1)
by TOPREALB:9;
then
- p in (Sphere ((0. (TOP-REAL n1)),1)) \ {p}
by Th3;
then reconsider S = (TOP-REAL n1) | ((Sphere ((0. (TOP-REAL n1)),1)) \ {p}) as non empty SubSpace of TOP-REAL n1 ;
A7:
[#] S = (Sphere ((0. (TOP-REAL n1)),1)) \ {p}
by PRE_TOPC:def 5;
then
stereographic_projection (S,p) is being_homeomorphism
by A6, MFOLD_2:31;
then A8:
TPlane (p,(0. (TOP-REAL n1))),S are_homeomorphic
by T_0TOPSP:def 1;
A9:
S is having_trivial_Fundamental_Group
by A8, Th13;
Tunit_circle n1 is SubSpace of TOP-REAL n1
;
then A10:
TUnitSphere n is SubSpace of TOP-REAL n1
by MFOLD_2:def 4;
(Sphere ((0. (TOP-REAL n1)),1)) \ {p} c= Sphere ((0. (TOP-REAL n1)),1)
by XBOOLE_1:36;
then
(Sphere ((0. (TOP-REAL n1)),1)) \ {p} c= the carrier of (Tcircle ((0. (TOP-REAL n1)),1))
by TOPREALB:9;
then
(Sphere ((0. (TOP-REAL n1)),1)) \ {p} c= the carrier of (Tunit_circle n1)
by TOPREALB:def 7;
then
(Sphere ((0. (TOP-REAL n1)),1)) \ {p} c= the carrier of (TUnitSphere n)
by MFOLD_2:def 4;
then reconsider S0 = S as non empty SubSpace of TUnitSphere n by A7, A10, TOPMETR:3;
0 in the carrier of I[01]
by BORSUK_1:43;
then A11:
0 in dom f
by FUNCT_2:def 1;
t,t are_connected
;
then A12:
( f is continuous & f . 0 = t & f . 1 = t )
by BORSUK_2:def 2;
then
t in rng f
by A11, FUNCT_1:3;
then A13:
not t in {p}
by A3, TARSKI:def 1;
A14: the carrier of (TUnitSphere n) =
the carrier of (Tunit_circle n1)
by MFOLD_2:def 4
.=
the carrier of (Tcircle ((0. (TOP-REAL n1)),1))
by TOPREALB:def 7
.=
Sphere ((0. (TOP-REAL n1)),1)
by TOPREALB:9
;
reconsider t0 = t as Point of S0 by A7, A14, A13, XBOOLE_0:def 5;
dom f = the carrier of I[01]
by FUNCT_2:def 1;
then reconsider f0 = f as Function of I[01],S0 by A7, A3, A14, FUNCT_2:2, ZFMISC_1:34;
A15:
t0,t0 are_connected
;
f0 is continuous
by JORDAN16:8;
then reconsider f0 = f as Loop of t0 by A12, A15, BORSUK_2:def 2;
f0 is nullhomotopic
by A9;
hence
f is nullhomotopic
by Th18; verum