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

begin

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 ;
attr f is rational-valued means :Def4: :: VALUED_0:def 4
rng f c= RAT ;
attr f is integer-valued means :Def5: :: VALUED_0:def 5
rng f c= INT ;
attr f is natural-valued means :Def6: :: 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 Def4 defines rational-valued VALUED_0:def 4 :
for f being Relation holds
( f is rational-valued iff rng f c= RAT );

:: deftheorem Def5 defines integer-valued VALUED_0:def 5 :
for f being Relation holds
( f is integer-valued iff rng f c= INT );

:: deftheorem Def6 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 -> integer-valued set ;
coherence
for b₁ being Relation st b₁ is natural-valued holds
b₁ is integer-valued

proof end;

cluster Relation-like integer-valued -> rational-valued set ;
coherence
for b₁ being Relation st b₁ is integer-valued holds
b₁ is rational-valued

proof end;

cluster Relation-like rational-valued -> real-valued set ;
coherence
for b₁ being Relation st b₁ is rational-valued holds
b₁ is real-valued

proof end;

cluster Relation-like real-valued -> ext-real-valued 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 set ;
coherence
for b₁ being Relation st b₁ is real-valued holds
b₁ is complex-valued

proof end;

end;

registration

cluster empty Relation-like -> natural-valued 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 set ;
existence
ex b₁ being Function st b₁ is natural-valued

proof end;

end;

registration

let R be complex-valued Relation;
cluster proj2 R -> complex-membered ;
coherence
rng R is complex-membered

proof end;

end;

registration

let R be ext-real-valued Relation;
cluster proj2 R -> ext-real-membered ;
coherence
rng R is ext-real-membered

proof end;

end;

registration

let R be real-valued Relation;
cluster proj2 R -> real-membered ;
coherence
rng R is real-membered

proof end;

end;

registration

let R be rational-valued Relation;
cluster proj2 R -> rational-membered ;
coherence
rng R is rational-membered

proof end;

end;

registration

let R be integer-valued Relation;
cluster proj2 R -> integer-membered ;
coherence
rng R is integer-membered

proof end;

end;

registration

let R be natural-valued Relation;
cluster proj2 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 Th4: :: VALUED_0:4

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

proof end;

theorem Th5: :: VALUED_0:5

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

proof end;

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 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 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 Element of bool R;
coherence
for b₁ being Subset of R holds b₁ is real-valued by Th3;

end;

registration

let R be rational-valued Relation;
cluster -> rational-valued Element of bool R;
coherence
for b₁ being Subset of R holds b₁ is rational-valued by Th4;

end;

registration

let R be integer-valued Relation;
cluster -> integer-valued Element of bool R;
coherence
for b₁ being Subset of R holds b₁ is integer-valued by Th5;

end;

registration

let R be natural-valued Relation;
cluster -> natural-valued 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 rational-valued Relation;
cluster R \/ S -> rational-valued ;
coherence
R \/ S is rational-valued

proof end;

end;

registration

let R, S be integer-valued Relation;
cluster R \/ S -> integer-valued ;
coherence
R \/ S is integer-valued

proof end;

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 rational-valued Relation;
let S be Relation;
cluster R /\ S -> rational-valued ;
coherence
R /\ S is rational-valued

proof end;

cluster R \ S -> rational-valued ;
coherence
R \ S is rational-valued ;

end;

registration

let R be integer-valued Relation;
let S be Relation;
cluster R /\ S -> integer-valued ;
coherence
R /\ S is integer-valued

proof end;

cluster R \ S -> integer-valued ;
coherence
R \ S is integer-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 rational-valued Relation;
cluster R \+\ S -> rational-valued ;
coherence
R \+\ S is rational-valued ;

end;

registration

let R, S be integer-valued Relation;
cluster R \+\ S -> integer-valued ;
coherence
R \+\ S is integer-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 rational-valued Relation;
let X be set ;
cluster R .: X -> rational-membered ;
coherence
R .: X is rational-membered

proof end;

end;

registration

