:: Number-Valued Functions
:: by Library Committee
::
:: Received November 22, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users

definition

let f be Relation;

attr f is complex-valued means :Def1: :: VALUED_0:def 1
rng f c= COMPLEX ;

attr f is ext-real-valued means :Def2: :: VALUED_0:def 2
rng f c= ExtREAL ;

attr f is real-valued means :Def3: :: VALUED_0:def 3
rng f c= REAL ;

::$CD 2

attr f is natural-valued means :Def4: :: VALUED_0:def 6
rng f c= NAT ;

end;

:: deftheorem Def1 defines complex-valued VALUED_0:def 1 :
for f being Relation holds
( f is complex-valued iff rng f c= COMPLEX );

:: deftheorem Def2 defines ext-real-valued VALUED_0:def 2 :
for f being Relation holds
( f is ext-real-valued iff rng f c= ExtREAL );

:: deftheorem Def3 defines real-valued VALUED_0:def 3 :
for f being Relation holds
( f is real-valued iff rng f c= REAL );

:: deftheorem VALUED_0:def 4 :
canceled;

:: deftheorem VALUED_0:def 5 :
canceled;

:: deftheorem Def4 defines natural-valued VALUED_0:def 6 :
for f being Relation holds
( f is natural-valued iff rng f c= NAT );

registration

cluster Relation-like natural-valued -> INT -valued for set ;

coherence
for b₁ being Relation st b₁ is natural-valued holds
b₁ is INT -valued

proof end;

cluster Relation-like INT -valued -> RAT -valued for set ;

coherence
for b₁ being Relation st b₁ is INT -valued holds
b₁ is RAT -valued

proof end;

cluster Relation-like INT -valued -> real-valued for set ;

coherence
for b₁ being Relation st b₁ is INT -valued holds
b₁ is real-valued

proof end;

cluster Relation-like RAT -valued -> real-valued for set ;

coherence
for b₁ being Relation st b₁ is RAT -valued holds
b₁ is real-valued

proof end;

cluster Relation-like real-valued -> ext-real-valued for set ;

coherence
for b₁ being Relation st b₁ is real-valued holds
b₁ is ext-real-valued

proof end;

cluster Relation-like real-valued -> complex-valued for set ;

coherence
for b₁ being Relation st b₁ is real-valued holds
b₁ is complex-valued

proof end;

cluster Relation-like natural-valued -> RAT -valued for set ;

coherence
for b₁ being Relation st b₁ is natural-valued holds
b₁ is RAT -valued

proof end;

cluster Relation-like natural-valued -> real-valued for set ;

coherence
for b₁ being Relation st b₁ is natural-valued holds
b₁ is real-valued

proof end;

end;

registration

cluster Relation-like empty -> natural-valued for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is natural-valued

proof end;

end;

registration

cluster Relation-like Function-like natural-valued for set ;

existence
ex b₁ being Function st b₁ is natural-valued

proof end;

end;

registration

let R be complex-valued Relation;

cluster rng R -> complex-membered ;

coherence
rng R is complex-membered

proof end;

end;

registration

let R be ext-real-valued Relation;

cluster rng R -> ext-real-membered ;

coherence
rng R is ext-real-membered

proof end;

end;

registration

let R be real-valued Relation;

cluster rng R -> real-membered ;

coherence
rng R is real-membered

proof end;

end;

registration

let R be RAT -valued Relation;

cluster rng R -> rational-membered ;

coherence
rng R is rational-membered ;

end;

registration

let R be INT -valued Relation;

cluster rng R -> integer-membered ;

coherence
rng R is integer-membered ;

end;

registration

let R be natural-valued Relation;

cluster rng R -> natural-membered ;

coherence
rng R is natural-membered

proof end;

end;

theorem Th1: :: VALUED_0:1

for R being Relation
for S being complex-valued Relation st R c= S holds
R is complex-valued

proof end;

theorem Th2: :: VALUED_0:2

for R being Relation
for S being ext-real-valued Relation st R c= S holds
R is ext-real-valued

proof end;

theorem Th3: :: VALUED_0:3

for R being Relation
for S being real-valued Relation st R c= S holds
R is real-valued

