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

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

proof end;

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 positive Real st Ball (p,r) c= P )

proof end;

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 ) )

proof end;

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 positive Real st Ball (q,r) c= f .: V )

proof end;

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 positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )

proof end;

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 positive Real st q = f . p holds
ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) )

proof end;

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 positive Real st Ball ((f . p),r) c= f .: V )

proof end;

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 positive Real ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )

proof end;

theorem :: TOPS_4:9

for n, m 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 positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) )

proof end;

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 positive Real st ].((f . p) - r),((f . p) + r).[ c= f .: V )

proof end;

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 positive Real ex V being open Subset of T st
( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )

proof end;

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 positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ )

proof end;

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 positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) )

proof end;

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 positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )

proof end;

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 positive Real st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) )

proof end;

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 positive Real st f .: (Ball (p,s)) c= V )

proof end;

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 positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) )

proof end;

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 positive Real ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )

proof end;

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 positive Real st f .: (Ball (p,s)) c= V )

proof end;

theorem :: TOPS_4:20

for n, m 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 positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) )

proof end;

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 positive Real ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )

proof end;

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 positive Real st f .: ].(p - s),(p + s).[ c= V )

proof end;

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 positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ )

proof end;

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 positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ )

proof end;

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 positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) )

proof end;