let T be non empty TopSpace; :: thesis: ( T is injective implies for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective )
assume A1:
T is injective
; :: thesis: for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective
let S be non empty SubSpace of T; :: thesis: ( S is_a_retract_of T implies S is injective )
assume
S is_a_retract_of T
; :: thesis: S is injective
then consider r being continuous Function of T,S such that
A2:
r is being_a_retraction
by BORSUK_1:def 20;
set p = incl S;
A3:
incl S is continuous
by TMAP_1:98;
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis: for f being Function of X,S st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
let F be Function of X,S; :: thesis: ( F is continuous implies for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F ) )
assume A4:
F is continuous
; :: thesis: for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F )
let Y be non empty TopSpace; :: thesis: ( X is SubSpace of Y implies ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F ) )
assume A5:
X is SubSpace of Y
; :: thesis: ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F )
reconsider f = (incl S) * F as Function of X,T ;
f is continuous
by A3, A4;
then consider g being Function of Y,T such that
A6:
g is continuous
and
A7:
g | the carrier of X = f
by A1, A5, Def5;
take G = r * g; :: thesis: ( G is continuous & G | the carrier of X = F )
thus
G is continuous
by A6; :: thesis: G | the carrier of X = F
A8:
the carrier of X c= the carrier of Y
by A5, BORSUK_1:35;
A9:
the carrier of S c= the carrier of T
by BORSUK_1:35;
A10: (dom G) /\ the carrier of X =
the carrier of Y /\ the carrier of X
by FUNCT_2:def 1
.=
the carrier of X
by A5, BORSUK_1:35, XBOOLE_1:28
;
A11:
dom F = the carrier of X
by FUNCT_2:def 1;
for x being set st x in dom F holds
F . x = G . x
proof
let x be
set ;
:: thesis: ( x in dom F implies F . x = G . x )
assume A12:
x in dom F
;
:: thesis: F . x = G . x
then A13:
x in the
carrier of
X
;
A14:
F . x in rng F
by A12, FUNCT_1:def 5;
then
F . x in the
carrier of
S
;
then reconsider y =
F . x as
Point of
T by A9;
A15:
F . x = r . y
by A2, A14, BORSUK_1:def 19;
A16:
f . x =
(incl S) . y
by A12, FUNCT_2:21
.=
F . x
by A14, TMAP_1:95
;
g . x = f . x
by A7, A12, FUNCT_1:72;
hence
F . x = G . x
by A8, A13, A15, A16, FUNCT_2:21;
:: thesis: verum
end;
hence
G | the carrier of X = F
by A10, A11, FUNCT_1:68; :: thesis: verum