let S, T be non empty complete lower TopLattice; :: thesis: for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds
f is continuous
reconsider BB = { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Def1;
let f be Function of S,T; :: thesis: ( ( for X being non empty Subset of S holds f preserves_inf_of X ) implies f is continuous )
assume A1: for X being non empty Subset of S holds f preserves_inf_of X ; :: thesis: f is continuous
now :: thesis: for A being Subset of T st A in BB holds
f " (A `) is closed
let A be Subset of T; :: thesis: ( A in BB implies f " (b1 `) is closed )
A2: ex_inf_of f " (A `),S by YELLOW_0:17;
A3: ex_inf_of A ` ,T by YELLOW_0:17;
A4: ex_inf_of f .: (f " (A `)),T by YELLOW_0:17;
assume A in BB ; :: thesis: f " (b1 `) is closed
then consider x being Element of T such that
A5: A = (uparrow x) ` ;
set s = inf (f " (uparrow x));
per cases ( f " (A `) = {} S or f " (A `) <> {} ) ;
suppose f " (A `) = {} S ; :: thesis: f " (b1 `) is closed
hence f " (A `) is closed ; :: thesis: verum
end;
suppose f " (A `) <> {} ; :: thesis: f " (b1 `) is closed
then f preserves_inf_of f " (A `) by A1;
then A6: f . (inf (f " (uparrow x))) = inf (f .: (f " (A `))) by A5, A2;
inf (A `) = x by A5, WAYBEL_0:39;
then A7: x <= f . (inf (f " (uparrow x))) by A6, A3, A4, FUNCT_1:75, YELLOW_0:35;
f " (A `) = uparrow (inf (f " (uparrow x)))
proof
thus f " (A `) c= uparrow (inf (f " (uparrow x))) :: according to XBOOLE_0:def 10 :: thesis: uparrow (inf (f " (uparrow x))) c= f " (A `)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f " (A `) or a in uparrow (inf (f " (uparrow x))) )
assume A8: a in f " (A `) ; :: thesis: a in uparrow (inf (f " (uparrow x)))
then reconsider a = a as Element of S ;
inf (f " (uparrow x)) <= a by A5, A8, YELLOW_2:22;
hence a in uparrow (inf (f " (uparrow x))) by WAYBEL_0:18; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in uparrow (inf (f " (uparrow x))) or a in f " (A `) )
assume A9: a in uparrow (inf (f " (uparrow x))) ; :: thesis: a in f " (A `)
then reconsider a = a as Element of S ;
f preserves_inf_of {(inf (f " (uparrow x))),a} by A1;
then A10: f . ((inf (f " (uparrow x))) "/\" a) = (f . (inf (f " (uparrow x)))) "/\" (f . a) by YELLOW_3:8;
inf (f " (uparrow x)) <= a by A9, WAYBEL_0:18;
then f . (inf (f " (uparrow x))) = (f . (inf (f " (uparrow x)))) "/\" (f . a) by A10, YELLOW_5:10;
then f . (inf (f " (uparrow x))) <= f . a by YELLOW_0:23;
then x <= f . a by A7, ORDERS_2:3;
then f . a in uparrow x by WAYBEL_0:18;
hence a in f " (A `) by A5, FUNCT_2:38; :: thesis: verum
end;
hence f " (A `) is closed by Th4; :: thesis: verum
end;
end;
end;
hence f is continuous by YELLOW_9:35; :: thesis: verum