proof end;

theorem :: VALUED_0:4

for R being Relation
for S being RAT -valued Relation st R c= S holds
R is RAT -valued ;

theorem :: VALUED_0:5

for R being Relation
for S being INT -valued Relation st R c= S holds
R is INT -valued ;

theorem Th6: :: VALUED_0:6

for R being Relation
for S being natural-valued Relation st R c= S holds
R is natural-valued

proof end;

registration

let R be complex-valued Relation;

cluster -> complex-valued for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is complex-valued by Th1;

end;

registration

let R be ext-real-valued Relation;

cluster -> ext-real-valued for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is ext-real-valued by Th2;

end;

registration

let R be real-valued Relation;

cluster -> real-valued for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is real-valued by Th3;

end;

registration

let R be RAT -valued Relation;

cluster -> RAT -valued for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is RAT -valued ;

end;

registration

let R be INT -valued Relation;

cluster -> INT -valued for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is INT -valued ;

end;

registration

let R be natural-valued Relation;

cluster -> natural-valued for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is natural-valued by Th6;

end;

registration

let R, S be complex-valued Relation;

cluster R \/ S -> complex-valued ;

coherence
R \/ S is complex-valued

proof end;

end;

registration

let R, S be ext-real-valued Relation;

cluster R \/ S -> ext-real-valued ;

coherence
R \/ S is ext-real-valued

proof end;

end;

registration

let R, S be real-valued Relation;

cluster R \/ S -> real-valued ;

coherence
R \/ S is real-valued

proof end;

end;

registration

let R, S be RAT -valued Relation;

cluster R \/ S -> RAT -valued ;

coherence
R \/ S is RAT -valued ;

end;

registration

let R, S be INT -valued Relation;

cluster R \/ S -> INT -valued ;

coherence
R \/ S is INT -valued ;

end;

registration

let R, S be natural-valued Relation;

cluster R \/ S -> natural-valued ;

coherence
R \/ S is natural-valued

proof end;

end;

registration

let R be complex-valued Relation;
let S be Relation;

cluster R /\ S -> complex-valued ;

coherence
R /\ S is complex-valued

proof end;

cluster R \ S -> complex-valued ;

coherence
R \ S is complex-valued ;

end;

registration

let R be ext-real-valued Relation;
let S be Relation;

cluster R /\ S -> ext-real-valued ;

coherence
R /\ S is ext-real-valued

proof end;

cluster R \ S -> ext-real-valued ;

coherence
R \ S is ext-real-valued ;

end;

registration

let R be real-valued Relation;
let S be Relation;

cluster R /\ S -> real-valued ;

coherence
R /\ S is real-valued

proof end;

cluster R \ S -> real-valued ;

coherence
R \ S is real-valued ;

end;

registration

let R be RAT -valued Relation;
let S be Relation;

cluster R /\ S -> RAT -valued ;

coherence
R /\ S is RAT -valued ;

cluster R \ S -> RAT -valued ;

coherence
R \ S is RAT -valued ;

end;

registration

let R be INT -valued Relation;
let S be Relation;

cluster R /\ S -> INT -valued ;

coherence
R /\ S is INT -valued ;

cluster R \ S -> INT -valued ;

coherence
R \ S is INT -valued ;

end;

registration

let R be natural-valued Relation;
let S be Relation;

cluster R /\ S -> natural-valued ;

coherence
R /\ S is natural-valued

proof end;

cluster R \ S -> natural-valued ;

coherence
R \ S is natural-valued ;

end;

registration

let R, S be complex-valued Relation;

cluster R \+\ S -> complex-valued ;

coherence
R \+\ S is complex-valued ;

end;

registration

let R, S be ext-real-valued Relation;

cluster R \+\ S -> ext-real-valued ;

coherence
R \+\ S is ext-real-valued ;

end;

registration

let R, S be real-valued Relation;

cluster R \+\ S -> real-valued ;

coherence
R \+\ S is real-valued ;

end;

registration

let R, S be RAT -valued Relation;

cluster R \+\ S -> RAT -valued ;

coherence
R \+\ S is RAT -valued ;

end;

registration

