:: Miscellaneous Facts about Open Functions and Continuous Functions
:: by Artur Korni{\l}owicz
::
:: Received February 9, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

theorem Th1: :: TOPS_4:1
for A, B, S, T being TopSpace
for f being Function of A,S
for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds
g is open
proofend;

theorem :: TOPS_4:2
for m being Nat
for P being Subset of (TOP-REAL m) holds
( P is open iff for p being Point of (TOP-REAL m) st p in P holds
ex r being real positive number st Ball (p,r) c= P )
proofend;

theorem Th3: :: TOPS_4:3
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is open iff for p being Point of X
for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V ) )
proofend;

theorem Th4: :: TOPS_4:4
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of T,(TopSpaceMetr M) holds
( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V )
proofend;

theorem Th5: :: TOPS_4:5
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of (TopSpaceMetr M),T holds
( f is open iff for p being Point of M
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
proofend;

theorem Th6: :: TOPS_4:6
for M1, M2 being non empty MetrSpace
for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is open iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) )
proofend;

theorem :: TOPS_4:7
for m being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL m) holds
( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V )
proofend;

theorem :: TOPS_4:8
for m being 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 real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
proofend;

theorem :: TOPS_4:9
for m, n being Nat
for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) )
proofend;

theorem :: TOPS_4:10
for T being non empty TopSpace
for f being Function of T,R^1 holds
( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V )
proofend;

theorem :: TOPS_4:11
for T being non empty TopSpace
for f being Function of R^1,T holds
( f is open iff for p being Point of R^1
for r being real positive number ex V being open Subset of T st
( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )
proofend;

theorem :: TOPS_4:12
for f being Function of R^1,R^1 holds
( f is open iff for p being Point of R^1
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ )
proofend;

theorem :: TOPS_4:13
for m being Nat
for f being Function of (TOP-REAL m),R^1 holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) )
proofend;

theorem :: TOPS_4:14
for m being Nat
for f being Function of R^1,(TOP-REAL m) holds
( f is open iff for p being Point of R^1
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )
proofend;

begin

theorem :: TOPS_4:15
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of T,(TopSpaceMetr M) holds
( f is continuous iff for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) )
proofend;

theorem :: TOPS_4:16
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of (TopSpaceMetr M),T holds
( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
proofend;

theorem Th17: :: TOPS_4:17
for M1, M2 being non empty MetrSpace
for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is continuous iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) )
proofend;

theorem :: TOPS_4:18
for m being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL m) holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )
proofend;

theorem :: TOPS_4:19
for m being Nat
for T being non empty TopSpace
for f being Function of (TOP-REAL m),T holds
( f is continuous iff for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
proofend;

theorem :: TOPS_4:20
for m, n being Nat
for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is continuous iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) )
proofend;

theorem :: TOPS_4:21
for T being non empty TopSpace
for f being Function of T,R^1 holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )
proofend;

theorem :: TOPS_4:22
for T being non empty TopSpace
for f being Function of R^1,T holds
( f is continuous iff for p being Point of R^1
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: ].(p - s),(p + s).[ c= V )
proofend;

theorem :: TOPS_4:23
for f being Function of R^1,R^1 holds
( f is continuous iff for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ )
proofend;

theorem :: TOPS_4:24
for m being Nat
for f being Function of (TOP-REAL m),R^1 holds
( f is continuous iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ )
proofend;

theorem :: TOPS_4:25
for m being Nat
for f being Function of R^1,(TOP-REAL m) holds
( f is continuous iff for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) )
proofend;