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