let R, S be INT -valued Relation;

cluster R \+\ S -> INT -valued ;

coherence
R \+\ S is INT -valued ;

end;

registration

let R, S be natural-valued Relation;

cluster R \+\ S -> natural-valued ;

coherence
R \+\ S is natural-valued ;

end;

registration

let R be complex-valued Relation;
let X be set ;

cluster R .: X -> complex-membered ;

coherence
R .: X is complex-membered

proof end;

end;

registration

let R be ext-real-valued Relation;
let X be set ;

cluster R .: X -> ext-real-membered ;

coherence
R .: X is ext-real-membered

proof end;

end;

registration

let R be real-valued Relation;
let X be set ;

cluster R .: X -> real-membered ;

coherence
R .: X is real-membered

proof end;

end;

registration

let R be RAT -valued Relation;
let X be set ;

cluster R .: X -> rational-membered ;

coherence
R .: X is rational-membered

proof end;

end;

registration

let R be INT -valued Relation;
let X be set ;

cluster R .: X -> integer-membered ;

coherence
R .: X is integer-membered

proof end;

end;

registration

let R be natural-valued Relation;
let X be set ;

cluster R .: X -> natural-membered ;

coherence
R .: X is natural-membered

proof end;

end;

registration

let R be complex-valued Relation;
let x be object ;

cluster Im (R,x) -> complex-membered ;

coherence
Im (R,x) is complex-membered ;

end;

registration

let R be ext-real-valued Relation;
let x be object ;

cluster Im (R,x) -> ext-real-membered ;

coherence
Im (R,x) is ext-real-membered ;

end;

registration

let R be real-valued Relation;
let x be object ;

cluster Im (R,x) -> real-membered ;

coherence
Im (R,x) is real-membered ;

end;

registration

let R be RAT -valued Relation;
let x be object ;

cluster Im (R,x) -> rational-membered ;

coherence
Im (R,x) is rational-membered ;

end;

registration

let R be INT -valued Relation;
let x be object ;

cluster Im (R,x) -> integer-membered ;

coherence
Im (R,x) is integer-membered ;

end;

registration

let R be natural-valued Relation;
let x be object ;

cluster Im (R,x) -> natural-membered ;

coherence
Im (R,x) is natural-membered ;

end;

registration

let R be complex-valued Relation;
let X be set ;

cluster R | X -> complex-valued ;

coherence
R | X is complex-valued

proof end;

end;

registration

let R be ext-real-valued Relation;
let X be set ;

cluster R | X -> ext-real-valued ;

coherence
R | X is ext-real-valued

proof end;

end;

registration

let R be real-valued Relation;
let X be set ;

cluster R | X -> real-valued ;

coherence
R | X is real-valued

proof end;

end;

registration

let R be RAT -valued Relation;
let X be set ;

cluster R | X -> RAT -valued ;

coherence
R | X is RAT -valued ;

end;

registration

let R be INT -valued Relation;
let X be set ;

cluster R | X -> INT -valued ;

coherence
R | X is INT -valued ;

end;

registration

let R be natural-valued Relation;
let X be set ;

cluster R | X -> natural-valued ;

coherence
R | X is natural-valued

proof end;

end;

registration

let X be complex-membered set ;

cluster id X -> complex-valued ;

coherence
id X is complex-valued by MEMBERED:1;

end;

registration

let X be ext-real-membered set ;

cluster id X -> ext-real-valued ;

coherence
id X is ext-real-valued by MEMBERED:2;

end;

registration

let X be real-membered set ;

cluster id X -> real-valued ;

coherence
id X is real-valued by MEMBERED:3;

end;

registration

let X be rational-membered set ;

cluster id X -> RAT -valued ;

coherence
id X is RAT -valued by MEMBERED:4;

end;

registration

let X be integer-membered set ;

cluster id X -> INT -valued ;

coherence
id X is INT -valued by MEMBERED:5;

end;

registration

let X be natural-membered set ;

cluster id X -> natural-valued ;

coherence
id X is natural-valued by MEMBERED:6;

end;

registration

let R be Relation;
let S be complex-valued Relation;

cluster R * S -> complex-valued ;

