let NTX, NTY be NTopSpace; :: thesis: for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st f is_continuous_at x & y = f . x holds
for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V
let x be Point of NTX; :: thesis: for y being Point of NTY
for f being Function of NTX,NTY st f is_continuous_at x & y = f . x holds
for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V
let y be Point of NTY; :: thesis: for f being Function of NTX,NTY st f is_continuous_at x & y = f . x holds
for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V
let f be Function of NTX,NTY; :: thesis: ( f is_continuous_at x & y = f . x implies for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V )
assume that
A1: f is_continuous_at x and
A2: y = f . x ; :: thesis: for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V
( U_FMT x is Filter of the carrier of NTX & x in lim_filter (U_FMT x) ) ;
then f . x in lim_filter (f,(U_FMT x)) by A1;
then consider z being Point of NTY such that
A3: f . x = z and
A4: filter_image (f,(U_FMT x)) is_filter-finer_than U_FMT z ;
A5: U_FMT y c= filter_image (f,(U_FMT x)) by A3, A4, A2, CARDFIL2:def 6;
for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V
proof
let V be Element of U_FMT y; :: thesis: ex W being Element of U_FMT x st f .: W c= V
V in filter_image (f,(U_FMT x)) by A5;
then V in { M where M is Subset of NTY : f " M in U_FMT x } by CARDFIL2:def 13;
then consider M being Subset of NTY such that
A6: V = M and
A7: f " M in U_FMT x ;
set W = f " M;
f .: (f " M) c= M by FUNCT_1:75;
hence ex W being Element of U_FMT x st f .: W c= V by A6, A7; :: thesis: verum
end;
hence for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ; :: thesis: verum