let X be non empty TopSpace; :: thesis: for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let M be non empty MetrSpace; :: thesis: for f being Function of X,(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let f be Function of X,(TopSpaceMetr M); :: thesis: ( f is continuous implies for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open )
assume A1: f is continuous ; :: thesis: for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let r be Real; :: thesis: for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let u be Element of M; :: thesis: for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let P be Subset of (TopSpaceMetr M); :: thesis: ( P = Ball (u,r) implies f " P is open )
reconsider P9 = P as Subset of (TopSpaceMetr M) ;
assume P = Ball (u,r) ; :: thesis: f " P is open
then ( [#] (TopSpaceMetr M) <> {} & P9 is open ) by TOPMETR:14;
hence f " P is open by A1, TOPS_2:43; :: thesis: verum