coherence
R * S is complex-valued

proof end;

end;

registration

let R be Relation;
let S be ext-real-valued Relation;

cluster R * S -> ext-real-valued ;

coherence
R * S is ext-real-valued

proof end;

end;

registration

let R be Relation;
let S be real-valued Relation;

cluster R * S -> real-valued ;

coherence
R * S is real-valued

proof end;

end;

registration

let R be Relation;
let S be RAT -valued Relation;

cluster R * S -> RAT -valued ;

coherence
R * S is RAT -valued ;

end;

registration

let R be Relation;
let S be INT -valued Relation;

cluster R * S -> INT -valued ;

coherence
R * S is INT -valued ;

end;

registration

let R be Relation;
let S be natural-valued Relation;

cluster R * S -> natural-valued ;

coherence
R * S is natural-valued

proof end;

end;

definition

let f be Function;

redefine attr f is complex-valued means :: VALUED_0:def 7
for x being object st x in dom f holds
f . x is complex ;

compatibility
( f is complex-valued iff for x being object st x in dom f holds
f . x is complex )

proof end;

redefine attr f is ext-real-valued means :: VALUED_0:def 8
for x being object st x in dom f holds
f . x is ext-real ;

compatibility
( f is ext-real-valued iff for x being object st x in dom f holds
f . x is ext-real )

proof end;

redefine attr f is real-valued means :: VALUED_0:def 9
for x being object st x in dom f holds
f . x is real ;

compatibility
( f is real-valued iff for x being object st x in dom f holds
f . x is real )

proof end;

redefine attr f is natural-valued means :: VALUED_0:def 12
for x being object st x in dom f holds
f . x is natural ;

compatibility
( f is natural-valued iff for x being object st x in dom f holds
f . x is natural )

proof end;

end;

:: deftheorem defines complex-valued VALUED_0:def 7 :
for f being Function holds
( f is complex-valued iff for x being object st x in dom f holds
f . x is complex );

:: deftheorem defines ext-real-valued VALUED_0:def 8 :
for f being Function holds
( f is ext-real-valued iff for x being object st x in dom f holds
f . x is ext-real );

:: deftheorem defines real-valued VALUED_0:def 9 :
for f being Function holds
( f is real-valued iff for x being object st x in dom f holds
f . x is real );

:: deftheorem VALUED_0:def 10 :
canceled;

:: deftheorem VALUED_0:def 11 :
canceled;

:: deftheorem defines natural-valued VALUED_0:def 12 :
for f being Function holds
( f is natural-valued iff for x being object st x in dom f holds
f . x is natural );

theorem Th7: :: VALUED_0:7

for f being Function holds
( f is complex-valued iff for x being object holds f . x is complex )

proof end;

theorem Th8: :: VALUED_0:8

for f being Function holds
( f is ext-real-valued iff for x being object holds f . x is ext-real )

proof end;

theorem Th9: :: VALUED_0:9

for f being Function holds
( f is real-valued iff for x being object holds f . x is real )

proof end;

theorem Th10: :: VALUED_0:10

for f being Function holds
( f is RAT -valued iff for x being object holds f . x is rational )

proof end;

theorem Th11: :: VALUED_0:11

for f being Function holds
( f is INT -valued iff for x being object holds f . x is integer )

proof end;

theorem Th12: :: VALUED_0:12

for f being Function holds
( f is natural-valued iff for x being object holds f . x is natural )

proof end;

registration

let f be complex-valued Function;
let x be object ;

cluster f . x -> complex ;

coherence
f . x is complex by Th7;

end;

registration

let f be ext-real-valued Function;
let x be object ;

cluster f . x -> ext-real ;

coherence
f . x is ext-real by Th8;

end;

registration

let f be real-valued Function;
let x be object ;

cluster f . x -> real ;

coherence
f . x is real by Th9;

end;

registration

let f be RAT -valued Function;
let x be object ;

cluster f . x -> rational ;

coherence
f . x is rational by Th10;

end;

registration

let f be INT -valued Function;
let x be object ;

cluster f . x -> integer ;

coherence
f . x is integer by Th11;

end;

registration