let R be integer-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 set ;
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 set ;
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 set ;
cluster Im (R,x) -> real-membered ;
coherence
Im (R,x) is real-membered ;

end;

registration

let R be rational-valued Relation;
let x be set ;
cluster Im (R,x) -> rational-membered ;
coherence
Im (R,x) is rational-membered ;

end;

registration

let R be integer-valued Relation;
let x be set ;
cluster Im (R,x) -> integer-membered ;
coherence
Im (R,x) is integer-membered ;

end;

registration

let R be natural-valued Relation;
let x be set ;
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 rational-valued Relation;
let X be set ;
cluster R | X -> rational-valued ;
coherence
R | X is rational-valued

proof end;

end;

registration

let R be integer-valued Relation;
let X be set ;
cluster R | X -> integer-valued ;
coherence
R | X is integer-valued

proof end;

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

proof end;

end;

registration

let X be ext-real-membered set ;
cluster id X -> ext-real-valued ;
coherence
id X is ext-real-valued

proof end;

end;

registration

let X be real-membered set ;
cluster id X -> real-valued ;
coherence
id X is real-valued

proof end;

end;

registration

let X be rational-membered set ;
cluster id X -> rational-valued ;
coherence
id X is rational-valued

proof end;

end;

registration

let X be integer-membered set ;
cluster id X -> integer-valued ;
coherence
id X is integer-valued

proof end;

end;

registration

let X be natural-membered set ;
cluster id X -> natural-valued ;
coherence
id X is natural-valued

proof end;

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 rational-valued Relation;
cluster R * S -> rational-valued ;
coherence
R * S is rational-valued

proof end;

end;

registration

let R be Relation;
let S be integer-valued Relation;
cluster R * S -> integer-valued ;
coherence
R * S is integer-valued

proof end;

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 :Def7: :: VALUED_0:def 7
for x being set st x in dom f holds
f . x is complex ;
compatibility
( f is complex-valued iff for x being set st x in dom f holds
f . x is complex )

proof end;

redefine attr f is ext-real-valued means :Def8: :: VALUED_0:def 8
for x being set st x in dom f holds
f . x is ext-real ;
compatibility
( f is ext-real-valued iff for x being set st x in dom f holds
f . x is ext-real )

proof end;

redefine attr f is real-valued means :Def9: :: VALUED_0:def 9
for x being set st x in dom f holds
f . x is real ;
compatibility
( f is real-valued iff for x being set st x in dom f holds
f . x is real )

proof end;

redefine attr f is rational-valued means :Def10: :: VALUED_0:def 10
for x being set st x in dom f holds
f . x is rational ;
compatibility
( f is rational-valued iff for x being set st x in dom f holds
f . x is rational )

proof end;

redefine attr f is integer-valued means :Def11: :: VALUED_0:def 11
for x being set st x in dom f holds
f . x is integer ;
compatibility
( f is integer-valued iff for x being set st x in dom f holds
f . x is integer )

proof end;

redefine attr f is natural-valued means :Def12: :: VALUED_0:def 12
for x being set st x in dom f holds
f . x is natural ;
compatibility
( f is natural-valued iff for x being set st x in dom f holds
f . x is natural )

proof end;

end;

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

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

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

:: deftheorem Def10 defines rational-valued VALUED_0:def 10 :
for f being Function holds
( f is rational-valued iff for x being set st x in dom f holds
f . x is rational );

:: deftheorem Def11 defines integer-valued VALUED_0:def 11 :
for f being Function holds
( f is integer-valued iff for x being set st x in dom f holds
f . x is integer );

:: deftheorem Def12 defines natural-valued VALUED_0:def 12 :
for f being Function holds
( f is natural-valued iff for x being set 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 set 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 set 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 set holds f . x is real )

proof end;

theorem Th10: :: VALUED_0:10

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

proof end;

theorem Th11: :: VALUED_0:11

for f being Function holds
( f is integer-valued iff for x being set 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 set holds f . x is natural )

proof end;

registration

