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