let T be monotone-convergence T_0-TopSpace; :: thesis: for R being T_0-TopSpace st R is_Retract_of T holds
R is monotone-convergence
let R be T_0-TopSpace; :: thesis: ( R is_Retract_of T implies R is monotone-convergence )
given c being continuous Function of R,T, r being continuous Function of T,R such that A1: r * c = id R ; :: according to WAYBEL25:def 1 :: thesis: R is monotone-convergence
let D be non empty directed Subset of (Omega R); :: according to WAYBEL25:def 4 :: thesis: ( ex_sup_of D, Omega R & ( for V being open Subset of R st sup D in V holds
D meets V ) )
A2: TopStruct(# the carrier of R, the topology of R #) = TopStruct(# the carrier of (Omega R), the topology of (Omega R) #) by Def2;
then reconsider DR = D as non empty Subset of R ;
A3: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
then reconsider f = c * r as Function of (Omega T),(Omega T) ;
reconsider rr = r as Function of (Omega T),(Omega R) by A3, A2;
A4: r .: (c .: D) = (r * c) .: DR by RELAT_1:126
.= D by A1, FUNCT_1:92 ;
reconsider cc = c as Function of (Omega R),(Omega T) by A3, A2;
cc is continuous by A3, A2, YELLOW12:36;
then A5: cc .: D is directed by YELLOW_2:15;
then A6: ex_sup_of cc .: D, Omega T by Def4;
f is continuous by A3, YELLOW12:36;
then A7: f preserves_sup_of cc .: D by A5, WAYBEL_0:def 37;
rr is continuous by A3, A2, YELLOW12:36;
then A8: rr preserves_sup_of cc .: D by A5, WAYBEL_0:def 37;
hence ex_sup_of D, Omega R by A6, A4; :: thesis: for V being open Subset of R st sup D in V holds
D meets V
A9: c . (sup D) = c . (r . (sup (cc .: D))) by A6, A4, A8
.= f . (sup (cc .: D)) by A3, FUNCT_2:15
.= sup (f .: (cc .: D)) by A6, A7
.= sup (cc .: D) by A4, RELAT_1:126 ;
let V be open Subset of R; :: thesis: ( sup D in V implies D meets V )
assume sup D in V ; :: thesis: D meets V
then A10: c . (sup D) in c .: V by FUNCT_2:35;
A11: c .: V c= r " V
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in c .: V or a in r " V )
assume a in c .: V ; :: thesis: a in r " V
then consider x being object such that
A12: x in the carrier of R and
A13: x in V and
A14: a = c . x by FUNCT_2:64;
reconsider x = x as Point of R by A12;
A15: a = c . x by A14;
r . a = (r * c) . x by A14, FUNCT_2:15
.= x by A1 ;
hence a in r " V by A13, A15, FUNCT_2:38; :: thesis: verum
end;
[#] R <> {} ;
then r " V is open by TOPS_2:43;
then c .: D meets r " V by A5, A11, A9, A10, Def4;
then consider d being object such that
A16: d in cc .: D and
A17: d in r " V by XBOOLE_0:3;
now :: thesis: ex a being set st
( a in D & a in V )
take a = r . d; :: thesis: ( a in D & a in V )
thus a in D by A4, A16, FUNCT_2:35; :: thesis: a in V
thus a in V by A17, FUNCT_2:38; :: thesis: verum
end;
hence D meets V by XBOOLE_0:3; :: thesis: verum