let f be complex-valued Function;
let x be set ;
cluster f . x -> complex ;
coherence
f . x is complex by Th7;

end;

registration

let f be ext-real-valued Function;
let x be set ;
cluster f . x -> ext-real ;
coherence
f . x is ext-real by Th8;

end;

registration

let f be real-valued Function;
let x be set ;
cluster f . x -> real ;
coherence
f . x is real by Th9;

end;

registration

let f be rational-valued Function;
let x be set ;
cluster f . x -> rational ;
coherence
f . x is rational by Th10;

end;

registration

let f be integer-valued Function;
let x be set ;
cluster f . x -> integer ;
coherence
f . x is integer by Th11;

end;

registration

let f be natural-valued Function;
let x be set ;
cluster f . x -> natural ;
coherence
f . x is natural by Th12;

end;

registration

let X be set ;
let x be complex number ;
cluster X --> x -> complex-valued ;
coherence
X --> x is complex-valued

proof end;

end;

registration

let X be set ;
let x be ext-real number ;
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 number ;
cluster X --> x -> real-valued ;
coherence
X --> x is real-valued

proof end;

end;

registration

let X be set ;
let x be rational number ;
cluster X --> x -> rational-valued ;
coherence
X --> x is rational-valued

proof end;

end;

registration

let X be set ;
let x be integer number ;
cluster X --> x -> integer-valued ;
coherence
X --> x is integer-valued

proof end;

end;

registration

let X be set ;
let x be natural number ;
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 rational-valued Function;
cluster f +* g -> rational-valued ;
coherence
f +* g is rational-valued

proof end;

end;

registration

let f, g be integer-valued Function;
cluster f +* g -> integer-valued ;
coherence
f +* g is integer-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 set ;
let y be complex number ;
cluster x .--> y -> complex-valued ;
coherence
x .--> y is complex-valued ;

end;

registration

let x be set ;
let y be ext-real number ;
cluster x .--> y -> ext-real-valued ;
coherence
x .--> y is ext-real-valued ;

end;

registration

let x be set ;
let y be real number ;
cluster x .--> y -> real-valued ;
coherence
x .--> y is real-valued ;

end;

registration

let x be set ;
let y be rational number ;
cluster x .--> y -> rational-valued ;
coherence
x .--> y is rational-valued ;

end;

registration

let x be set ;
let y be integer number ;
cluster x .--> y -> integer-valued ;
coherence
x .--> y is integer-valued ;

end;

registration

let x be set ;
let y be natural number ;
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 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 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 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 -> rational-valued Element of bool [:X,Y:];
coherence
for b₁ being Relation of X,Y holds b₁ is rational-valued

proof end;

end;

registration

let X be set ;
let Y be integer-membered set ;
cluster -> integer-valued Element of bool [:X,Y:];
coherence
for b₁ being Relation of X,Y holds b₁ is integer-valued

proof end;

end;

registration

let X be set ;
let Y be natural-membered set ;
cluster -> natural-valued 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:] -> rational-valued ;
coherence
[:X,Y:] is rational-valued

proof end;

end;

registration

let X be set ;
let Y be integer-membered set ;
cluster [:X,Y:] -> integer-valued ;
coherence
[:X,Y:] is integer-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

let f be ext-real-valued Relation;
synonym non-zero f for non-empty ;

end;

registration

cluster non empty Relation-like Function-like constant natural-valued set ;
existence
ex b₁ being Function st
( not b₁ is empty & b₁ is constant & b₁ is natural-valued )

proof end;

end;

theorem :: VALUED_0:13

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

proof end;

theorem :: VALUED_0:14

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

proof end;

theorem :: VALUED_0:15

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

proof end;

theorem :: VALUED_0:16

for f being non empty constant rational-valued Function ex r being rational number st
for x being set st x in dom f holds
f . x = r

proof end;

theorem :: VALUED_0:17

for f being non empty constant integer-valued Function ex r being integer number st
for x being set st x in dom f holds
f . x = r

proof end;

theorem :: VALUED_0:18

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

proof end;

begin

definition