let f be natural-valued Function;
let x be object ;

cluster f . x -> natural ;

coherence
f . x is natural by Th12;

end;

registration

let X be set ;
let x be Complex;

cluster X --> x -> complex-valued ;

coherence
X --> x is complex-valued

proof end;

end;

registration

let X be set ;
let x be ExtReal;

cluster X --> x -> ext-real-valued ;

coherence
X --> x is ext-real-valued

proof end;

end;

registration

let X be set ;
let x be Real;

cluster X --> x -> real-valued ;

coherence
X --> x is real-valued

proof end;

end;

registration

let X be set ;
let x be Rational;

cluster X --> x -> RAT -valued ;

coherence
X --> x is RAT -valued

proof end;

end;

registration

let X be set ;
let x be Integer;

cluster X --> x -> INT -valued ;

coherence
X --> x is INT -valued

proof end;

end;

registration

let X be set ;
let x be Nat;

cluster X --> x -> natural-valued ;

coherence
X --> x is natural-valued

proof end;

end;

registration

let f, g be complex-valued Function;

cluster f +* g -> complex-valued ;

coherence
f +* g is complex-valued

proof end;

end;

registration

let f, g be ext-real-valued Function;

cluster f +* g -> ext-real-valued ;

coherence
f +* g is ext-real-valued

proof end;

end;

registration

let f, g be real-valued Function;

cluster f +* g -> real-valued ;

coherence
f +* g is real-valued

proof end;

end;

registration

let f, g be RAT -valued Function;

cluster f +* g -> RAT -valued ;

coherence
f +* g is RAT -valued

proof end;

end;

registration

let f, g be INT -valued Function;

cluster f +* g -> INT -valued ;

coherence
f +* g is INT -valued

proof end;

end;

registration

let f, g be natural-valued Function;

cluster f +* g -> natural-valued ;

coherence
f +* g is natural-valued

proof end;

end;

registration

let x be object ;
let y be Complex;

cluster x .--> y -> complex-valued ;

coherence
x .--> y is complex-valued ;

end;

registration

let x be object ;
let y be ExtReal;

cluster x .--> y -> ext-real-valued ;

coherence
x .--> y is ext-real-valued ;

end;

registration

let x be object ;
let y be Real;

cluster x .--> y -> real-valued ;

coherence
x .--> y is real-valued ;

end;

registration

let x be object ;
let y be Rational;

cluster x .--> y -> RAT -valued ;

coherence
x .--> y is RAT -valued ;

end;

registration

let x be object ;
let y be Integer;

cluster x .--> y -> INT -valued ;

coherence
x .--> y is INT -valued ;

end;

registration

let x be object ;
let y be Nat;

cluster x .--> y -> natural-valued ;

coherence
x .--> y is natural-valued ;

end;

registration

let X be set ;
let Y be complex-membered set ;

cluster -> complex-valued for Element of bool [:X,Y:];

coherence
for b₁ being Relation of X,Y holds b₁ is complex-valued

proof end;

end;

registration

let X be set ;
let Y be ext-real-membered set ;

cluster -> ext-real-valued for Element of bool [:X,Y:];

coherence
for b₁ being Relation of X,Y holds b₁ is ext-real-valued

proof end;

end;

registration

let X be set ;
let Y be real-membered set ;

cluster -> real-valued for Element of bool [:X,Y:];

coherence
for b₁ being Relation of X,Y holds b₁ is real-valued

proof end;

end;

registration

let X be set ;
let Y be rational-membered set ;

cluster -> RAT -valued for Element of bool [:X,Y:];

coherence
for b₁ being Relation of X,Y holds b₁ is RAT -valued

proof end;

end;

registration

let X be set ;
let Y be integer-membered set ;

cluster -> INT -valued for Element of bool [:X,Y:];

coherence
for b₁ being Relation of X,Y holds b₁ is INT -valued

proof end;

end;

registration

let X be set ;
let Y be natural-membered set ;

cluster -> natural-valued for Element of bool [:X,Y:];

coherence
for b₁ being Relation of X,Y holds b₁ is natural-valued

proof end;

end;

registration

let X be set ;
let Y be complex-membered set ;

