:: 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
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RELAT_1, FUNCT_1, TOPS_1, ARYTM_1, CONNSP_2, EUCLID, PRE_TOPC,
      ORDINAL2, METRIC_1, TOPMETR, RCOMP_1, PCOMPS_1, TARSKI, XBOOLE_0,
      NUMBERS, NAT_1, SUBSET_1, XXREAL_0, ARYTM_3, CARD_1, XXREAL_1, REAL_1;
 notations TARSKI, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1, NUMBERS,
      XCMPLX_0, XREAL_0, XXREAL_0, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1,
      CONNSP_2, METRIC_1, PCOMPS_1, TOPMETR, T_0TOPSP, EUCLID, TOPREAL9,
      TOPREALB;
 constructors TOPREAL9, TOPREALB, TOPS_1, T_0TOPSP, FUNCSDOM, PCOMPS_1;
 registrations XBOOLE_0, RELAT_1, MEMBERED, XREAL_0, PRE_TOPC, STRUCT_0,
      EUCLID, TOPREALB, XXREAL_0, METRIC_1, TOPMETR, TOPREAL9, PCOMPS_1,
      RCOMP_1, TOPGRP_1, VALUED_0, ORDINAL1;
 requirements SUBSET, REAL;


begin :: Open functions

reserve
  n, m for Nat,
  T for non empty TopSpace,
  M, M1, M2 for non empty MetrSpace;

theorem :: TOPS_4:1
  for A, B, S, T being TopSpace,
      f being Function of A,S, g being Function of B,T st
  the TopStruct of A = the TopStruct of B &
  the TopStruct of S = the TopStruct of T &
  f = g & f is open holds g is open;

theorem :: TOPS_4:2
  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
  ex r being positive Real st Ball(p,r) c= P;

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

theorem :: TOPS_4:4
  for f being Function of T,TopSpaceMetr(M) holds f is open iff
  for p being Point of T, V being open Subset of T,
      q being Point of M st q = f.p & p in V
  ex r being positive Real st Ball(q,r) c= f.:V;

theorem :: TOPS_4:5
  for f being Function of TopSpaceMetr(M),T holds f is open iff
  for p being Point of M, r being positive Real
  ex W being open Subset of T st f.p in W & W c= f.:Ball(p,r);

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

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

theorem :: TOPS_4:8
  for f being Function of TOP-REAL m,T holds f is open iff
  for p being Point of TOP-REAL m, r being positive Real
  ex W being open Subset of T st f.p in W & W c= f.:Ball(p,r);

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

theorem :: TOPS_4:10
  for f being Function of T,R^1 holds f is open iff
  for p being Point of T, V being open Subset of T st p in V
  ex r being positive Real st ].f.p-r,f.p+r.[ c= f.:V;

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

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

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

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

begin :: Continuous functions

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

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

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

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

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

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

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

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

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

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

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