let T be Hausdorff TopLattice; for N being convergent net of T
for f being Function of T,T st f is continuous holds
f . (lim N) in Lim (f * N)
let N be convergent net of T; for f being Function of T,T st f is continuous holds
f . (lim N) in Lim (f * N)
let f be Function of T,T; ( f is continuous implies f . (lim N) in Lim (f * N) )
assume A1:
f is continuous
; f . (lim N) in Lim (f * N)
for V being a_neighborhood of f . (lim N) holds f * N is_eventually_in V
proof
let V be
a_neighborhood of
f . (lim N);
f * N is_eventually_in V
A2:
dom f = the
carrier of
T
by FUNCT_2:def 1;
consider O being
a_neighborhood of
lim N such that A3:
f .: O c= V
by A1, BORSUK_1:def 1;
lim N in Lim N
by YELLOW_6:def 17;
then
N is_eventually_in O
by YELLOW_6:def 15;
then consider s0 being
Element of
N such that A4:
for
j being
Element of
N st
s0 <= j holds
N . j in O
;
A5:
RelStr(# the
carrier of
(f * N), the
InternalRel of
(f * N) #)
= RelStr(# the
carrier of
N, the
InternalRel of
N #)
by Def8;
then reconsider s1 =
s0 as
Element of
(f * N) ;
take
s1
;
WAYBEL_0:def 11 for b1 being Element of the carrier of (f * N) holds
( not s1 <= b1 or (f * N) . b1 in V )
let j1 be
Element of
(f * N);
( not s1 <= j1 or (f * N) . j1 in V )
assume A6:
s1 <= j1
;
(f * N) . j1 in V
reconsider j =
j1 as
Element of
N by A5;
N . j in O
by A4, A5, A6, YELLOW_0:1;
then A7:
f . (N . j) in f .: O
by A2, FUNCT_1:def 6;
A8:
the
carrier of
(f * N) = dom the
mapping of
N
by A5, FUNCT_2:def 1;
(f * N) . j1 =
(f * the mapping of N) . j1
by Def8
.=
f . (N . j)
by A8, FUNCT_1:13
;
hence
(f * N) . j1 in V
by A3, A7;
verum
end;
hence
f . (lim N) in Lim (f * N)
by YELLOW_6:def 15; verum