let f be ext-real-valued Function;
attr f is increasing means :Def13: :: VALUED_0:def 13
for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2;
attr f is decreasing means :Def14: :: VALUED_0:def 14
for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 > f . e2;
attr f is non-decreasing means :Def15: :: VALUED_0:def 15
for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2;
attr f is non-increasing means :Def16: :: VALUED_0:def 16
for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 >= f . e2;

end;

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

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

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

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

registration

cluster trivial Relation-like Function-like ext-real-valued -> ext-real-valued increasing decreasing set ;
coherence
for b₁ being ext-real-valued Function st b₁ is trivial holds
( b₁ is increasing & b₁ is decreasing )

proof end;

end;

registration

cluster Relation-like Function-like ext-real-valued increasing -> ext-real-valued non-decreasing 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 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 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 non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued increasing Element of bool [:NAT,NAT:];
existence
ex b₁ being sequence of NAT st b₁ is increasing

proof end;

end;

definition

let X be set ;
let s be sequence of X;
mode subsequence of s -> sequence of X means :Def17: :: VALUED_0:def 17
ex N being increasing sequence of NAT st it = s * N;
existence
ex b₁ being sequence of X ex N being increasing sequence of NAT st b₁ = s * N

proof end;

end;

:: deftheorem Def17 defines subsequence VALUED_0:def 17 :
for X being set
for s, b₃ being sequence of X holds
( b₃ is subsequence of s iff ex N being increasing sequence of NAT st b₃ = s * N );

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 X being set
for s being sequence of X holds s is subsequence of s

proof end;

theorem :: VALUED_0:20

for X being set
for s1, s2, s3 being sequence of X st s1 is subsequence of s2 & s2 is subsequence of s3 holds
s1 is subsequence of s3

proof end;

registration

let X be set ;
cluster Relation-like NAT -defined X -valued Function-like constant quasi_total Element of bool [:NAT,X:];
existence
ex b₁ being sequence of X st b₁ is constant

proof end;

end;

theorem Th21: :: VALUED_0:21

for X being set
for s being sequence of X
for s1 being subsequence of s holds rng s1 c= rng s

proof end;

registration

let X be set ;
let s be constant sequence of X;
cluster -> constant subsequence of s;
coherence
for b₁ being subsequence of s holds b₁ is constant

proof end;

end;

definition

let X be 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;

proof end;

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;

registration

let X be with_non-empty_element set ;
cluster non empty Relation-like non-empty NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:];
existence
ex b₁ being sequence of X st b₁ is non-zero

proof end;

end;

registration

let X be with_non-empty_element set ;
let s be non-empty sequence of X;
cluster -> non-empty subsequence of s;
coherence
for b₁ being subsequence of s holds b₁ is non-zero

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 Th24: :: 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 constant

proof end;

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 constant

proof end;

theorem :: VALUED_0:26

for X being non empty set
for s, s1 being sequence of X st s is constant & 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 );

registration

cluster Relation-like COMPLEX -valued -> complex-valued set ;
coherence
for b₁ being Relation st b₁ is COMPLEX -valued holds
b₁ is complex-valued

proof end;

cluster Relation-like ExtREAL -valued -> ext-real-valued set ;
coherence
for b₁ being Relation st b₁ is ExtREAL -valued holds
b₁ is ext-real-valued

proof end;

cluster Relation-like REAL -valued -> real-valued set ;
coherence
for b₁ being Relation st b₁ is REAL -valued holds
b₁ is real-valued

proof end;

cluster Relation-like RAT -valued -> rational-valued set ;
coherence
for b₁ being Relation st b₁ is RAT -valued holds
b₁ is rational-valued

proof end;

cluster Relation-like INT -valued -> integer-valued set ;
coherence
for b₁ being Relation st b₁ is INT -valued holds
b₁ is integer-valued

proof end;

cluster Relation-like NAT -valued -> natural-valued set ;
coherence
for b₁ being Relation st b₁ is NAT -valued holds
b₁ is natural-valued

proof end;

end;