:: by Library Committee

::

:: Received November 22, 2007

:: Copyright (c) 2007-2019 Association of Mizar Users

:: deftheorem Def1 defines complex-valued VALUED_0:def 1 :

for f being Relation holds

( f is complex-valued iff rng f c= COMPLEX );

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

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

for f being Relation holds

( f is real-valued iff rng f c= REAL );

:: deftheorem Def4 defines natural-valued VALUED_0:def 6 :

for f being Relation holds

( f is natural-valued iff rng f c= NAT );

for f being Relation holds

( f is natural-valued iff rng f c= NAT );

registration

coherence

for b_{1} being Relation st b_{1} is natural-valued holds

b_{1} is INT -valued

for b_{1} being Relation st b_{1} is INT -valued holds

b_{1} is RAT -valued

for b_{1} being Relation st b_{1} is INT -valued holds

b_{1} is real-valued

for b_{1} being Relation st b_{1} is RAT -valued holds

b_{1} is real-valued

for b_{1} being Relation st b_{1} is real-valued holds

b_{1} is ext-real-valued

for b_{1} being Relation st b_{1} is real-valued holds

b_{1} is complex-valued

for b_{1} being Relation st b_{1} is natural-valued holds

b_{1} is RAT -valued

for b_{1} being Relation st b_{1} is natural-valued holds

b_{1} is real-valued

end;
for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration
end;

theorem :: VALUED_0:4

theorem :: VALUED_0:5

registration

let R be complex-valued Relation;

coherence

for b_{1} being Subset of R holds b_{1} is complex-valued
by Th1;

end;
coherence

for b

registration

let R be ext-real-valued Relation;

coherence

for b_{1} being Subset of R holds b_{1} is ext-real-valued
by Th2;

end;
coherence

for b

registration

let R be real-valued Relation;

coherence

for b_{1} being Subset of R holds b_{1} is real-valued
by Th3;

end;
coherence

for b

registration
end;

registration
end;

registration

let R be natural-valued Relation;

coherence

for b_{1} being Subset of R holds b_{1} is natural-valued
by Th6;

end;
coherence

for b

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let R be complex-valued Relation;

let S be Relation;

coherence

R /\ S is complex-valued

R \ S is complex-valued ;

end;
let S be Relation;

coherence

R /\ S is complex-valued

proof end;

coherence R \ S is complex-valued ;

registration

let R be ext-real-valued Relation;

let S be Relation;

coherence

R /\ S is ext-real-valued

R \ S is ext-real-valued ;

end;
let S be Relation;

coherence

R /\ S is ext-real-valued

proof end;

coherence R \ S is ext-real-valued ;

registration

let R be real-valued Relation;

let S be Relation;

coherence

R /\ S is real-valued

R \ S is real-valued ;

end;
let S be Relation;

coherence

R /\ S is real-valued

proof end;

coherence R \ S is real-valued ;

registration

let R be RAT -valued Relation;

let S be Relation;

coherence

R /\ S is RAT -valued ;

coherence

R \ S is RAT -valued ;

end;
let S be Relation;

coherence

R /\ S is RAT -valued ;

coherence

R \ S is RAT -valued ;

registration

let R be INT -valued Relation;

let S be Relation;

coherence

R /\ S is INT -valued ;

coherence

R \ S is INT -valued ;

end;
let S be Relation;

coherence

R /\ S is INT -valued ;

coherence

R \ S is INT -valued ;

registration

let R be natural-valued Relation;

let S be Relation;

coherence

R /\ S is natural-valued

R \ S is natural-valued ;

end;
let S be Relation;

coherence

R /\ S is natural-valued

proof end;

coherence R \ S is natural-valued ;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

definition

let f be Function;

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

f . x is complex )

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

f . x is ext-real )

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

f . x is real )

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

f . x is natural )

end;
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 for x being object st x in dom f holds

f . x is complex ;

( 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 for x being object st x in dom f holds

f . x is ext-real ;

( 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 for x being object st x in dom f holds

f . x is real ;

( 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 for x being object st x in dom f holds

f . x is natural ;

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

f . x is natural )

proof 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 );

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

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

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

for f being Function holds

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

f . x is natural );

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let X be set ;

let Y be complex-membered set ;

coherence

for b_{1} being Relation of X,Y holds b_{1} is complex-valued

end;
let Y be complex-membered set ;

coherence

for b

proof end;

registration

let X be set ;

let Y be ext-real-membered set ;

coherence

for b_{1} being Relation of X,Y holds b_{1} is ext-real-valued

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

coherence

for b

proof end;

registration

let X be set ;

let Y be real-membered set ;

coherence

for b_{1} being Relation of X,Y holds b_{1} is real-valued

end;
let Y be real-membered set ;

coherence

for b

proof end;

registration

let X be set ;

let Y be rational-membered set ;

coherence

for b_{1} being Relation of X,Y holds b_{1} is RAT -valued

end;
let Y be rational-membered set ;

coherence

for b

proof end;

registration

let X be set ;

let Y be integer-membered set ;

coherence

for b_{1} being Relation of X,Y holds b_{1} is INT -valued

