:: On the Continuity of Some Functions
:: by Artur Korni{\l}owicz
::
:: Received February 9, 2010
:: Copyright (c) 2010-2016 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, VALUED_0, TOPS_1, MEMBERED, XBOOLE_0, ARYTM_1,
COMPLEX1, ARYTM_3, XCMPLX_0, FINSEQ_1, EUCLID, PRE_TOPC, ORDINAL2,
TOPREALB, METRIC_1, TOPMETR, RCOMP_1, PCOMPS_1, FUNCT_3, FINSEQ_2,
RLVECT_1, RVSUM_1, SQUARE_1, FUNCT_4, VALUED_2, ALGSTR_0, SUBSET_1,
FUNCOP_1, PARTFUN1, CARD_3, FINSET_1, ZFMISC_1, TARSKI, CARD_1, TOPREALC,
NAT_1, XXREAL_0, VALUED_1, NUMBERS, ORDINAL4, STRUCT_0, XXREAL_1,
SUPINF_2, FUNCT_7, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, CARD_1, NUMBERS,
VALUED_0, VALUED_1, XCMPLX_0, XREAL_0, XXREAL_0, FUNCT_3, MEMBERED,
COMPLEX1, SQUARE_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, RCOMP_1, FUNCT_7,
VALUED_2, STRUCT_0, RVSUM_1, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1,
TOPMETR, T_0TOPSP, BORSUK_1, ALGSTR_0, RLVECT_1, RLTOPSP1, EUCLID,
WAYBEL18, TOPREAL9, TOPREALB;
constructors MONOID_0, FUNCT_7, FINSEQOP, VALUED_2, TOPREAL9, TOPREALB,
TOPS_1, COMPLEX1, T_0TOPSP, SQUARE_1, FUNCT_4, FUNCSDOM, CONVEX1,
WAYBEL18, BINOP_2, EUCLID_9, PARTFUN3, REAL_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, MEMBERED,
XCMPLX_0, XREAL_0, VALUED_2, PRE_TOPC, STRUCT_0, EUCLID, MONOID_0,
TOPREALB, XXREAL_0, NAT_1, TOPMETR, FUNCT_2, RVSUM_1, TOPREAL9, SQUARE_1,
RCOMP_1, TOPS_1, FUNCT_7, NUMBERS, RLVECT_1, FINSEQ_1, FUNCOP_1,
WAYBEL18, BORSUK_1, PRE_POLY, JORDAN2B, FINSEQ_2, PARTFUN3, EUCLID_9,
CARD_1, FINSET_1, RELSET_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
begin :: Preliminaries
reserve
x for object, X for set,
i, n, m for Nat,
r, s for Real,
c, c1, c2, d for Complex,
f, g for complex-valued Function,
g1 for n-element complex-valued FinSequence,
f1 for n-element real-valued FinSequence,
T for non empty TopSpace,
p for Element of TOP-REAL n;
theorem :: TOPREALC:1
for X being trivial set, Y being set st X,Y are_equipotent holds Y is trivial
;
registration
let r be Real;
cluster r^2 -> non negative;
end;
registration
let r be positive Real;
cluster r^2 -> positive;
end;
registration
cluster sqrt(0) -> zero;
end;
registration
let f be empty set;
cluster sqr(f) -> empty;
cluster |.f.| -> zero;
end;
theorem :: TOPREALC:2
f(#)(c1+c2) = f(#)c1 + f(#)c2;
theorem :: TOPREALC:3
f(#)(c1-c2) = f(#)c1 - f(#)c2;
theorem :: TOPREALC:4
f(/)c + g(/)c = (f+g)(/)c;
theorem :: TOPREALC:5
f(/)c - g(/)c = (f-g)(/)c;
theorem :: TOPREALC:6
c1 <> 0 & c2 <> 0 implies f(/)c1 - g(/)c2 = (f(#)c2-g(#)c1) (/) (c1*c2);
theorem :: TOPREALC:7
c <> 0 implies f(/)c - g = (f-c(#)g) (/) c;
theorem :: TOPREALC:8
(c-d)(#)f = c(#)f - d(#)f;
theorem :: TOPREALC:9
(f-g)^2 = (g-f)^2;
theorem :: TOPREALC:10
(f(/)c)^2 = f^2 (/) c^2;
theorem :: TOPREALC:11
|. (n|->r) - (n|->s) .| = sqrt(n) * |.r-s.|;
registration
let f,x,c;
cluster f+*(x,c) -> complex-valued;
end;
theorem :: TOPREALC:12
((0*n)+*(x,c))^2 = (0*n)+*(x,c^2);
theorem :: TOPREALC:13
x in Seg n implies |.(0*n)+*(x,r).| = |.r.|;
theorem :: TOPREALC:14
(0.REAL n)+*(x,0) = 0.REAL n;
theorem :: TOPREALC:15
mlt(f1,(0.REAL n)+*(x,r)) = (0.REAL n)+*(x,f1.x*r);
theorem :: TOPREALC:16
|(f1,(0.REAL n)+*(x,r))| = f1.x * r;
theorem :: TOPREALC:17
(g1+*(i,c)) - g1 = (0*n)+*(i,c-(g1.i));
theorem :: TOPREALC:18
|.<*r*>.| = |.r.|;
theorem :: TOPREALC:19
for f being real-valued FinSequence holds f is FinSequence of REAL;
theorem :: TOPREALC:20
for f being real-valued FinSequence st |.f.| <> 0
ex i being Nat st i in dom f & f.i <> 0;
theorem :: TOPREALC:21
for f being real-valued FinSequence holds |.Sum f.| <= Sum abs f;
theorem :: TOPREALC:22
for A being non empty 1-sorted, B being 1-element 1-sorted
for t being Point of B
for f being Function of A,B holds f = A --> t;
registration
let n be non zero Nat, i be Element of Seg n;
let T be real-membered non empty TopSpace;
cluster proj(Seg n --> T,i) -> real-valued;
end;
definition
let n; let p be Element of REAL n; let r;
redefine func p(/)r -> Element of REAL n;
end;
theorem :: TOPREALC:23
for p, q being Point of TOP-REAL m holds p in Ball(q,r) iff -p in Ball(-q,r);
definition
let S be 1-sorted;
attr S is complex-functions-membered means
:: TOPREALC:def 1
the carrier of S is complex-functions-membered;
attr S is real-functions-membered means
:: TOPREALC:def 2
the carrier of S is real-functions-membered;
end;
registration
let n;
cluster TOP-REAL n -> real-functions-membered;
end;
registration
cluster TOP-REAL 0 -> real-membered;
end;
registration
cluster TOP-REAL 0 -> trivial;
end;
registration
cluster real-functions-membered -> complex-functions-membered for 1-sorted;
end;
registration
cluster strict non empty real-functions-membered for 1-sorted;
end;
registration
let S be complex-functions-membered 1-sorted;
cluster the carrier of S -> complex-functions-membered;
end;
registration
let S be real-functions-membered 1-sorted;
cluster the carrier of S -> real-functions-membered;
end;
registration
cluster strict non empty real-functions-membered for TopSpace;
end;
registration
let S be complex-functions-membered TopSpace;
cluster -> complex-functions-membered for SubSpace of S;
end;
registration
let S be real-functions-membered TopSpace;
cluster -> real-functions-membered for SubSpace of S;
end;
definition
let X be complex-functions-membered set;
func (-)X -> complex-functions-membered set means
:: TOPREALC:def 3
for f being complex-valued Function holds -f in it iff f in X;
involutiveness;
end;
registration
let X be empty set;
cluster (-)X -> empty;
end;
registration
let X be non empty complex-functions-membered set;
cluster (-)X -> non empty;
end;
theorem :: TOPREALC:24
for X being complex-functions-membered set,
f being complex-valued Function holds
-f in X iff f in (-)X;
registration
let X be real-functions-membered set;
cluster (-)X -> real-functions-membered;
end;
theorem :: TOPREALC:25
for X being Subset of TOP-REAL n holds -X = (-)X;
definition
let n;
let X be Subset of TOP-REAL n;
redefine func (-)X -> Subset of TOP-REAL n;
end;
registration
let n;
let X be open Subset of TOP-REAL n;
cluster (-)X -> open for Subset of TOP-REAL n;
end;
definition
let R,S,T be non empty TopSpace, f be Function of [:R,S:],T;
let x be Point of [:R,S:];
redefine func f.x -> Point of T;
end;
definition
let R,S,T be non empty TopSpace, f be Function of [:R,S:],T;
let r be Point of R, s be Point of S;
redefine func f.(r,s) -> Point of T;
end;
definition
let n, p, r;
redefine func p + r -> Point of TOP-REAL n;
end;
definition
let n, p, r;
redefine func p - r -> Point of TOP-REAL n;
end;
definition
let n, p, r;
redefine func p (#) r -> Point of TOP-REAL n;
end;
definition
let n, p, r;
redefine func p (/) r -> Point of TOP-REAL n;
end;
definition
let n; let p1, p2 be Point of TOP-REAL n;
redefine func p1 (#) p2 -> Point of TOP-REAL n;
commutativity;
end;
definition
let n; let p be Point of TOP-REAL n;
redefine func sqr p -> Point of TOP-REAL n;
end;
definition
let n; let p1, p2 be Point of TOP-REAL n;
redefine func p1 /" p2 -> Point of TOP-REAL n;
end;
definition
let n, p, x, r;
redefine func p+*(x,r) -> Point of TOP-REAL n;
end;
theorem :: TOPREALC:26
for a, o being Point of TOP-REAL n holds
n <> 0 & a in Ball(o,r) implies |.Sum(a-o).| < n*r;
registration
let n;
cluster Euclid n -> real-functions-membered;
end;
theorem :: TOPREALC:27
for V being add-associative right_zeroed
right_complementable non empty addLoopStr, v,u being Element of V
holds v + u - u = v;
theorem :: TOPREALC:28
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u being Element of V
holds v - u + u = v;
theorem :: TOPREALC:29
for Y being complex-functions-membered set, f being PartFunc of X,Y holds
f[+]c = f<+>(dom f-->c);
theorem :: TOPREALC:30
for Y being complex-functions-membered set, f being PartFunc of X,Y holds
f[-]c = f<->(dom f-->c);
theorem :: TOPREALC:31
for Y being complex-functions-membered set, f being PartFunc of X,Y holds
f[#]c = f<#>(dom f-->c);
theorem :: TOPREALC:32
for Y being complex-functions-membered set, f being PartFunc of X,Y holds
f[/]c = f(dom f-->c);
registration
let D be complex-functions-membered set;
let f, g be FinSequence of D;
cluster f<++>g -> FinSequence-like;
cluster f<-->g -> FinSequence-like;
cluster f<##>g -> FinSequence-like;
cluster fg -> FinSequence-like;
end;
theorem :: TOPREALC:33
for f being Function of X,TOP-REAL n holds <->f is Function of X,TOP-REAL n;
theorem :: TOPREALC:34
for f being Function of TOP-REAL i,TOP-REAL n holds
f(-) is Function of TOP-REAL i,TOP-REAL n;
theorem :: TOPREALC:35
for f being Function of X,TOP-REAL n holds f[+]r is Function of X,TOP-REAL n;
theorem :: TOPREALC:36
for f being Function of X,TOP-REAL n holds
f[-]r is Function of X,TOP-REAL n;
theorem :: TOPREALC:37
for f being Function of X,TOP-REAL n holds f[#]r is Function of X,TOP-REAL n;
theorem :: TOPREALC:38
for f being Function of X,TOP-REAL n holds
f[/]r is Function of X,TOP-REAL n;
theorem :: TOPREALC:39
for f, g being Function of X,TOP-REAL n holds
f<++>g is Function of X,TOP-REAL n;
theorem :: TOPREALC:40
for f, g being Function of X,TOP-REAL n holds
f<-->g is Function of X,TOP-REAL n;
theorem :: TOPREALC:41
for f, g being Function of X,TOP-REAL n holds
f<##>g is Function of X,TOP-REAL n;
theorem :: TOPREALC:42
for f, g being Function of X,TOP-REAL n holds
fg is Function of X,TOP-REAL n;
theorem :: TOPREALC:43
for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds
f<+>g is Function of X,TOP-REAL n;
theorem :: TOPREALC:44
for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds
f<->g is Function of X,TOP-REAL n;
theorem :: TOPREALC:45
for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds
f<#>g is Function of X,TOP-REAL n;
theorem :: TOPREALC:46
for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds
fg is Function of X,TOP-REAL n;
definition
let n be Nat;
let T be non empty set;
let R be real-membered set;
let f be Function of T,R;
func incl(f,n) -> Function of T,TOP-REAL n means
:: TOPREALC:def 4
for t being Element of T holds it.t = n |-> f.t;
end;
theorem :: TOPREALC:47
for R being real-membered set for f being Function of T,R, t being Point of T
st x in Seg n holds incl(f,n).t.x = f.t;
theorem :: TOPREALC:48
for T being non empty set, R being real-membered set, f being Function of T,R
holds incl(f,0) = T --> 0;
theorem :: TOPREALC:49
for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds
f<+>g = f<++>incl(g,n);
theorem :: TOPREALC:50
for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds
f<->g = f<-->incl(g,n);
theorem :: TOPREALC:51
for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds
f<#>g = f<##>incl(g,n);
theorem :: TOPREALC:52
for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds
fg = fincl(g,n);
definition
let n;
func TIMES(n) -> Function of [:TOP-REAL n,TOP-REAL n:],TOP-REAL n means
:: TOPREALC:def 5
for x,y being Point of TOP-REAL n holds it.(x,y) = x(#)y;
end;
theorem :: TOPREALC:53
TIMES(0) = [:TOP-REAL 0,TOP-REAL 0:] --> 0.TOP-REAL 0;
theorem :: TOPREALC:54
for f, g being Function of T,TOP-REAL n holds f <##> g = TIMES(n).:(f,g);
definition
let m, n;
func PROJ(m,n) -> Function of TOP-REAL m,R^1 means
:: TOPREALC:def 6
for p being Element of TOP-REAL m holds it.p = p/.n;
end;
theorem :: TOPREALC:55
for p being Point of TOP-REAL m st n in dom p holds
PROJ(m,n).:Ball(p,r) = ]. p/.n-r , p/.n+r .[;
theorem :: TOPREALC:56
for m being non zero Nat for f being Function of T,R^1 holds
f = PROJ(m,m) * incl(f,m);
begin :: Continuity
registration
let T;
cluster non-empty continuous for Function of T,R^1;
end;
theorem :: TOPREALC:57
n in Seg m implies PROJ(m,n) is continuous;
theorem :: TOPREALC:58
n in Seg m implies PROJ(m,n) is open;
registration
let n,T;
let f be continuous Function of T,R^1;
cluster incl(f,n) -> continuous;
end;
registration
let n;
cluster TIMES(n) -> continuous;
end;
theorem :: TOPREALC:59
for f being Function of TOP-REAL m,TOP-REAL n st f is continuous holds
f(-) is continuous Function of TOP-REAL m,TOP-REAL n;
registration
let T; let f be continuous Function of T,R^1;
cluster -f -> continuous for Function of T,R^1;
end;
registration
let T; let f be non-empty continuous Function of T,R^1;
cluster f" -> continuous for Function of T,R^1;
end;
registration
let T; let f be continuous Function of T,R^1; let r;
cluster f+r -> continuous for Function of T,R^1;
cluster f-r -> continuous for Function of T,R^1;
cluster f(#)r -> continuous for Function of T,R^1;
cluster f(/)r -> continuous for Function of T,R^1;
end;
registration
let T; let f, g be continuous Function of T,R^1;
cluster f+g -> continuous for Function of T,R^1;
cluster f-g -> continuous for Function of T,R^1;
cluster f(#)g -> continuous for Function of T,R^1;
end;
registration
let T; let f be continuous Function of T,R^1;
let g be non-empty continuous Function of T,R^1;
cluster f /" g -> continuous for Function of T,R^1;
end;
registration
let n,T;
let f, g be continuous Function of T,TOP-REAL n;
cluster f<++>g -> continuous for Function of T,TOP-REAL n;
cluster f<-->g -> continuous for Function of T,TOP-REAL n;
cluster f<##>g -> continuous for Function of T,TOP-REAL n;
end;
registration
let n,T;
let f be continuous Function of T,TOP-REAL n;
let g be continuous Function of T,R^1;
cluster f<+>g -> continuous for Function of T,TOP-REAL n;
cluster f<->g -> continuous for Function of T,TOP-REAL n;
cluster f<#>g -> continuous for Function of T,TOP-REAL n;
end;
registration
let n,T;
let f be continuous Function of T,TOP-REAL n;
let g be non-empty continuous Function of T,R^1;
cluster fg -> continuous for Function of T,TOP-REAL n;
end;
registration
let n,T,r;
let f be continuous Function of T,TOP-REAL n;
cluster f[+]r -> continuous for Function of T,TOP-REAL n;
cluster f[-]r -> continuous for Function of T,TOP-REAL n;
cluster f[#]r -> continuous for Function of T,TOP-REAL n;
cluster f[/]r -> continuous for Function of T,TOP-REAL n;
end;
theorem :: TOPREALC:60
for r being non negative Real
for n being non zero Nat, p being Point of Tcircle(0.TOP-REAL n,r)
holds -p is Point of Tcircle(0.TOP-REAL n,r);
theorem :: TOPREALC:61
for r being non negative Real
for f being Function of Tcircle(0.TOP-REAL(n+1),r),TOP-REAL n holds
f(-) is Function of Tcircle(0.TOP-REAL(n+1),r),TOP-REAL n;
definition
let n be Nat, r be non negative Real;
let X be Subset of Tcircle(0.TOP-REAL(n+1),r);
redefine func (-)X -> Subset of Tcircle(0.TOP-REAL(n+1),r);
end;
registration
let m;
let r be non negative Real;
let X be open Subset of Tcircle(0.TOP-REAL(m+1),r);
cluster (-)X -> open for Subset of Tcircle(0.TOP-REAL(m+1),r);
end;
theorem :: TOPREALC:62
for r being non negative Real
for f being continuous Function of Tcircle(0.TOP-REAL(m+1),r),TOP-REAL m
holds f(-) is continuous Function of Tcircle(0.TOP-REAL(m+1),r),TOP-REAL m;