let T be non empty TopSpace; ( ( for t being Point of T
for f being Loop of t holds f is nullhomotopic ) implies T is having_trivial_Fundamental_Group )
assume A1:
for t being Point of T
for f being Loop of t holds f is nullhomotopic
; T is having_trivial_Fundamental_Group
for t being Point of T holds pi_1 (T,t) is trivial
proof
let t be
Point of
T;
pi_1 (T,t) is trivial
set C = the
constant Loop of
t;
the
carrier of
(pi_1 (T,t)) = {(Class ((EqRel (T,t)), the constant Loop of t))}
proof
set E =
EqRel (
T,
t);
hereby TARSKI:def 3,
XBOOLE_0:def 10 {(Class ((EqRel (T,t)), the constant Loop of t))} c= the carrier of (pi_1 (T,t))
let x be
object ;
( x in the carrier of (pi_1 (T,t)) implies x in {(Class ((EqRel (T,t)), the constant Loop of t))} )assume
x in the
carrier of
(pi_1 (T,t))
;
x in {(Class ((EqRel (T,t)), the constant Loop of t))}then consider P being
Loop of
t such that A2:
x = Class (
(EqRel (T,t)),
P)
by TOPALG_1:47;
P is
nullhomotopic
by A1;
then consider C1 being
constant Loop of
t such that A3:
P,
C1 are_homotopic
;
C1, the
constant Loop of
t are_homotopic
by Th5;
then
P, the
constant Loop of
t are_homotopic
by A3, BORSUK_6:79;
then
x = Class (
(EqRel (T,t)), the
constant Loop of
t)
by A2, TOPALG_1:46;
hence
x in {(Class ((EqRel (T,t)), the constant Loop of t))}
by TARSKI:def 1;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {(Class ((EqRel (T,t)), the constant Loop of t))} or x in the carrier of (pi_1 (T,t)) )
assume
x in {(Class ((EqRel (T,t)), the constant Loop of t))}
;
x in the carrier of (pi_1 (T,t))
then A4:
x = Class (
(EqRel (T,t)), the
constant Loop of
t)
by TARSKI:def 1;
the
constant Loop of
t in Loops t
by TOPALG_1:def 1;
then
x in Class (EqRel (T,t))
by A4, EQREL_1:def 3;
hence
x in the
carrier of
(pi_1 (T,t))
by TOPALG_1:def 5;
verum
end;
hence
pi_1 (
T,
t) is
trivial
;
verum
end;
hence
T is having_trivial_Fundamental_Group
; verum