cluster [:X,Y:] -> complex-valued ;

coherence
[:X,Y:] is complex-valued

proof end;

end;

registration

let X be set ;
let Y be ext-real-membered set ;

cluster [:X,Y:] -> ext-real-valued ;

coherence
[:X,Y:] is ext-real-valued

proof end;

end;

registration

let X be set ;
let Y be real-membered set ;

cluster [:X,Y:] -> real-valued ;

coherence
[:X,Y:] is real-valued

proof end;

end;

registration

let X be set ;
let Y be rational-membered set ;

cluster [:X,Y:] -> RAT -valued ;

coherence
[:X,Y:] is RAT -valued

proof end;

end;

registration

let X be set ;
let Y be integer-membered set ;

cluster [:X,Y:] -> INT -valued ;

coherence
[:X,Y:] is INT -valued

proof end;

end;

registration

let X be set ;
let Y be natural-membered set ;

cluster [:X,Y:] -> natural-valued ;

coherence
[:X,Y:] is natural-valued

proof end;

end;

:::notation
::: synonym f is non-zero for f is non-empty;
:::end;

registration

cluster Relation-like RAT -valued INT -valued Function-like constant non empty natural-valued for set ;

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is constant & b₁ is natural-valued & b₁ is INT -valued & b₁ is RAT -valued )

proof end;

end;

theorem :: VALUED_0:13

for f being constant non empty complex-valued Function ex r being Complex st
for x being object st x in dom f holds
f . x = r

proof end;

theorem :: VALUED_0:14

for f being constant non empty ext-real-valued Function ex r being ExtReal st
for x being object st x in dom f holds
f . x = r

proof end;

theorem :: VALUED_0:15

for f being constant non empty real-valued Function ex r being Real st
for x being object st x in dom f holds
f . x = r

proof end;

theorem :: VALUED_0:16

for f being RAT -valued constant non empty Function ex r being Rational st
for x being object st x in dom f holds
f . x = r

proof end;

theorem :: VALUED_0:17

for f being INT -valued constant non empty Function ex r being Integer st
for x being object st x in dom f holds
f . x = r

proof end;

theorem :: VALUED_0:18

for f being constant non empty natural-valued Function ex r being Nat st
for x being object st x in dom f holds
f . x = r

proof end;

definition

let f be ext-real-valued Function;

attr f is increasing means :Def9: :: VALUED_0:def 13
for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2;

attr f is decreasing means :Def10: :: VALUED_0:def 14
for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 > f . e2;

attr f is non-decreasing means :Def11: :: VALUED_0:def 15
for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2;

attr f is non-increasing means :Def12: :: VALUED_0:def 16
for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 >= f . e2;

end;

:: deftheorem Def9 defines increasing VALUED_0:def 13 :
for f being ext-real-valued Function holds
( f is increasing iff for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2 );

:: deftheorem Def10 defines decreasing VALUED_0:def 14 :
for f being ext-real-valued Function holds
( f is decreasing iff for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 > f . e2 );

:: deftheorem Def11 defines non-decreasing VALUED_0:def 15 :
for f being ext-real-valued Function holds
( f is non-decreasing iff for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2 );

:: deftheorem Def12 defines non-increasing VALUED_0:def 16 :
for f being ext-real-valued Function holds
( f is non-increasing iff for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 >= f . e2 );

:: 2008.08.31, A.T.

registration

cluster Relation-like Function-like trivial ext-real-valued -> ext-real-valued increasing decreasing for set ;

coherence
for b₁ being ext-real-valued Function st b₁ is trivial holds
( b₁ is increasing & b₁ is decreasing ) by ZFMISC_1:def 10;

end;

registration

cluster Relation-like Function-like ext-real-valued increasing -> ext-real-valued non-decreasing for set ;

coherence
for b₁ being ext-real-valued Function st b₁ is increasing holds
b₁ is non-decreasing

proof end;

cluster Relation-like Function-like ext-real-valued decreasing -> ext-real-valued non-increasing for set ;

coherence
for b₁ being ext-real-valued Function st b₁ is decreasing holds
b₁ is non-increasing

proof end;

end;