end;
let Y be integer-membered set ;

coherence

for b

proof end;

registration

let X be set ;

let Y be natural-membered set ;

coherence

for b_{1} being Relation of X,Y holds b_{1} is natural-valued

end;
let Y be natural-membered set ;

coherence

for b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

:::notation

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

:::end;

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

:::end;

registration

ex b_{1} being Function st

( not b_{1} is empty & b_{1} is constant & b_{1} is natural-valued & b_{1} is INT -valued & b_{1} is RAT -valued )
end;

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

existence ex b

( not b

proof 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

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

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

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

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

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

for x being object st x in dom f holds

f . x = r

proof end;

definition

let f be ext-real-valued Function;

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

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;

for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 < e2 holds

f . e1 > f . e2;

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

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

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

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

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

for b_{1} being ext-real-valued Function st b_{1} is trivial holds

( b_{1} is increasing & b_{1} is decreasing )
by ZFMISC_1:def 10;

end;

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

coherence for b

( b

registration

for b_{1} being ext-real-valued Function st b_{1} is increasing holds

b_{1} is non-decreasing

for b_{1} being ext-real-valued Function st b_{1} is decreasing holds

b_{1} is non-increasing
end;

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

coherence for b

b

proof end;

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

coherence for b

b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let f be ext-real-valued decreasing Function;

let g be ext-real-valued increasing Function;

coherence

g * f is decreasing

f * g is decreasing

end;
let g be ext-real-valued increasing Function;

coherence

g * f is decreasing

proof end;

coherence f * g is decreasing

proof end;

registration

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

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

coherence

g * f is non-increasing

f * g is non-increasing

end;
let g be ext-real-valued non-decreasing Function;

coherence

g * f is non-increasing

proof end;

coherence f * g is non-increasing

proof end;

registration

let X be ext-real-membered set ;

coherence

for b_{1} being Function of X,X st b_{1} = id X holds

b_{1} is increasing

end;
coherence

for b

b

proof end;

registration

ex b_{1} being sequence of NAT st b_{1} is increasing
end;

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

proof end;

definition

let s be ManySortedSet of NAT ;

ex b_{1} being ManySortedSet of NAT ex N being increasing sequence of NAT st b_{1} = s * N

end;
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 N being increasing sequence of NAT st it = s * N;

ex b

proof end;

:: deftheorem Def13 defines subsequence VALUED_0:def 17 :

for s, b_{2} being ManySortedSet of NAT holds

( b_{2} is subsequence of s iff ex N being increasing sequence of NAT st b_{2} = s * N );

for s, b

( b

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 ;

coherence

for b_{1} being subsequence of s holds b_{1} is X -valued

end;
let s be X -valued ManySortedSet of NAT ;

coherence

for b

proof 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_{1} being subsequence of s holds b_{1} is sequence of X

end;
let s be sequence of X;

:: original: subsequence

redefine mode subsequence of s -> sequence of X;

coherence

for b

proof 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

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

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

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 ;

ex b_{1} being sequence of X st b_{1} is constant

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

existence ex b

proof 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

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;

coherence

for b_{1} being subsequence of s holds b_{1} is constant

end;
let s be constant sequence of X;

coherence

for b

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

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

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 ;

ex b_{1} being sequence of X st b_{1} is non-empty

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

proof end;

registration

let X be with_non-empty_element set ;

let s be non-empty sequence of X;

coherence

for b_{1} being subsequence of s holds b_{1} is non-empty

end;
let s be non-empty sequence of X;

coherence

for b

proof end;

definition

let X be non empty set ;

let s be sequence of X;

( s is constant iff ex x being Element of X st

for n being Nat holds s . n = x )

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

( s is constant iff ex x being Element of X st

for n being Nat holds s . n = x )

proof 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 );

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 :: VALUED_0:24

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()

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

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)

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

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)

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

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

:: deftheorem defines zeroed VALUED_0:def 19 :

for f being ext-real-valued Function holds

( f is zeroed iff f . {} = 0 );

for f being ext-real-valued Function holds

( f is zeroed iff f . {} = 0 );

:: new, 2009.02.03, A.T.

registration

coherence

for b_{1} being Relation st b_{1} is COMPLEX -valued holds

b_{1} is complex-valued
;

coherence

for b_{1} being Relation st b_{1} is ExtREAL -valued holds

b_{1} is ext-real-valued
;

coherence

for b_{1} being Relation st b_{1} is REAL -valued holds

b_{1} is real-valued
;

coherence

for b_{1} being Relation st b_{1} is NAT -valued holds

b_{1} is natural-valued
;

end;
for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

definition

let s be ManySortedSet of NAT ;

( s is constant iff ex x being set st

for n being Nat holds s . n = x )

end;
redefine attr s is constant means :: VALUED_0:def 20

ex x being set st

for n being Nat holds s . n = x;

compatibility ex x being set st

for n being Nat holds s . n = x;

( s is constant iff ex x being set st

for n being Nat holds s . n = x )

proof 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 );

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;

for M being ManySortedSet of NAT

for s being subsequence of M holds rng s c= rng M by Lm1;

registration
end;