:: by Artur Korni{\l}owicz

::

:: Received February 9, 2010

:: Copyright (c) 2010-2017 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

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 )

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

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 )

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

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

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 )

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

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

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 )

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

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

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

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

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

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 )

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

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

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 )

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

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

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 )

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

( 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).[ )

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

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;