registration

let f, g be ext-real-valued increasing Function;

cluster f * g -> increasing ;

coherence
g * f is increasing

proof end;

end;

registration

let f, g be ext-real-valued non-decreasing Function;

cluster f * g -> non-decreasing ;

coherence
g * f is non-decreasing

proof end;

end;

registration

let f, g be ext-real-valued decreasing Function;

cluster f * g -> increasing ;

coherence
g * f is increasing

proof end;

end;

registration

let f, g be ext-real-valued non-increasing Function;

cluster f * g -> non-decreasing ;

coherence
g * f is non-decreasing

proof end;

end;

registration

let f be ext-real-valued decreasing Function;
let g be ext-real-valued increasing Function;

cluster f * g -> decreasing ;

coherence
g * f is decreasing

proof end;

cluster g * f -> decreasing ;

coherence
f * g is decreasing

proof end;

end;

registration

let f be ext-real-valued non-increasing Function;
let g be ext-real-valued non-decreasing Function;

cluster f * g -> non-increasing ;

coherence
g * f is non-increasing

proof end;

cluster g * f -> non-increasing ;

coherence
f * g is non-increasing

proof end;

end;

registration

let X be ext-real-membered set ;

cluster id X -> increasing for Function of X,X;

coherence
for b₁ being Function of X,X st b₁ = id X holds
b₁ is increasing

proof end;

end;

registration

cluster Relation-like omega -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing for Element of bool [:omega,NAT:];

existence
ex b₁ being sequence of NAT st b₁ is increasing

proof end;

end;

definition

let s be ManySortedSet of NAT ;

mode subsequence of s -> ManySortedSet of NAT means :Def13: :: VALUED_0:def 17
ex N being increasing sequence of NAT st it = s * N;

existence
ex b₁ being ManySortedSet of NAT ex N being increasing sequence of NAT st b₁ = s * N

proof end;

end;

:: deftheorem Def13 defines subsequence VALUED_0:def 17 :
for s, b₂ being ManySortedSet of NAT holds
( b₂ is subsequence of s iff ex N being increasing sequence of NAT st b₂ = s * N );

Lm1: for x being non empty set
for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M

proof end;

registration

let X be non empty set ;
let s be X -valued ManySortedSet of NAT ;

cluster -> X -valued for subsequence of s;

coherence
for b₁ being subsequence of s holds b₁ is X -valued

proof end;

end;

definition

let X be non empty set ;
let s be sequence of X;
:: original: subsequence
redefine mode subsequence of s -> sequence of X;
coherence
for b₁ being subsequence of s holds b₁ is sequence of X

proof end;

end;

definition

let X be non empty set ;
let s be sequence of X;
let k be Nat;
:: original: ^\
redefine func s ^\ k -> subsequence of s;
coherence
s ^\ k is subsequence of s

proof end;

end;

theorem :: VALUED_0:19

for XX being non empty set
for ss being sequence of XX holds ss is subsequence of ss

proof end;

theorem :: VALUED_0:20

for XX being non empty set
for ss1, ss2, ss3 being sequence of XX st ss1 is subsequence of ss2 & ss2 is subsequence of ss3 holds
ss1 is subsequence of ss3

proof end;

:: to be generalized to Function of X,Y

registration

let X be set ;

cluster Relation-like omega -defined X -valued Function-like constant quasi_total for Element of bool [:omega,X:];

existence
ex b₁ being sequence of X st b₁ is constant

proof end;

end;

theorem Th21: :: VALUED_0:21

for XX being non empty set
for ss being sequence of XX
for ss1 being subsequence of ss holds rng ss1 c= rng ss

proof end;

registration

let X be non empty set ;
let s be constant sequence of X;

cluster -> constant for subsequence of s;

coherence
for b₁ being subsequence of s holds b₁ is constant

proof end;

end;

:: from FRECHET2, 2008.09.08, A.T.

definition

let X be non empty set ;
let N be increasing sequence of NAT;
let s be sequence of X;
:: original: *
redefine func s * N -> subsequence of s;
correctness
coherence
N * s is subsequence of s;
by Def13;

end;

theorem :: VALUED_0:22

