let X be non empty TopSpace; for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st ( for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ) holds
f is continuous
let M be non empty MetrSpace; for f being Function of X,(TopSpaceMetr M) st ( for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ) holds
f is continuous
let f be Function of X,(TopSpaceMetr M); ( ( for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ) implies f is continuous )
assume A1:
for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open
; f is continuous
A2:
for P1 being Subset of (TopSpaceMetr M) st P1 is open holds
f " P1 is open
proof
let P1 be
Subset of
(TopSpaceMetr M);
( P1 is open implies f " P1 is open )
assume A3:
P1 is
open
;
f " P1 is open
for
x being
set holds
(
x in f " P1 iff ex
Q being
Subset of
X st
(
Q is
open &
Q c= f " P1 &
x in Q ) )
proof
let x be
set ;
( x in f " P1 iff ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) )
now ( x in f " P1 implies ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) )assume A4:
x in f " P1
;
ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q )then A5:
x in dom f
by FUNCT_1:def 7;
A6:
f . x in P1
by A4, FUNCT_1:def 7;
then reconsider u =
f . x as
Element of
M by TOPMETR:12;
consider r being
Real such that A7:
r > 0
and A8:
Ball (
u,
r)
c= P1
by A3, A6, TOPMETR:15;
reconsider r =
r as
Real ;
reconsider PB =
Ball (
u,
r) as
Subset of
(TopSpaceMetr M) by TOPMETR:12;
A9:
f " PB c= f " P1
by A8, RELAT_1:143;
f . x in Ball (
u,
r)
by A7, TBSP_1:11;
then
x in f " (Ball (u,r))
by A5, FUNCT_1:def 7;
hence
ex
Q being
Subset of
X st
(
Q is
open &
Q c= f " P1 &
x in Q )
by A1, A7, A9;
verum end;
hence
(
x in f " P1 iff ex
Q being
Subset of
X st
(
Q is
open &
Q c= f " P1 &
x in Q ) )
;
verum
end;
hence
f " P1 is
open
by TOPS_1:25;
verum
end;
[#] (TopSpaceMetr M) <> {}
;
hence
f is continuous
by A2, TOPS_2:43; verum