:: Number-Valued Functions
:: by Library Committee
::
:: Received November 22, 2007
:: Copyright (c) 2007-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 NUMBERS, RELAT_1, TARSKI, XBOOLE_0, FUNCT_1, MEMBERED, SUBSET_1,
XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, INT_1, ORDINAL1, FUNCOP_1, FUNCT_4,
ZFMISC_1, ORDINAL2, ARYTM_3, NAT_1, PARTFUN1, FUNCT_2, SETFAM_1, CARD_1,
VALUED_0, PBOOLE, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE,
ORDINAL1, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4,
NUMBERS, MEMBERED, XCMPLX_0, XREAL_0, XXREAL_0, RAT_1, NAT_1, INT_1;
constructors XCMPLX_0, RAT_1, MEMBERED, FUNCOP_1, FUNCT_4, XXREAL_0, PARTFUN1,
NAT_1, SETFAM_1, RELSET_1, NUMBERS;
registrations MEMBERED, RELAT_1, FUNCOP_1, XREAL_0, RAT_1, ORDINAL1, INT_1,
FUNCT_1, XBOOLE_0, RELSET_1, FUNCT_2, SETFAM_1, SUBSET_1, PBOOLE, NAT_1;
requirements SUBSET, BOOLE, NUMERALS;
begin
definition
let f be Relation;
attr f is complex-valued means
:: VALUED_0:def 1
rng f c= COMPLEX;
attr f is ext-real-valued means
:: VALUED_0:def 2
rng f c= ExtREAL;
attr f is real-valued means
:: VALUED_0:def 3
rng f c= REAL;
::$CD 2
attr f is natural-valued means
:: VALUED_0:def 6
rng f c= NAT;
end;
registration
cluster natural-valued -> INT-valued for Relation;
cluster INT-valued -> RAT-valued for Relation;
cluster INT-valued -> real-valued for Relation;
cluster RAT-valued -> real-valued for Relation;
cluster real-valued -> ext-real-valued for Relation;
cluster real-valued -> complex-valued for Relation;
cluster natural-valued -> RAT-valued for Relation;
cluster natural-valued -> real-valued for Relation;
end;
registration
cluster empty -> natural-valued for Relation;
end;
registration
cluster natural-valued for Function;
end;
registration
let R be complex-valued Relation;
cluster rng R -> complex-membered;
end;
registration
let R be ext-real-valued Relation;
cluster rng R -> ext-real-membered;
end;
registration
let R be real-valued Relation;
cluster rng R -> real-membered;
end;
registration
let R be RAT-valued Relation;
cluster rng R -> rational-membered;
end;
registration
let R be INT-valued Relation;
cluster rng R -> integer-membered;
end;
registration
let R be natural-valued Relation;
cluster rng R -> natural-membered;
end;
reserve x,y for object,X for set,
f for Function,
R,S for Relation;
theorem :: VALUED_0:1
for S being complex-valued Relation st R c= S holds R is complex-valued;
theorem :: VALUED_0:2
for S being ext-real-valued Relation st R c= S holds R is ext-real-valued;
theorem :: VALUED_0:3
for S being real-valued Relation st R c= S holds R is real-valued;
theorem :: VALUED_0:4
for S being RAT-valued Relation st R c= S holds R is RAT-valued;
theorem :: VALUED_0:5
for S being INT-valued Relation st R c= S holds R is INT-valued;
theorem :: VALUED_0:6
for S being natural-valued Relation st R c= S holds R is natural-valued;
registration
let R be complex-valued Relation;
cluster -> complex-valued for Subset of R;
end;
registration
let R be ext-real-valued Relation;
cluster -> ext-real-valued for Subset of R;
end;
registration
let R be real-valued Relation;
cluster -> real-valued for Subset of R;
end;
registration
let R be RAT-valued Relation;
cluster -> RAT-valued for Subset of R;
end;
registration
let R be INT-valued Relation;
cluster -> INT-valued for Subset of R;
end;
registration
let R be natural-valued Relation;
cluster -> natural-valued for Subset of R;
end;
registration
let R,S be complex-valued Relation;
cluster R \/ S -> complex-valued;
end;
registration
let R,S be ext-real-valued Relation;
cluster R \/ S -> ext-real-valued;
end;
registration
let R,S be real-valued Relation;
cluster R \/ S -> real-valued;
end;
registration
let R,S be RAT-valued Relation;
cluster R \/ S -> RAT-valued;
end;
registration
let R,S be INT-valued Relation;
cluster R \/ S -> INT-valued;
end;
registration
let R,S be natural-valued Relation;
cluster R \/ S -> natural-valued;
end;
registration
let R be complex-valued Relation;
let S;
cluster R /\ S -> complex-valued;
cluster R \ S -> complex-valued;
end;
registration
let R be ext-real-valued Relation;
let S;
cluster R /\ S -> ext-real-valued;
cluster R \ S -> ext-real-valued;
end;
registration
let R be real-valued Relation;
let S;
cluster R /\ S -> real-valued;
cluster R \ S -> real-valued;
end;
registration
let R be RAT-valued Relation;
let S;
cluster R /\ S -> RAT-valued;
cluster R \ S -> RAT-valued;
end;
registration
let R be INT-valued Relation;
let S;
cluster R /\ S -> INT-valued;
cluster R \ S -> INT-valued;
end;
registration
let R be natural-valued Relation;
let S;
cluster R /\ S -> natural-valued;
cluster R \ S -> natural-valued;
end;
registration
let R,S be complex-valued Relation;
cluster R \+\ S -> complex-valued;
end;
registration
let R,S be ext-real-valued Relation;
cluster R \+\ S -> ext-real-valued;
end;
registration
let R,S be real-valued Relation;
cluster R \+\ S -> real-valued;
end;
registration
let R,S be RAT-valued Relation;
cluster R \+\ S -> RAT-valued;
end;
registration
let R,S be INT-valued Relation;
cluster R \+\ S -> INT-valued;
end;
registration
let R,S be natural-valued Relation;
cluster R \+\ S -> natural-valued;
end;
registration
let R be complex-valued Relation;
let X;
cluster R.:X -> complex-membered;
end;
registration
let R be ext-real-valued Relation;
let X;
cluster R.:X -> ext-real-membered;
end;
registration
let R be real-valued Relation;
let X;
cluster R.:X -> real-membered;
end;
registration
let R be RAT-valued Relation;
let X;
cluster R.:X -> rational-membered;
end;
registration
let R be INT-valued Relation;
let X;
cluster R.:X -> integer-membered;
end;
registration
let R be natural-valued Relation;
let X;
cluster R.:X -> natural-membered;
end;
registration
let R be complex-valued Relation;
let x;
cluster Im(R,x) -> complex-membered;
end;
registration
let R be ext-real-valued Relation;
let x;
cluster Im(R,x) -> ext-real-membered;
end;
registration
let R be real-valued Relation;
let x;
cluster Im(R,x) -> real-membered;
end;
registration
let R be RAT-valued Relation;
let x;
cluster Im(R,x) -> rational-membered;
end;
registration
let R be INT-valued Relation;
let x;
cluster Im(R,x) -> integer-membered;
end;
registration
let R be natural-valued Relation;
let x;
cluster Im(R,x) -> natural-membered;
end;
registration
let R be complex-valued Relation;
let X;
cluster R|X -> complex-valued;
end;
registration
let R be ext-real-valued Relation;
let X;
cluster R|X -> ext-real-valued;
end;
registration
let R be real-valued Relation;
let X;
cluster R|X -> real-valued;
end;
registration
let R be RAT-valued Relation;
let X;
cluster R|X -> RAT-valued;
end;
registration
let R be INT-valued Relation;
let X;
cluster R|X -> INT-valued;
end;
registration
let R be natural-valued Relation;
let X;
cluster R|X -> natural-valued;
end;
registration
let X be complex-membered set;
cluster id X -> complex-valued;
end;
registration
let X be ext-real-membered set;
cluster id X -> ext-real-valued;
end;
registration
let X be real-membered set;
cluster id X -> real-valued;
end;
registration
let X be rational-membered set;
cluster id X -> RAT-valued;
end;
registration
let X be integer-membered set;
cluster id X -> INT-valued;
end;
registration
let X be natural-membered set;
cluster id X -> natural-valued;
end;
registration
let R;
let S be complex-valued Relation;
cluster R*S -> complex-valued;
end;
registration
let R;
let S be ext-real-valued Relation;
cluster R*S -> ext-real-valued;
end;
registration
let R;
let S be real-valued Relation;
cluster R*S -> real-valued;
end;
registration
let R;
let S be RAT-valued Relation;
cluster R*S -> RAT-valued;
end;
registration
let R;
let S be INT-valued Relation;
cluster R*S -> INT-valued;
end;
registration
let R;
let S be natural-valued Relation;
cluster R*S -> natural-valued;
end;
definition
let f be Function;
redefine attr f is complex-valued means
:: VALUED_0:def 7
for x st x in dom f holds f.x is complex;
redefine attr f is ext-real-valued means
:: VALUED_0:def 8
for x st x in dom f holds f.x is ext-real;
redefine attr f is real-valued means
:: VALUED_0:def 9
for x st x in dom f holds f.x is real;
::$CD 2
redefine attr f is natural-valued means
:: VALUED_0:def 12
for x st x in dom f holds f.x is natural;
end;
theorem :: VALUED_0:7
f is complex-valued iff for x holds f.x is complex;
theorem :: VALUED_0:8
f is ext-real-valued iff for x holds f.x is ext-real;
theorem :: VALUED_0:9
f is real-valued iff for x holds f.x is real;
theorem :: VALUED_0:10
f is RAT-valued iff for x holds f.x is rational;
theorem :: VALUED_0:11
f is INT-valued iff for x holds f.x is integer;
theorem :: VALUED_0:12
f is natural-valued iff for x holds f.x is natural;
registration
let f be complex-valued Function;
let x be object;
cluster f.x -> complex;
end;
registration
let f be ext-real-valued Function;
let x be object;
cluster f.x -> ext-real;
end;
registration
let f be real-valued Function;
let x be object;
cluster f.x -> real;
end;
registration
let f be RAT-valued Function;
let x be object;
cluster f.x -> rational;
end;
registration
let f be INT-valued Function;
let x be object;
cluster f.x -> integer;
end;
registration
let f be natural-valued Function;
let x be object;
cluster f.x -> natural;
end;
registration
let X;
let x be Complex;
cluster X --> x -> complex-valued;
end;
registration
let X;
let x be ExtReal;
cluster X --> x -> ext-real-valued;
end;
registration
let X;
let x be Real;
cluster X --> x -> real-valued;
end;
registration
let X;
let x be Rational;
cluster X --> x -> RAT-valued;
end;
registration
let X;
let x be Integer;
cluster X --> x -> INT-valued;
end;
registration
let X;
let x be Nat;
cluster X --> x -> natural-valued;
end;
registration
let f,g be complex-valued Function;
cluster f +* g -> complex-valued;
end;
registration
let f,g be ext-real-valued Function;
cluster f +* g -> ext-real-valued;
end;
registration
let f,g be real-valued Function;
cluster f +* g -> real-valued;
end;
registration
let f,g be RAT-valued Function;
cluster f +* g -> RAT-valued;
end;
registration
let f,g be INT-valued Function;
cluster f +* g -> INT-valued;
end;
registration
let f,g be natural-valued Function;
cluster f +* g -> natural-valued;
end;
registration
let x;
let y be Complex;
cluster x .--> y -> complex-valued;
end;
registration
let x;
let y be ExtReal;
cluster x .--> y -> ext-real-valued;
end;
registration
let x;
let y be Real;
cluster x .--> y -> real-valued;
end;
registration
let x;
let y be Rational;
cluster x .--> y -> RAT-valued;
end;
registration
let x;
let y be Integer;
cluster x .--> y -> INT-valued;
end;
registration
let x;
let y be Nat;
cluster x .--> y -> natural-valued;
end;
registration
let X;
let Y be complex-membered set;
cluster -> complex-valued for Relation of X,Y;
end;
registration
let X;
let Y be ext-real-membered set;
cluster -> ext-real-valued for Relation of X,Y;
end;
registration
let X;
let Y be real-membered set;
cluster -> real-valued for Relation of X,Y;
end;
registration
let X;
let Y be rational-membered set;
cluster -> RAT-valued for Relation of X,Y;
end;
registration
let X;
let Y be integer-membered set;
cluster -> INT-valued for Relation of X,Y;
end;
registration
let X;
let Y be natural-membered set;
cluster -> natural-valued for Relation of X,Y;
end;
registration
let X;
let Y be complex-membered set;
cluster [:X,Y:] -> complex-valued;
end;
registration
let X;
let Y be ext-real-membered set;
cluster [:X,Y:] -> ext-real-valued;
end;
registration
let X;
let Y be real-membered set;
cluster [:X,Y:] -> real-valued;
end;
registration
let X;
let Y be rational-membered set;
cluster [:X,Y:] -> RAT-valued;
end;
registration
let X;
let Y be integer-membered set;
cluster [:X,Y:] -> INT-valued;
end;
registration
let X;
let Y be natural-membered set;
cluster [:X,Y:] -> natural-valued;
end;
:::notation
::: synonym f is non-zero for f is non-empty;
:::end;
registration
cluster non empty constant natural-valued INT-valued RAT-valued for Function;
end;
theorem :: VALUED_0:13
for f being non empty constant complex-valued Function ex r being
Complex st for x being object st x in dom f holds f.x = r;
theorem :: VALUED_0:14
for f being non empty constant ext-real-valued Function ex r being
ExtReal st for x being object st x in dom f holds f.x = r;
theorem :: VALUED_0:15
for f being non empty constant real-valued Function ex r being Real
st for x being object st x in dom f holds f.x = r;
theorem :: VALUED_0:16
for f being non empty constant RAT-valued Function ex r being
Rational st for x being object st x in dom f holds f.x = r;
theorem :: VALUED_0:17
for f being non empty constant INT-valued Function ex r being
Integer st for x being object st x in dom f holds f.x = r;
theorem :: VALUED_0:18
for f being non empty constant natural-valued Function ex r being
Nat st for x being object st x in dom f holds f.x = r;
begin :: inecreasing & decreasing functions
reserve e1,e2 for ExtReal;
definition
let f be ext-real-valued Function;
attr f is increasing means
:: VALUED_0:def 13
for e1,e2 st e1 in dom f & e2 in dom f & e1 < e2 holds f.e1 < f.e2;
attr f is decreasing means
:: VALUED_0:def 14
for e1,e2 st e1 in dom f & e2 in dom f & e1 < e2 holds f.e1 > f.e2;
attr f is non-decreasing means
:: VALUED_0:def 15
for e1,e2 st e1 in dom f & e2 in dom f & e1 <= e2 holds f.e1 <= f.e2;
attr f is non-increasing means
:: VALUED_0:def 16
for e1,e2 st e1 in dom f & e2 in dom f & e1 <= e2 holds f.e1 >= f.e2;
end;
:: 2008.08.31, A.T.
registration
cluster trivial -> increasing decreasing for ext-real-valued Function;
end;
registration
cluster increasing -> non-decreasing for ext-real-valued Function;
cluster decreasing -> non-increasing for ext-real-valued Function;
end;
registration
let f,g be increasing ext-real-valued Function;
cluster g*f -> increasing;
end;
registration
let f,g be non-decreasing ext-real-valued Function;
cluster g*f -> non-decreasing;
end;
registration
let f,g be decreasing ext-real-valued Function;
cluster g*f -> increasing;
end;
registration
let f,g be non-increasing ext-real-valued Function;
cluster g*f -> non-decreasing;
end;
registration
let f be decreasing ext-real-valued Function;
let g be increasing ext-real-valued Function;
cluster g*f -> decreasing;
cluster f*g -> decreasing;
end;
registration
let f be non-increasing ext-real-valued Function;
let g be non-decreasing ext-real-valued Function;
cluster g*f -> non-increasing;
cluster f*g -> non-increasing;
end;
registration
let X be ext-real-membered set;
cluster id X -> increasing for Function of X,X;
end;
registration
cluster increasing for sequence of NAT;
end;
definition
let s be ManySortedSet of NAT;
mode subsequence of s -> ManySortedSet of NAT means
:: VALUED_0:def 17
ex N being increasing sequence of NAT st it = s * N;
end;
registration
let X be non empty set, s be X-valued ManySortedSet of NAT;
cluster -> X-valued for subsequence of s;
end;
definition
let X be non empty set, s be sequence of X;
redefine mode subsequence of s -> sequence of X;
end;
definition
let X be non empty set, s be sequence of X, k be Nat;
redefine func s ^\ k -> subsequence of s;
end;
reserve s,s1,s2,s3 for sequence of X;
reserve XX for non empty set,
ss,ss1,ss2,ss3 for sequence of XX;
theorem :: VALUED_0:19
ss is subsequence of ss;
theorem :: VALUED_0:20
ss1 is subsequence of ss2 & ss2 is subsequence of ss3 implies
ss1 is subsequence of ss3;
:: to be generalized to Function of X,Y
registration
let X;
cluster constant for sequence of X;
end;
theorem :: VALUED_0:21
for ss1 being subsequence of ss holds rng ss1 c= rng ss;
registration
let X be non empty set;
let s be constant sequence of X;
cluster -> constant for subsequence of s;
end;
:: from FRECHET2, 2008.09.08, A.T.
definition
let X be non empty set, N be increasing sequence of NAT, s be sequence of X;
redefine func s*N -> subsequence of s;
end;
:: from RFUNCT_2 etc. 2008.09.10, A.T.
reserve X,Y for non empty set,
Z for set;
reserve s,s1 for sequence of X,
h,h1 for PartFunc of X,Y,
h2 for PartFunc of Y ,Z,
x for Element of X,
N for increasing sequence of NAT;
theorem :: VALUED_0:22
rng s c= dom h & s1 is subsequence of s implies h/*s1 is subsequence of h/*s;
:: to be generalized
registration
let X be with_non-empty_element set;
cluster non-empty for sequence of X;
end;
registration
let X be with_non-empty_element set, s be non-empty sequence of X;
cluster -> non-empty for subsequence of s;
end;
reserve i,j for Nat;
definition
let X be non empty set, s be sequence of X;
redefine attr s is constant means
:: VALUED_0:def 18
ex x being Element of X st for n being Nat holds s.n=x;
end;
theorem :: VALUED_0:23
for X being set for s being constant sequence of X holds s.i = s.j;
theorem :: VALUED_0:24
(for i,j holds s.i = s.j) implies s is constant;
theorem :: VALUED_0:25
(for i holds s.i = s.(i+1)) implies s is constant;
theorem :: VALUED_0:26
s is constant & s1 is subsequence of s implies s = s1;
reserve n for Nat;
theorem :: VALUED_0:27
rng s c= dom h implies (h/*s)^\n=h/*(s^\n);
theorem :: VALUED_0:28
s.n in rng s;
theorem :: VALUED_0:29
h is total implies h/*(s^\n) = (h/*s)^\n;
theorem :: VALUED_0:30
rng s c= dom h implies h.:(rng s) = rng (h/*s);
theorem :: VALUED_0:31
rng s c= dom (h2*h1) implies h2/*(h1/*s) = (h2*h1)/*s;
definition
let f be ext-real-valued Function;
attr f is zeroed means
:: VALUED_0:def 19
f.{} = 0;
end;
:: new, 2009.02.03, A.T.
registration
cluster COMPLEX-valued -> complex-valued for Relation;
cluster ExtREAL-valued -> ext-real-valued for Relation;
cluster REAL-valued -> real-valued for Relation;
cluster NAT-valued -> natural-valued for Relation;
end;
definition
let s be ManySortedSet of NAT;
redefine attr s is constant means
:: VALUED_0:def 20
ex x being set st for n being Nat holds s.n=x;
end;
theorem :: VALUED_0:32
for x being non empty set, M be ManySortedSet of NAT,
s be subsequence of M
holds rng s c= rng M;
registration
let X be set;
cluster natural-valued for ManySortedSet of X;
end;