for X, Y being non empty set
for s, s1 being sequence of X
for h being PartFunc of X,Y st rng s c= dom h & s1 is subsequence of s holds
h /* s1 is subsequence of h /* s

proof end;

:: to be generalized

registration

let X be with_non-empty_element set ;

cluster Relation-like non-empty omega -defined X -valued Function-like non empty total quasi_total for Element of bool [:omega,X:];

existence
ex b₁ being sequence of X st b₁ is non-empty

proof end;

end;

registration

let X be with_non-empty_element set ;
let s be non-empty sequence of X;

cluster -> non-empty for subsequence of s;

coherence
for b₁ being subsequence of s holds b₁ is non-empty

proof end;

end;

definition

let X be non empty set ;
let s be sequence of X;

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

compatibility
( s is constant iff ex x being Element of X st
for n being Nat holds s . n = x )

proof end;

end;

:: deftheorem defines constant VALUED_0:def 18 :
for X being non empty set
for s being sequence of X holds
( s is constant iff ex x being Element of X st
for n being Nat holds s . n = x );

theorem Th23: :: VALUED_0:23

for i, j being Nat
for X being set
for s being constant sequence of X holds s . i = s . j

proof end;

theorem :: VALUED_0:24

for X being non empty set
for s being sequence of X st ( for i, j being Nat holds s . i = s . j ) holds
s is V30() ;

theorem :: VALUED_0:25

for X being non empty set
for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds
s is V30()

proof end;

theorem :: VALUED_0:26

for X being non empty set
for s, s1 being sequence of X st s is V30() & s1 is subsequence of s holds
s = s1

proof end;

theorem Th27: :: VALUED_0:27

for X, Y being non empty set
for s being sequence of X
for h being PartFunc of X,Y
for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)

proof end;

theorem Th28: :: VALUED_0:28

for X being non empty set
for s being sequence of X
for n being Nat holds s . n in rng s

proof end;

theorem :: VALUED_0:29

for X, Y being non empty set
for s being sequence of X
for h being PartFunc of X,Y
for n being Nat st h is total holds
h /* (s ^\ n) = (h /* s) ^\ n

proof end;

theorem Th30: :: VALUED_0:30

for X, Y being non empty set
for s being sequence of X
for h being PartFunc of X,Y st rng s c= dom h holds
h .: (rng s) = rng (h /* s)

proof end;

theorem :: VALUED_0:31

for X, Y being non empty set
for Z being set
for s being sequence of X
for h1 being PartFunc of X,Y
for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s

proof end;

definition

let f be ext-real-valued Function;

attr f is zeroed means :: VALUED_0:def 19
f . {} = 0 ;

end;

:: deftheorem defines zeroed VALUED_0:def 19 :
for f being ext-real-valued Function holds
( f is zeroed iff f . {} = 0 );

:: new, 2009.02.03, A.T.

registration

cluster Relation-like COMPLEX -valued -> complex-valued for set ;

coherence
for b₁ being Relation st b₁ is COMPLEX -valued holds
b₁ is complex-valued ;

cluster Relation-like ExtREAL -valued -> ext-real-valued for set ;

coherence
for b₁ being Relation st b₁ is ExtREAL -valued holds
b₁ is ext-real-valued ;

cluster Relation-like REAL -valued -> real-valued for set ;

coherence
for b₁ being Relation st b₁ is REAL -valued holds
b₁ is real-valued ;

cluster Relation-like NAT -valued -> natural-valued for set ;

coherence
for b₁ being Relation st b₁ is NAT -valued holds
b₁ is natural-valued ;

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;

compatibility
( s is constant iff ex x being set st
for n being Nat holds s . n = x )

proof end;

end;

:: deftheorem defines constant VALUED_0:def 20 :
for s being ManySortedSet of NAT holds
( s is constant iff ex x being set st
for n being Nat holds s . n = x );

theorem :: VALUED_0:32

for x being non empty set
for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M by Lm1;

registration

let X be set ;

cluster Relation-like X -defined Function-like total natural-valued for set ;

existence
ex b₁ being ManySortedSet of X st b₁ is natural-valued

proof end;

end;