let NTX, NTY be NTopSpace; :: thesis: for A being Subset of NTX
for B being Subset of NTY
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 & x is_adherent_point_of A & y = f . x & B = f .: A holds
y is_adherent_point_of B
let A be Subset of NTX; :: thesis: for B being Subset of NTY
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 & x is_adherent_point_of A & y = f . x & B = f .: A holds
y is_adherent_point_of B
let B be Subset of NTY; :: 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 & x is_adherent_point_of A & y = f . x & B = f .: A holds
y is_adherent_point_of B
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 & x is_adherent_point_of A & y = f . x & B = f .: A holds
y is_adherent_point_of B
let y be Point of NTY; :: thesis: for f being Function of NTX,NTY st f is_continuous_at x & x is_adherent_point_of A & y = f . x & B = f .: A holds
y is_adherent_point_of B
let f be Function of NTX,NTY; :: thesis: ( f is_continuous_at x & x is_adherent_point_of A & y = f . x & B = f .: A implies y is_adherent_point_of B )
assume that
A1: f is_continuous_at x and
A2: x is_adherent_point_of A and
A3: y = f . x and
A4: B = f .: A ; :: thesis: y is_adherent_point_of B
now :: thesis: for V being Element of U_FMT y holds V meets B
let V be Element of U_FMT y; :: thesis: V meets B
consider W being Element of U_FMT x such that
A5: f .: W c= V by A1, A3, Lm11;
A6: f .: (f " V) c= V by FUNCT_1:75;
now :: thesis: ( f " (f .: W) in U_FMT x & f " (f .: W) c= f " V )
now :: thesis: ( W c= f " (f .: W) & W in U_FMT x & U_FMT x is Filter of the carrier of NTX )
dom f = the carrier of NTX by FUNCT_2:def 1;
hence W c= f " (f .: W) by FUNCT_1:76; :: thesis: ( W in U_FMT x & U_FMT x is Filter of the carrier of NTX )
thus W in U_FMT x ; :: thesis: U_FMT x is Filter of the carrier of NTX
thus U_FMT x is Filter of the carrier of NTX ; :: thesis: verum
end;
hence f " (f .: W) in U_FMT x by CARD_FIL:def 1; :: thesis: f " (f .: W) c= f " V
thus f " (f .: W) c= f " V by A5, RELAT_1:143; :: thesis: verum
end;
then f " V in U_FMT x by CARD_FIL:def 1;
then f " V meets A by A2;
then not (f " V) /\ A is empty ;
then consider a being object such that
A7: a in (f " V) /\ A ;
now :: thesis: ( a in dom f & a in f " V )
( dom f = the carrier of NTX & a in A ) by A7, XBOOLE_0:def 4, FUNCT_2:def 1;
hence a in dom f ; :: thesis: a in f " V
thus a in f " V by A7, XBOOLE_0:def 4; :: thesis: verum
end;
then A8: f . a in f .: (f " V) by FUNCT_1:def 6;
( dom f = the carrier of NTX & a in A ) by A7, XBOOLE_0:def 4, FUNCT_2:def 1;
then f . a in f .: A by FUNCT_1:def 6;
hence V meets B by A4, A8, A6, XBOOLE_0:def 4; :: thesis: verum
end;
hence y is_adherent_point_of B ; :: thesis: verum