let T be non empty TopSpace; for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )
let s be Function of [:NAT,NAT:], the carrier of T; for x being Point of T holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )
let x be Point of T; ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )
set F = filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).));
A1:
( filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )
( filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x iff x in lim_filter (filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))) )
proof
thus
(
filter_image (
s,
<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
is_filter-finer_than NeighborhoodSystem x implies
x in lim_filter (filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))) )
;
( x in lim_filter (filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))) implies filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x )
assume
x in lim_filter (filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)))
;
filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x
then
ex
y being
Point of
T st
(
x = y &
filter_image (
s,
<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
is_filter-finer_than NeighborhoodSystem y )
;
hence
filter_image (
s,
<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
is_filter-finer_than NeighborhoodSystem x
;
verum
end;
hence
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )
by A1; verum