let m be Nat; for T being non empty TopSpace
for f being Function of (TOP-REAL m),T holds
( f is open iff for p being Point of (TOP-REAL m)
for r being positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
let T be non empty TopSpace; for f being Function of (TOP-REAL m),T holds
( f is open iff for p being Point of (TOP-REAL m)
for r being positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
let f be Function of (TOP-REAL m),T; ( f is open iff for p being Point of (TOP-REAL m)
for r being positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
A1:
TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m)
by EUCLID:def 8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),T ;
A2:
TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #)
;
thus
( f is open implies for p being Point of (TOP-REAL m)
for r being positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
( ( for p being Point of (TOP-REAL m)
for r being positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) ) implies f is open )proof
assume A3:
f is
open
;
for p being Point of (TOP-REAL m)
for r being positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
let p be
Point of
(TOP-REAL m);
for r being positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )let r be
positive Real;
ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
reconsider q =
p as
Point of
(Euclid m) by EUCLID:67;
f1 is
open
by A3, A1, A2, Th1;
then consider W being
open Subset of
T such that A4:
(
f1 . p in W &
W c= f1 .: (Ball (q,r)) )
by Th5;
Ball (
p,
r)
= Ball (
q,
r)
by TOPREAL9:13;
hence
ex
W being
open Subset of
T st
(
f . p in W &
W c= f .: (Ball (p,r)) )
by A4;
verum
end;
assume A5:
for p being Point of (TOP-REAL m)
for r being positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
; f is open
for p being Point of (Euclid m)
for r being positive Real ex W being open Subset of T st
( f1 . p in W & W c= f1 .: (Ball (p,r)) )
then
f1 is open
by Th5;
hence
f is open
by A1, A2, Th1; verum