:: VALUED_0 semantic presentation
begin
definition
let f be Relation;
attrf is complex-valued means :Def1: :: VALUED_0:def 1
rng f c= COMPLEX ;
attrf is ext-real-valued means :Def2: :: VALUED_0:def 2
rng f c= ExtREAL ;
attrf is real-valued means :Def3: :: VALUED_0:def 3
rng f c= REAL ;
canceled;
canceled;
attrf 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 VALUED_0:def_4_:_
canceled;
:: deftheorem VALUED_0:def_5_:_
canceled;
:: 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 -> INT -valued for set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is INT -valued
proof
let R be Relation; ::_thesis: ( R is natural-valued implies R is INT -valued )
assume rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is INT -valued
hence rng R c= INT by NUMBERS:17, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
cluster Relation-like INT -valued -> RAT -valued for set ;
coherence
for b1 being Relation st b1 is INT -valued holds
b1 is RAT -valued
proof
let R be Relation; ::_thesis: ( R is INT -valued implies R is RAT -valued )
assume rng R c= INT ; :: according to RELAT_1:def_19 ::_thesis: R is RAT -valued
hence rng R c= RAT by NUMBERS:14, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
cluster Relation-like INT -valued -> real-valued for set ;
coherence
for b1 being Relation st b1 is INT -valued holds
b1 is real-valued
proof
let R be Relation; ::_thesis: ( R is INT -valued implies R is real-valued )
assume rng R c= INT ; :: according to RELAT_1:def_19 ::_thesis: R is real-valued
hence rng R c= REAL by XBOOLE_1:1, NUMBERS:15; :: according to VALUED_0:def_3 ::_thesis: verum
end;
cluster Relation-like RAT -valued -> real-valued for set ;
coherence
for b1 being Relation st b1 is RAT -valued holds
b1 is real-valued
proof
let R be Relation; ::_thesis: ( R is RAT -valued implies R is real-valued )
assume rng R c= RAT ; :: according to RELAT_1:def_19 ::_thesis: R is real-valued
hence rng R c= REAL by NUMBERS:12, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
end;
cluster Relation-like real-valued -> ext-real-valued for set ;
coherence
for b1 being Relation st b1 is real-valued holds
b1 is ext-real-valued
proof
let R be Relation; ::_thesis: ( R is real-valued implies R is ext-real-valued )
assume rng R c= REAL ; :: according to VALUED_0:def_3 ::_thesis: R is ext-real-valued
hence rng R c= ExtREAL by NUMBERS:31, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
end;
cluster Relation-like real-valued -> complex-valued for set ;
coherence
for b1 being Relation st b1 is real-valued holds
b1 is complex-valued
proof
let R be Relation; ::_thesis: ( R is real-valued implies R is complex-valued )
assume rng R c= REAL ; :: according to VALUED_0:def_3 ::_thesis: R is complex-valued
hence rng R c= COMPLEX by NUMBERS:11, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
cluster Relation-like natural-valued -> RAT -valued for set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is RAT -valued
proof
let R be Relation; ::_thesis: ( R is natural-valued implies R is RAT -valued )
assume rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is RAT -valued
hence rng R c= RAT by NUMBERS:18, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
cluster Relation-like natural-valued -> real-valued for set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is real-valued
proof
let R be Relation; ::_thesis: ( R is natural-valued implies R is real-valued )
assume rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is real-valued
hence rng R c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
end;
end;
registration
cluster empty Relation-like -> natural-valued for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is natural-valued
proof
let R be Relation; ::_thesis: ( R is empty implies R is natural-valued )
assume R is empty ; ::_thesis: R is natural-valued
hence rng R c= NAT by RELAT_1:38, XBOOLE_1:2; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like natural-valued for set ;
existence
ex b1 being Function st b1 is natural-valued
proof
take {} ; ::_thesis: {} is natural-valued
thus {} is natural-valued ; ::_thesis: verum
end;
end;
registration
let R be complex-valued Relation;
cluster rng R -> complex-membered ;
coherence
rng R is complex-membered
proof
rng R c= COMPLEX by Def1;
hence rng R is complex-membered ; ::_thesis: verum
end;
end;
registration
let R be ext-real-valued Relation;
cluster rng R -> ext-real-membered ;
coherence
rng R is ext-real-membered
proof
rng R c= ExtREAL by Def2;
hence rng R is ext-real-membered ; ::_thesis: verum
end;
end;
registration
let R be real-valued Relation;
cluster rng R -> real-membered ;
coherence
rng R is real-membered
proof
rng R c= REAL by Def3;
hence rng R is real-membered ; ::_thesis: verum
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
rng R c= NAT by Def6;
hence rng R is natural-membered ; ::_thesis: verum
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
let R be Relation; ::_thesis: for S being complex-valued Relation st R c= S holds
R is complex-valued
let S be complex-valued Relation; ::_thesis: ( R c= S implies R is complex-valued )
assume R c= S ; ::_thesis: R is complex-valued
then A1: rng R c= rng S by RELAT_1:11;
rng S c= COMPLEX by Def1;
hence rng R c= COMPLEX by A1, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
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
let R be Relation; ::_thesis: for S being ext-real-valued Relation st R c= S holds
R is ext-real-valued
let S be ext-real-valued Relation; ::_thesis: ( R c= S implies R is ext-real-valued )
assume R c= S ; ::_thesis: R is ext-real-valued
then A1: rng R c= rng S by RELAT_1:11;
rng S c= ExtREAL by Def2;
hence rng R c= ExtREAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
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
let R be Relation; ::_thesis: for S being real-valued Relation st R c= S holds
R is real-valued
let S be real-valued Relation; ::_thesis: ( R c= S implies R is real-valued )
assume R c= S ; ::_thesis: R is real-valued
then A1: rng R c= rng S by RELAT_1:11;
rng S c= REAL by Def3;
hence rng R c= REAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
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
let R be Relation; ::_thesis: for S being natural-valued Relation st R c= S holds
R is natural-valued
let S be natural-valued Relation; ::_thesis: ( R c= S implies R is natural-valued )
assume R c= S ; ::_thesis: R is natural-valued
then A1: rng R c= rng S by RELAT_1:11;
rng S c= NAT by Def6;
hence rng R c= NAT by A1, XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum
end;
registration
let R be complex-valued Relation;
cluster -> complex-valued for Element of bool R;
coherence
for b1 being Subset of R holds b1 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 b1 being Subset of R holds b1 is ext-real-valued by Th2;
end;
registration
let R be real-valued Relation;
cluster -> real-valued for Element of bool R;
coherence
for b1 being Subset of R holds b1 is real-valued by Th3;
end;
registration
let R be RAT -valued Relation;
cluster -> RAT -valued for Element of bool R;
coherence
for b1 being Subset of R holds b1 is RAT -valued ;
end;
registration
let R be INT -valued Relation;
cluster -> INT -valued for Element of bool R;
coherence
for b1 being Subset of R holds b1 is INT -valued ;
end;
registration
let R be natural-valued Relation;
cluster -> natural-valued for Element of bool R;
coherence
for b1 being Subset of R holds b1 is natural-valued by Th6;
end;
registration
let R, S be complex-valued Relation;
clusterR \/ S -> complex-valued ;
coherence
R \/ S is complex-valued
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
( rng R c= COMPLEX & rng S c= COMPLEX ) by Def1;
hence rng (R \/ S) c= COMPLEX by A1, XBOOLE_1:8; :: according to VALUED_0:def_1 ::_thesis: verum
end;
end;
registration
let R, S be ext-real-valued Relation;
clusterR \/ S -> ext-real-valued ;
coherence
R \/ S is ext-real-valued
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
( rng R c= ExtREAL & rng S c= ExtREAL ) by Def2;
hence rng (R \/ S) c= ExtREAL by A1, XBOOLE_1:8; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;
registration
let R, S be real-valued Relation;
clusterR \/ S -> real-valued ;
coherence
R \/ S is real-valued
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
( rng R c= REAL & rng S c= REAL ) by Def3;
hence rng (R \/ S) c= REAL by A1, XBOOLE_1:8; :: according to VALUED_0:def_3 ::_thesis: verum
end;
end;
registration
let R, S be RAT -valued Relation;
clusterR \/ S -> RAT -valued ;
coherence
R \/ S is RAT -valued ;
end;
registration
let R, S be INT -valued Relation;
clusterR \/ S -> INT -valued ;
coherence
R \/ S is INT -valued ;
end;
registration
let R, S be natural-valued Relation;
clusterR \/ S -> natural-valued ;
coherence
R \/ S is natural-valued
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
( rng R c= NAT & rng S c= NAT ) by Def6;
hence rng (R \/ S) c= NAT by A1, XBOOLE_1:8; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;
registration
let R be complex-valued Relation;
let S be Relation;
clusterR /\ S -> complex-valued ;
coherence
R /\ S is complex-valued
proof
R /\ S c= R by XBOOLE_1:17;
then A1: rng (R /\ S) c= rng R by RELAT_1:11;
rng R c= COMPLEX by Def1;
hence rng (R /\ S) c= COMPLEX by A1, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
clusterR \ S -> complex-valued ;
coherence
R \ S is complex-valued ;
end;
registration
let R be ext-real-valued Relation;
let S be Relation;
clusterR /\ S -> ext-real-valued ;
coherence
R /\ S is ext-real-valued
proof
R /\ S c= R by XBOOLE_1:17;
then A1: rng (R /\ S) c= rng R by RELAT_1:11;
rng R c= ExtREAL by Def2;
hence rng (R /\ S) c= ExtREAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
end;
clusterR \ S -> ext-real-valued ;
coherence
R \ S is ext-real-valued ;
end;
registration
let R be real-valued Relation;
let S be Relation;
clusterR /\ S -> real-valued ;
coherence
R /\ S is real-valued
proof
R /\ S c= R by XBOOLE_1:17;
then A1: rng (R /\ S) c= rng R by RELAT_1:11;
rng R c= REAL by Def3;
hence rng (R /\ S) c= REAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
end;
clusterR \ S -> real-valued ;
coherence
R \ S is real-valued ;
end;
registration
let R be RAT -valued Relation;
let S be Relation;
clusterR /\ S -> RAT -valued ;
coherence
R /\ S is RAT -valued ;
clusterR \ S -> RAT -valued ;
coherence
R \ S is RAT -valued ;
end;
registration
let R be INT -valued Relation;
let S be Relation;
clusterR /\ S -> INT -valued ;
coherence
R /\ S is INT -valued ;
clusterR \ S -> INT -valued ;
coherence
R \ S is INT -valued ;
end;
registration
let R be natural-valued Relation;
let S be Relation;
clusterR /\ S -> natural-valued ;
coherence
R /\ S is natural-valued
proof
R /\ S c= R by XBOOLE_1:17;
then A1: rng (R /\ S) c= rng R by RELAT_1:11;
rng R c= NAT by Def6;
hence rng (R /\ S) c= NAT by A1, XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum
end;
clusterR \ S -> natural-valued ;
coherence
R \ S is natural-valued ;
end;
registration
let R, S be complex-valued Relation;
clusterR \+\ S -> complex-valued ;
coherence
R \+\ S is complex-valued ;
end;
registration
let R, S be ext-real-valued Relation;
clusterR \+\ S -> ext-real-valued ;
coherence
R \+\ S is ext-real-valued ;
end;
registration
let R, S be real-valued Relation;
clusterR \+\ S -> real-valued ;
coherence
R \+\ S is real-valued ;
end;
registration
let R, S be RAT -valued Relation;
clusterR \+\ S -> RAT -valued ;
coherence
R \+\ S is RAT -valued ;
end;
registration
let R, S be INT -valued Relation;
clusterR \+\ S -> INT -valued ;
coherence
R \+\ S is INT -valued ;
end;
registration
let R, S be natural-valued Relation;
clusterR \+\ S -> natural-valued ;
coherence
R \+\ S is natural-valued ;
end;
registration
let R be complex-valued Relation;
let X be set ;
clusterR .: X -> complex-membered ;
coherence
R .: X is complex-membered
proof
R .: X c= rng R by RELAT_1:111;
hence R .: X is complex-membered ; ::_thesis: verum
end;
end;
registration
let R be ext-real-valued Relation;
let X be set ;
clusterR .: X -> ext-real-membered ;
coherence
R .: X is ext-real-membered
proof
R .: X c= rng R by RELAT_1:111;
hence R .: X is ext-real-membered ; ::_thesis: verum
end;
end;
registration
let R be real-valued Relation;
let X be set ;
clusterR .: X -> real-membered ;
coherence
R .: X is real-membered
proof
R .: X c= rng R by RELAT_1:111;
hence R .: X is real-membered ; ::_thesis: verum
end;
end;
registration
let R be RAT -valued Relation;
let X be set ;
clusterR .: X -> rational-membered ;
coherence
R .: X is rational-membered
proof
R .: X c= rng R by RELAT_1:111;
hence R .: X is rational-membered ; ::_thesis: verum
end;
end;
registration
let R be INT -valued Relation;
let X be set ;
clusterR .: X -> integer-membered ;
coherence
R .: X is integer-membered
proof
R .: X c= rng R by RELAT_1:111;
hence R .: X is integer-membered ; ::_thesis: verum
end;
end;
registration
let R be natural-valued Relation;
let X be set ;
clusterR .: X -> natural-membered ;
coherence
R .: X is natural-membered
proof
R .: X c= rng R by RELAT_1:111;
hence R .: X is natural-membered ; ::_thesis: verum
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 RAT -valued Relation;
let x be set ;
cluster Im (R,x) -> rational-membered ;
coherence
Im (R,x) is rational-membered ;
end;
registration
let R be INT -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 ;
clusterR | X -> complex-valued ;
coherence
R | X is complex-valued
proof
( rng R c= COMPLEX & rng (R | X) c= rng R ) by Def1, RELAT_1:70;
hence rng (R | X) c= COMPLEX by XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
end;
registration
let R be ext-real-valued Relation;
let X be set ;
clusterR | X -> ext-real-valued ;
coherence
R | X is ext-real-valued
proof
( rng R c= ExtREAL & rng (R | X) c= rng R ) by Def2, RELAT_1:70;
hence rng (R | X) c= ExtREAL by XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;
registration
let R be real-valued Relation;
let X be set ;
clusterR | X -> real-valued ;
coherence
R | X is real-valued
proof
( rng R c= REAL & rng (R | X) c= rng R ) by Def3, RELAT_1:70;
hence rng (R | X) c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
end;
end;
registration
let R be RAT -valued Relation;
let X be set ;
clusterR | X -> RAT -valued ;
coherence
R | X is RAT -valued ;
end;
registration
let R be INT -valued Relation;
let X be set ;
clusterR | X -> INT -valued ;
coherence
R | X is INT -valued ;
end;
registration
let R be natural-valued Relation;
let X be set ;
clusterR | X -> natural-valued ;
coherence
R | X is natural-valued
proof
( rng R c= NAT & rng (R | X) c= rng R ) by Def6, RELAT_1:70;
hence rng (R | X) c= NAT by XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;
registration
let X be complex-membered set ;
cluster id X -> complex-valued ;
coherence
id X is complex-valued
proof
thus rng (id X) c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
end;
registration
let X be ext-real-membered set ;
cluster id X -> ext-real-valued ;
coherence
id X is ext-real-valued
proof
thus rng (id X) c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;
registration
let X be real-membered set ;
cluster id X -> real-valued ;
coherence
id X is real-valued
proof
thus rng (id X) c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum
end;
end;
registration
let X be rational-membered set ;
cluster id X -> RAT -valued ;
coherence
id X is RAT -valued
proof
thus rng (id X) c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
registration
let X be integer-membered set ;
cluster id X -> INT -valued ;
coherence
id X is INT -valued
proof
thus rng (id X) c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
registration
let X be natural-membered set ;
cluster id X -> natural-valued ;
coherence
id X is natural-valued
proof
thus rng (id X) c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;
registration
let R be Relation;
let S be complex-valued Relation;
clusterR * S -> complex-valued ;
coherence
R * S is complex-valued
proof
( rng S c= COMPLEX & rng (R * S) c= rng S ) by Def1, RELAT_1:26;
hence rng (R * S) c= COMPLEX by XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
end;
registration
let R be Relation;
let S be ext-real-valued Relation;
clusterR * S -> ext-real-valued ;
coherence
R * S is ext-real-valued
proof
( rng S c= ExtREAL & rng (R * S) c= rng S ) by Def2, RELAT_1:26;
hence rng (R * S) c= ExtREAL by XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;
registration
let R be Relation;
let S be real-valued Relation;
clusterR * S -> real-valued ;
coherence
R * S is real-valued
proof
( rng S c= REAL & rng (R * S) c= rng S ) by Def3, RELAT_1:26;
hence rng (R * S) c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
end;
end;
registration
let R be Relation;
let S be RAT -valued Relation;
clusterR * S -> RAT -valued ;
coherence
R * S is RAT -valued ;
end;
registration
let R be Relation;
let S be INT -valued Relation;
clusterR * S -> INT -valued ;
coherence
R * S is INT -valued ;
end;
registration
let R be Relation;
let S be natural-valued Relation;
clusterR * S -> natural-valued ;
coherence
R * S is natural-valued
proof
( rng S c= NAT & rng (R * S) c= rng S ) by Def6, RELAT_1:26;
hence rng (R * S) c= NAT by XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum
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
thus ( f is complex-valued implies for x being set st x in dom f holds
f . x is complex ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is complex ) implies f is complex-valued )
proof
assume A1: f is complex-valued ; ::_thesis: for x being set st x in dom f holds
f . x is complex
let x be set ; ::_thesis: ( x in dom f implies f . x is complex )
assume A2: x in dom f ; ::_thesis: f . x is complex
reconsider f = f as complex-valued Function by A1;
f . x in rng f by A2, FUNCT_1:3;
hence f . x is complex ; ::_thesis: verum
end;
assume A3: for x being set st x in dom f holds
f . x is complex ; ::_thesis: f is complex-valued
let y be set ; :: according to TARSKI:def_3,VALUED_0:def_1 ::_thesis: ( not y in rng f or y in COMPLEX )
assume y in rng f ; ::_thesis: y in COMPLEX
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then y is complex by A3;
hence y in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
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
thus ( f is ext-real-valued implies for x being set st x in dom f holds
f . x is ext-real ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is ext-real ) implies f is ext-real-valued )
proof
assume A4: f is ext-real-valued ; ::_thesis: for x being set st x in dom f holds
f . x is ext-real
let x be set ; ::_thesis: ( x in dom f implies f . x is ext-real )
assume A5: x in dom f ; ::_thesis: f . x is ext-real
reconsider f = f as ext-real-valued Function by A4;
f . x in rng f by A5, FUNCT_1:3;
hence f . x is ext-real ; ::_thesis: verum
end;
assume A6: for x being set st x in dom f holds
f . x is ext-real ; ::_thesis: f is ext-real-valued
let y be set ; :: according to TARSKI:def_3,VALUED_0:def_2 ::_thesis: ( not y in rng f or y in ExtREAL )
assume y in rng f ; ::_thesis: y in ExtREAL
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then y is ext-real by A6;
hence y in ExtREAL by XXREAL_0:def_1; ::_thesis: verum
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
thus ( f is real-valued implies for x being set st x in dom f holds
f . x is real ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is real ) implies f is real-valued )
proof
assume A7: f is real-valued ; ::_thesis: for x being set st x in dom f holds
f . x is real
let x be set ; ::_thesis: ( x in dom f implies f . x is real )
assume A8: x in dom f ; ::_thesis: f . x is real
reconsider f = f as real-valued Function by A7;
f . x in rng f by A8, FUNCT_1:3;
hence f . x is real ; ::_thesis: verum
end;
assume A9: for x being set st x in dom f holds
f . x is real ; ::_thesis: f is real-valued
let y be set ; :: according to TARSKI:def_3,VALUED_0:def_3 ::_thesis: ( not y in rng f or y in REAL )
assume y in rng f ; ::_thesis: y in REAL
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then y is real by A9;
hence y in REAL by XREAL_0:def_1; ::_thesis: verum
end;
canceled;
canceled;
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
thus ( f is natural-valued implies for x being set st x in dom f holds
f . x is natural ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is natural ) implies f is natural-valued )
proof
assume A10: f is natural-valued ; ::_thesis: for x being set st x in dom f holds
f . x is natural
let x be set ; ::_thesis: ( x in dom f implies f . x is natural )
assume A11: x in dom f ; ::_thesis: f . x is natural
reconsider f = f as natural-valued Function by A10;
f . x in rng f by A11, FUNCT_1:3;
hence f . x is natural ; ::_thesis: verum
end;
assume A12: for x being set st x in dom f holds
f . x is natural ; ::_thesis: f is natural-valued
let y be set ; :: according to TARSKI:def_3,VALUED_0:def_6 ::_thesis: ( not y in rng f or y in NAT )
assume y in rng f ; ::_thesis: y in NAT
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then y is natural by A12;
hence y in NAT by ORDINAL1:def_12; ::_thesis: verum
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 VALUED_0:def_10_:_
canceled;
:: deftheorem VALUED_0:def_11_:_
canceled;
:: 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
let f be Function; ::_thesis: ( f is complex-valued iff for x being set holds f . x is complex )
hereby ::_thesis: ( ( for x being set holds f . x is complex ) implies f is complex-valued )
assume A1: f is complex-valued ; ::_thesis: for x being set holds f . b2 is complex
let x be set ; ::_thesis: f . b1 is complex
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is complex
hence f . x is complex by A1, Def7; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is complex
hence f . x is complex by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume for x being set holds f . x is complex ; ::_thesis: f is complex-valued
then for x being set st x in dom f holds
f . x is complex ;
hence f is complex-valued by Def7; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is ext-real-valued iff for x being set holds f . x is ext-real )
hereby ::_thesis: ( ( for x being set holds f . x is ext-real ) implies f is ext-real-valued )
assume A1: f is ext-real-valued ; ::_thesis: for x being set holds f . b2 is ext-real
let x be set ; ::_thesis: f . b1 is ext-real
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is ext-real
hence f . x is ext-real by A1, Def8; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is ext-real
hence f . x is ext-real by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume for x being set holds f . x is ext-real ; ::_thesis: f is ext-real-valued
then for x being set st x in dom f holds
f . x is ext-real ;
hence f is ext-real-valued by Def8; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is real-valued iff for x being set holds f . x is real )
hereby ::_thesis: ( ( for x being set holds f . x is real ) implies f is real-valued )
assume A1: f is real-valued ; ::_thesis: for x being set holds f . b2 is real
let x be set ; ::_thesis: f . b1 is real
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is real
hence f . x is real by A1, Def9; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is real
hence f . x is real by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume for x being set holds f . x is real ; ::_thesis: f is real-valued
then for x being set st x in dom f holds
f . x is real ;
hence f is real-valued by Def9; ::_thesis: verum
end;
theorem Th10: :: VALUED_0:10
for f being Function holds
( f is RAT -valued iff for x being set holds f . x is rational )
proof
let f be Function; ::_thesis: ( f is RAT -valued iff for x being set holds f . x is rational )
hereby ::_thesis: ( ( for x being set holds f . x is rational ) implies f is RAT -valued )
assume A1: f is RAT -valued ; ::_thesis: for x being set holds f . b2 is rational
let x be set ; ::_thesis: f . b1 is rational
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is rational
then f . x in rng f by FUNCT_1:def_3;
hence f . x is rational by A1; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is rational
hence f . x is rational by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume A2: for x being set holds f . x is rational ; ::_thesis: f is RAT -valued
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng f or y in RAT )
assume y in rng f ; ::_thesis: y in RAT
then consider x being set such that
x in dom f and
A3: f . x = y by FUNCT_1:def_3;
f . x is rational by A2;
hence y in RAT by A3, RAT_1:def_2; ::_thesis: verum
end;
theorem Th11: :: VALUED_0:11
for f being Function holds
( f is INT -valued iff for x being set holds f . x is integer )
proof
let f be Function; ::_thesis: ( f is INT -valued iff for x being set holds f . x is integer )
hereby ::_thesis: ( ( for x being set holds f . x is integer ) implies f is INT -valued )
assume A1: f is INT -valued ; ::_thesis: for x being set holds f . b2 is integer
let x be set ; ::_thesis: f . b1 is integer
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is integer
then f . x in rng f by FUNCT_1:def_3;
hence f . x is integer by A1; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is integer
hence f . x is integer by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume A2: for x being set holds f . x is integer ; ::_thesis: f is INT -valued
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng f or y in INT )
assume y in rng f ; ::_thesis: y in INT
then consider x being set such that
x in dom f and
A3: f . x = y by FUNCT_1:def_3;
f . x is integer by A2;
hence y in INT by A3, INT_1:def_2; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is natural-valued iff for x being set holds f . x is natural )
hereby ::_thesis: ( ( for x being set holds f . x is natural ) implies f is natural-valued )
assume A1: f is natural-valued ; ::_thesis: for x being set holds f . b2 is natural
let x be set ; ::_thesis: f . b1 is natural
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is natural
hence f . x is natural by A1, Def12; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is natural
hence f . x is natural by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume for x being set holds f . x is natural ; ::_thesis: f is natural-valued
then for x being set st x in dom f holds
f . x is natural ;
hence f is natural-valued by Def12; ::_thesis: verum
end;
registration
let f be complex-valued Function;
let x be set ;
clusterf . x -> complex ;
coherence
f . x is complex by Th7;
end;
registration
let f be ext-real-valued Function;
let x be set ;
clusterf . x -> ext-real ;
coherence
f . x is ext-real by Th8;
end;
registration
let f be real-valued Function;
let x be set ;
clusterf . x -> real ;
coherence
f . x is real by Th9;
end;
registration
let f be RAT -valued Function;
let x be set ;
clusterf . x -> rational ;
coherence
f . x is rational by Th10;
end;
registration
let f be INT -valued Function;
let x be set ;
clusterf . x -> integer ;
coherence
f . x is integer by Th11;
end;
registration
let f be natural-valued Function;
let x be set ;
clusterf . x -> natural ;
coherence
f . x is natural by Th12;
end;
registration
let X be set ;
let x be complex number ;
clusterX --> x -> complex-valued ;
coherence
X --> x is complex-valued
proof
rng (X --> x) c= COMPLEX by MEMBERED:1;
hence X --> x is complex-valued by Def1; ::_thesis: verum
end;
end;
registration
let X be set ;
let x be ext-real number ;
clusterX --> x -> ext-real-valued ;
coherence
X --> x is ext-real-valued
proof
rng (X --> x) c= ExtREAL by MEMBERED:2;
hence X --> x is ext-real-valued by Def2; ::_thesis: verum
end;
end;
registration
let X be set ;
let x be real number ;
clusterX --> x -> real-valued ;
coherence
X --> x is real-valued
proof
rng (X --> x) c= REAL by MEMBERED:3;
hence X --> x is real-valued by Def3; ::_thesis: verum
end;
end;
registration
let X be set ;
let x be rational number ;
clusterX --> x -> RAT -valued ;
coherence
X --> x is RAT -valued
proof
rng (X --> x) c= RAT by MEMBERED:4;
hence X --> x is RAT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
registration
let X be set ;
let x be integer number ;
clusterX --> x -> INT -valued ;
coherence
X --> x is INT -valued
proof
rng (X --> x) c= INT by MEMBERED:5;
hence X --> x is INT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
registration
let X be set ;
let x be Nat;
clusterX --> x -> natural-valued ;
coherence
X --> x is natural-valued
proof
rng (X --> x) c= NAT by MEMBERED:6;
hence X --> x is natural-valued by Def6; ::_thesis: verum
end;
end;
registration
let f, g be complex-valued Function;
clusterf +* g -> complex-valued ;
coherence
f +* g is complex-valued
proof
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then rng (f +* g) c= COMPLEX by MEMBERED:1;
hence f +* g is complex-valued by Def1; ::_thesis: verum
end;
end;
registration
let f, g be ext-real-valued Function;
clusterf +* g -> ext-real-valued ;
coherence
f +* g is ext-real-valued
proof
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then rng (f +* g) c= ExtREAL by MEMBERED:2;
hence f +* g is ext-real-valued by Def2; ::_thesis: verum
end;
end;
registration
let f, g be real-valued Function;
clusterf +* g -> real-valued ;
coherence
f +* g is real-valued
proof
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then rng (f +* g) c= REAL by MEMBERED:3;
hence f +* g is real-valued by Def3; ::_thesis: verum
end;
end;
registration
let f, g be RAT -valued Function;
clusterf +* g -> RAT -valued ;
coherence
f +* g is RAT -valued
proof
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then rng (f +* g) c= RAT by MEMBERED:4;
hence f +* g is RAT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
registration
let f, g be INT -valued Function;
clusterf +* g -> INT -valued ;
coherence
f +* g is INT -valued
proof
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then rng (f +* g) c= INT by MEMBERED:5;
hence f +* g is INT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
registration
let f, g be natural-valued Function;
clusterf +* g -> natural-valued ;
coherence
f +* g is natural-valued
proof
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then rng (f +* g) c= NAT by MEMBERED:6;
hence f +* g is natural-valued by Def6; ::_thesis: verum
end;
end;
registration
let x be set ;
let y be complex number ;
clusterx .--> y -> complex-valued ;
coherence
x .--> y is complex-valued ;
end;
registration
let x be set ;
let y be ext-real number ;
clusterx .--> y -> ext-real-valued ;
coherence
x .--> y is ext-real-valued ;
end;
registration
let x be set ;
let y be real number ;
clusterx .--> y -> real-valued ;
coherence
x .--> y is real-valued ;
end;
registration
let x be set ;
let y be rational number ;
clusterx .--> y -> RAT -valued ;
coherence
x .--> y is RAT -valued ;
end;
registration
let x be set ;
let y be integer number ;
clusterx .--> y -> INT -valued ;
coherence
x .--> y is INT -valued ;
end;
registration
let x be set ;
let y be Nat;
clusterx .--> 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 b1 being Relation of X,Y holds b1 is complex-valued
proof
let R be Relation of X,Y; ::_thesis: R is complex-valued
thus rng R c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum
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 b1 being Relation of X,Y holds b1 is ext-real-valued
proof
let R be Relation of X,Y; ::_thesis: R is ext-real-valued
thus rng R c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;
registration
let X be set ;
let Y be real-membered set ;
cluster -> real-valued for Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is real-valued
proof
let R be Relation of X,Y; ::_thesis: R is real-valued
thus rng R c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum
end;
end;
registration
let X be set ;
let Y be rational-membered set ;
cluster -> RAT -valued for Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is RAT -valued
proof
let R be Relation of X,Y; ::_thesis: R is RAT -valued
thus rng R c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
registration
let X be set ;
let Y be integer-membered set ;
cluster -> INT -valued for Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is INT -valued
proof
let R be Relation of X,Y; ::_thesis: R is INT -valued
thus rng R c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
registration
let X be set ;
let Y be natural-membered set ;
cluster -> natural-valued for Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is natural-valued
proof
let R be Relation of X,Y; ::_thesis: R is natural-valued
thus rng R c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum
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
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum
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
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum
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
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum
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
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum
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
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum
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
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;
notation
let f be ext-real-valued Relation;
synonym non-zero f for non-empty ;
end;
registration
cluster non empty Relation-like RAT -valued INT -valued Function-like constant natural-valued for set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is constant & b1 is natural-valued & b1 is INT -valued & b1 is RAT -valued )
proof
take 1 .--> 1 ; ::_thesis: ( not 1 .--> 1 is empty & 1 .--> 1 is constant & 1 .--> 1 is natural-valued & 1 .--> 1 is INT -valued & 1 .--> 1 is RAT -valued )
thus ( not 1 .--> 1 is empty & 1 .--> 1 is constant & 1 .--> 1 is natural-valued & 1 .--> 1 is INT -valued & 1 .--> 1 is RAT -valued ) ; ::_thesis: verum
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
let f be non empty constant complex-valued Function; ::_thesis: ex r being complex number st
for x being set st x in dom f holds
f . x = r
consider r being set such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set such that
A2: x in dom f by XBOOLE_0:def_1;
r = f . x by A1, A2;
hence ex r being complex number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
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
let f be non empty constant ext-real-valued Function; ::_thesis: ex r being ext-real number st
for x being set st x in dom f holds
f . x = r
consider r being set such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set such that
A2: x in dom f by XBOOLE_0:def_1;
r = f . x by A1, A2;
hence ex r being ext-real number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
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
let f be non empty constant real-valued Function; ::_thesis: ex r being real number st
for x being set st x in dom f holds
f . x = r
consider r being set such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set such that
A2: x in dom f by XBOOLE_0:def_1;
r = f . x by A1, A2;
hence ex r being real number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
end;
theorem :: VALUED_0:16
for f being non empty RAT -valued constant Function ex r being rational number st
for x being set st x in dom f holds
f . x = r
proof
let f be non empty RAT -valued constant Function; ::_thesis: ex r being rational number st
for x being set st x in dom f holds
f . x = r
consider r being set such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set such that
A2: x in dom f by XBOOLE_0:def_1;
r = f . x by A1, A2;
hence ex r being rational number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
end;
theorem :: VALUED_0:17
for f being non empty INT -valued constant Function ex r being integer number st
for x being set st x in dom f holds
f . x = r
proof
let f be non empty INT -valued constant Function; ::_thesis: ex r being integer number st
for x being set st x in dom f holds
f . x = r
consider r being set such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set such that
A2: x in dom f by XBOOLE_0:def_1;
r = f . x by A1, A2;
hence ex r being integer number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
end;
theorem :: VALUED_0:18
for f being non empty constant natural-valued Function ex r being Nat st
for x being set st x in dom f holds
f . x = r
proof
let f be non empty constant natural-valued Function; ::_thesis: ex r being Nat st
for x being set st x in dom f holds
f . x = r
consider r being set such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set such that
A2: x in dom f by XBOOLE_0:def_1;
r = f . x by A1, A2;
hence ex r being Nat st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
end;
begin
definition
let f be ext-real-valued Function;
attrf 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;
attrf 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;
attrf 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;
attrf 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 for set ;
coherence
for b1 being ext-real-valued Function st b1 is trivial holds
( b1 is increasing & b1 is decreasing )
proof
let f be ext-real-valued Function; ::_thesis: ( f is trivial implies ( f is increasing & f is decreasing ) )
assume A1: f is trivial ; ::_thesis: ( f is increasing & f is decreasing )
thus f is increasing ::_thesis: f is decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 < f . e2 )
assume ( e1 in dom f & e2 in dom f ) ; ::_thesis: ( not e1 < e2 or f . e1 < f . e2 )
hence ( not e1 < e2 or f . e1 < f . e2 ) by A1, ZFMISC_1:def_10; ::_thesis: verum
end;
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 > f . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 > f . e2 )
assume ( e1 in dom f & e2 in dom f ) ; ::_thesis: ( not e1 < e2 or f . e1 > f . e2 )
hence ( not e1 < e2 or f . e1 > f . e2 ) by A1, ZFMISC_1:def_10; ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like ext-real-valued increasing -> ext-real-valued non-decreasing for set ;
coherence
for b1 being ext-real-valued Function st b1 is increasing holds
b1 is non-decreasing
proof
let f be ext-real-valued Function; ::_thesis: ( f is increasing implies f is non-decreasing )
assume A1: f is increasing ; ::_thesis: f is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 <= e2 implies f . e1 <= f . e2 )
assume that
A2: ( e1 in dom f & e2 in dom f ) and
A3: e1 <= e2 ; ::_thesis: f . e1 <= f . e2
percases ( e1 = e2 or e1 < e2 ) by A3, XXREAL_0:1;
suppose e1 = e2 ; ::_thesis: f . e1 <= f . e2
hence f . e1 <= f . e2 ; ::_thesis: verum
end;
suppose e1 < e2 ; ::_thesis: f . e1 <= f . e2
hence f . e1 <= f . e2 by A1, A2, Def13; ::_thesis: verum
end;
end;
end;
cluster Relation-like Function-like ext-real-valued decreasing -> ext-real-valued non-increasing for set ;
coherence
for b1 being ext-real-valued Function st b1 is decreasing holds
b1 is non-increasing
proof
let f be ext-real-valued Function; ::_thesis: ( f is decreasing implies f is non-increasing )
assume A4: f is decreasing ; ::_thesis: f is non-increasing
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 >= f . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 <= e2 implies f . e1 >= f . e2 )
assume that
A5: ( e1 in dom f & e2 in dom f ) and
A6: e1 <= e2 ; ::_thesis: f . e1 >= f . e2
percases ( e1 = e2 or e1 < e2 ) by A6, XXREAL_0:1;
suppose e1 = e2 ; ::_thesis: f . e1 >= f . e2
hence f . e1 >= f . e2 ; ::_thesis: verum
end;
suppose e1 < e2 ; ::_thesis: f . e1 >= f . e2
hence f . e1 >= f . e2 by A4, A5, Def14; ::_thesis: verum
end;
end;
end;
end;
registration
let f, g be ext-real-valued increasing Function;
clusterf * g -> increasing ;
coherence
g * f is increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds
(g * f) . e1 < (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 < (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 < (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume e1 < e2 ; ::_thesis: (g * f) . e1 < (g * f) . e2
then A7: f . e1 < f . e2 by A3, A5, Def13;
( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence (g * f) . e1 < (g * f) . e2 by A4, A6, A7, Def13; ::_thesis: verum
end;
end;
registration
let f, g be ext-real-valued non-decreasing Function;
clusterf * g -> non-decreasing ;
coherence
g * f is non-decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds
(g * f) . e1 <= (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 <= (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 <= (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume e1 <= e2 ; ::_thesis: (g * f) . e1 <= (g * f) . e2
then A7: f . e1 <= f . e2 by A3, A5, Def15;
( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence (g * f) . e1 <= (g * f) . e2 by A4, A6, A7, Def15; ::_thesis: verum
end;
end;
registration
let f, g be ext-real-valued decreasing Function;
clusterf * g -> increasing ;
coherence
g * f is increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds
(g * f) . e1 < (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 < (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 < (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume e1 < e2 ; ::_thesis: (g * f) . e1 < (g * f) . e2
then A7: f . e1 > f . e2 by A3, A5, Def14;
( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence (g * f) . e1 < (g * f) . e2 by A4, A6, A7, Def14; ::_thesis: verum
end;
end;
registration
let f, g be ext-real-valued non-increasing Function;
clusterf * g -> non-decreasing ;
coherence
g * f is non-decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds
(g * f) . e1 <= (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 <= (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 <= (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume e1 <= e2 ; ::_thesis: (g * f) . e1 <= (g * f) . e2
then A7: f . e1 >= f . e2 by A3, A5, Def16;
( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence (g * f) . e1 <= (g * f) . e2 by A4, A6, A7, Def16; ::_thesis: verum
end;
end;
registration
let f be ext-real-valued decreasing Function;
let g be ext-real-valued increasing Function;
clusterf * g -> decreasing ;
coherence
g * f is decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds
(g * f) . e1 > (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 > (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 > (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume e1 < e2 ; ::_thesis: (g * f) . e1 > (g * f) . e2
then A7: f . e1 > f . e2 by A3, A5, Def14;
( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence (g * f) . e1 > (g * f) . e2 by A4, A6, A7, Def13; ::_thesis: verum
end;
clusterg * f -> decreasing ;
coherence
f * g is decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom (f * g) & e2 in dom (f * g) & e1 < e2 holds
(f * g) . e1 > (f * g) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (f * g) & e2 in dom (f * g) & e1 < e2 implies (f * g) . e1 > (f * g) . e2 )
assume that
A8: e1 in dom (f * g) and
A9: e2 in dom (f * g) ; ::_thesis: ( not e1 < e2 or (f * g) . e1 > (f * g) . e2 )
A10: e1 in dom g by A8, FUNCT_1:11;
then A11: (f * g) . e1 = f . (g . e1) by FUNCT_1:13;
A12: e2 in dom g by A9, FUNCT_1:11;
then A13: (f * g) . e2 = f . (g . e2) by FUNCT_1:13;
assume e1 < e2 ; ::_thesis: (f * g) . e1 > (f * g) . e2
then A14: g . e1 < g . e2 by A10, A12, Def13;
( g . e1 in dom f & g . e2 in dom f ) by A8, A9, FUNCT_1:11;
hence (f * g) . e1 > (f * g) . e2 by A11, A13, A14, Def14; ::_thesis: verum
end;
end;
registration
let f be ext-real-valued non-increasing Function;
let g be ext-real-valued non-decreasing Function;
clusterf * g -> non-increasing ;
coherence
g * f is non-increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds
(g * f) . e1 >= (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 >= (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 >= (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume e1 <= e2 ; ::_thesis: (g * f) . e1 >= (g * f) . e2
then A7: f . e1 >= f . e2 by A3, A5, Def16;
( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence (g * f) . e1 >= (g * f) . e2 by A4, A6, A7, Def15; ::_thesis: verum
end;
clusterg * f -> non-increasing ;
coherence
f * g is non-increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom (f * g) & e2 in dom (f * g) & e1 <= e2 holds
(f * g) . e1 >= (f * g) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (f * g) & e2 in dom (f * g) & e1 <= e2 implies (f * g) . e1 >= (f * g) . e2 )
assume that
A8: e1 in dom (f * g) and
A9: e2 in dom (f * g) ; ::_thesis: ( not e1 <= e2 or (f * g) . e1 >= (f * g) . e2 )
A10: e1 in dom g by A8, FUNCT_1:11;
then A11: (f * g) . e1 = f . (g . e1) by FUNCT_1:13;
A12: e2 in dom g by A9, FUNCT_1:11;
then A13: (f * g) . e2 = f . (g . e2) by FUNCT_1:13;
assume e1 <= e2 ; ::_thesis: (f * g) . e1 >= (f * g) . e2
then A14: g . e1 <= g . e2 by A10, A12, Def15;
( g . e1 in dom f & g . e2 in dom f ) by A8, A9, FUNCT_1:11;
hence (f * g) . e1 >= (f * g) . e2 by A11, A13, A14, Def16; ::_thesis: verum
end;
end;
registration
let X be ext-real-membered set ;
cluster id X -> increasing for Function of X,X;
coherence
for b1 being Function of X,X st b1 = id X holds
b1 is increasing
proof
id X is increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (id X) & e2 in dom (id X) & e1 < e2 holds
(id X) . e1 < (id X) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (id X) & e2 in dom (id X) & e1 < e2 implies (id X) . e1 < (id X) . e2 )
assume that
A1: e1 in dom (id X) and
A2: e2 in dom (id X) ; ::_thesis: ( not e1 < e2 or (id X) . e1 < (id X) . e2 )
(id X) . e1 = e1 by A1, FUNCT_1:18;
hence ( not e1 < e2 or (id X) . e1 < (id X) . e2 ) by A2, FUNCT_1:18; ::_thesis: verum
end;
hence for b1 being Function of X,X st b1 = id X holds
b1 is increasing ; ::_thesis: verum
end;
end;
registration
cluster non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing for Element of bool [:NAT,NAT:];
existence
ex b1 being sequence of NAT st b1 is increasing
proof
take id NAT ; ::_thesis: id NAT is increasing
thus id NAT is increasing ; ::_thesis: verum
end;
end;
definition
let s be ManySortedSet of NAT ;
mode subsequence of s -> ManySortedSet of NAT means :Def17: :: VALUED_0:def 17
ex N being increasing sequence of NAT st it = s * N;
existence
ex b1 being ManySortedSet of NAT ex N being increasing sequence of NAT st b1 = s * N
proof
take s ; ::_thesis: ex N being increasing sequence of NAT st s = s * N
take id NAT ; ::_thesis: s = s * (id NAT)
dom s = NAT by PARTFUN1:def_2;
hence s = s * (id NAT) by RELAT_1:52; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines subsequence VALUED_0:def_17_:_
for s, b2 being ManySortedSet of NAT holds
( b2 is subsequence of s iff ex N being increasing sequence of NAT st b2 = 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
let x be non empty set ; ::_thesis: for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M
let M be ManySortedSet of NAT ; ::_thesis: for s being subsequence of M holds rng s c= rng M
let s be subsequence of M; ::_thesis: rng s c= rng M
ex N being increasing sequence of NAT st s = M * N by Def17;
hence rng s c= rng M by RELAT_1:26; ::_thesis: verum
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 b1 being subsequence of s holds b1 is X -valued
proof
let ss be subsequence of s; ::_thesis: ss is X -valued
rng ss c= rng s by Lm1;
hence rng ss c= X by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
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 b1 being subsequence of s holds b1 is sequence of X
proof
let ss be subsequence of s; ::_thesis: ss is sequence of X
( rng ss c= X & dom ss = NAT ) by PARTFUN1:def_2;
hence ss is sequence of X by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let s be sequence of X;
let k be Nat;
:: original: ^\
redefine funcs ^\ k -> subsequence of s;
coherence
s ^\ k is subsequence of s
proof
set N = (id NAT) ^\ k;
(id NAT) ^\ k is increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) & e1 < e2 holds
((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) & e1 < e2 implies ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 )
assume ( e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) ) ; ::_thesis: ( not e1 < e2 or ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 )
then reconsider i = e1, j = e2 as Element of NAT ;
A1: ((id NAT) ^\ k) . j = (id NAT) . (j + k) by NAT_1:def_3
.= j + k by FUNCT_1:18 ;
assume A2: e1 < e2 ; ::_thesis: ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2
((id NAT) ^\ k) . i = (id NAT) . (i + k) by NAT_1:def_3
.= i + k by FUNCT_1:18 ;
hence ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 by A1, A2, XREAL_1:6; ::_thesis: verum
end;
then reconsider N = (id NAT) ^\ k as increasing sequence of NAT ;
thus s ^\ k is subsequence of s ::_thesis: verum
proof
take N ; :: according to VALUED_0:def_17 ::_thesis: s ^\ k = s * N
thus s ^\ k = (s * (id NAT)) ^\ k by FUNCT_2:17
.= s * N by NAT_1:50 ; ::_thesis: verum
end;
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
let XX be non empty set ; ::_thesis: for ss being sequence of XX holds ss is subsequence of ss
let ss be sequence of XX; ::_thesis: ss is subsequence of ss
take id NAT ; :: according to VALUED_0:def_17 ::_thesis: ss = ss * (id NAT)
thus ss = ss * (id NAT) by FUNCT_2:17; ::_thesis: verum
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
let XX be non empty set ; ::_thesis: 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
let ss1, ss2, ss3 be sequence of XX; ::_thesis: ( ss1 is subsequence of ss2 & ss2 is subsequence of ss3 implies ss1 is subsequence of ss3 )
given N1 being increasing sequence of NAT such that A1: ss1 = ss2 * N1 ; :: according to VALUED_0:def_17 ::_thesis: ( not ss2 is subsequence of ss3 or ss1 is subsequence of ss3 )
given N2 being increasing sequence of NAT such that A2: ss2 = ss3 * N2 ; :: according to VALUED_0:def_17 ::_thesis: ss1 is subsequence of ss3
take N2 * N1 ; :: according to VALUED_0:def_17 ::_thesis: ss1 = ss3 * (N2 * N1)
thus ss1 = ss3 * (N2 * N1) by A1, A2, RELAT_1:36; ::_thesis: verum
end;
registration
let X be set ;
cluster Relation-like NAT -defined X -valued Function-like constant quasi_total for Element of bool [:NAT,X:];
existence
ex b1 being sequence of X st b1 is constant
proof
percases ( X = {} or X <> {} ) ;
suppose X = {} ; ::_thesis: ex b1 being sequence of X st b1 is constant
then reconsider s = {} as sequence of X by FUNCT_2:def_1, RELSET_1:12;
take s ; ::_thesis: s is constant
thus s is constant ; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: ex b1 being sequence of X st b1 is constant
then consider x being set such that
A1: x in X by XBOOLE_0:def_1;
reconsider s = NAT --> x as sequence of X by A1, FUNCOP_1:45;
take s ; ::_thesis: s is constant
thus s is constant ; ::_thesis: verum
end;
end;
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
let XX be non empty set ; ::_thesis: for ss being sequence of XX
for ss1 being subsequence of ss holds rng ss1 c= rng ss
let ss be sequence of XX; ::_thesis: for ss1 being subsequence of ss holds rng ss1 c= rng ss
let ss1 be subsequence of ss; ::_thesis: rng ss1 c= rng ss
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ss1 or x in rng ss )
consider N being increasing sequence of NAT such that
A1: ss1 = ss * N by Def17;
assume x in rng ss1 ; ::_thesis: x in rng ss
then consider n being set such that
A2: n in NAT and
A3: x = ss1 . n by FUNCT_2:11;
A4: N . n in NAT by A2, FUNCT_2:5;
x = ss . (N . n) by A1, A2, A3, FUNCT_2:15;
hence x in rng ss by A4, FUNCT_2:4; ::_thesis: verum
end;
registration
let X be non empty set ;
let s be constant sequence of X;
cluster -> constant for subsequence of s;
coherence
for b1 being subsequence of s holds b1 is constant
proof
let s1 be subsequence of s; ::_thesis: s1 is constant
rng s1 c= rng s by Th21;
hence s1 is constant ; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let N be increasing sequence of NAT;
let s be sequence of X;
:: original: *
redefine funcs * N -> subsequence of s;
correctness
coherence
N * s is subsequence of s;
by Def17;
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
let X, Y be non empty set ; ::_thesis: 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
let s, s1 be sequence of X; ::_thesis: 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
let h be PartFunc of X,Y; ::_thesis: ( rng s c= dom h & s1 is subsequence of s implies h /* s1 is subsequence of h /* s )
assume that
A1: rng s c= dom h and
A2: s1 is subsequence of s ; ::_thesis: h /* s1 is subsequence of h /* s
consider N being increasing sequence of NAT such that
A3: s1 = s * N by A2, Def17;
take N ; :: according to VALUED_0:def_17 ::_thesis: h /* s1 = (h /* s) * N
thus h /* s1 = (h /* s) * N by A1, A3, FUNCT_2:110; ::_thesis: verum
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 for Element of bool [:NAT,X:];
existence
ex b1 being sequence of X st b1 is non-empty
proof
consider x being non empty set such that
A1: x in X by SETFAM_1:def_10;
reconsider s = NAT --> x as sequence of X by A1, FUNCOP_1:45;
take s ; ::_thesis: s is non-empty
thus s is non-empty ; ::_thesis: verum
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 b1 being subsequence of s holds b1 is non-empty
proof
let s1 be subsequence of s; ::_thesis: s1 is non-empty
rng s1 c= rng s by Th21;
hence not {} in rng s1 ; :: according to RELAT_1:def_9 ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let s be sequence of X;
:: original: constant
redefine attrs 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
hereby ::_thesis: ( ex x being Element of X st
for n being Nat holds s . n = x implies s is constant )
assume s is constant ; ::_thesis: ex x being Element of X st
for n being Nat holds s . n = x
then consider x being Element of X such that
A1: for n being Element of NAT st n in dom s holds
s . n = x by PARTFUN2:def_1;
take x = x; ::_thesis: for n being Nat holds s . n = x
let n be Nat; ::_thesis: s . n = x
( dom s = NAT & n in NAT ) by FUNCT_2:def_1, ORDINAL1:def_12;
hence s . n = x by A1; ::_thesis: verum
end;
given x being Element of X such that A2: for n being Nat holds s . n = x ; ::_thesis: s is constant
take x ; :: according to PARTFUN2:def_1 ::_thesis: for b1 being Element of NAT holds
( not b1 in dom s or s . b1 = x )
thus for b1 being Element of NAT holds
( not b1 in dom s or s . b1 = x ) by A2; ::_thesis: verum
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
let i, j be Nat; ::_thesis: for X being set
for s being constant sequence of X holds s . i = s . j
let X be set ; ::_thesis: for s being constant sequence of X holds s . i = s . j
let s be constant sequence of X; ::_thesis: s . i = s . j
percases ( X is empty or not X is empty ) ;
supposeA1: X is empty ; ::_thesis: s . i = s . j
then s . i = {} ;
hence s . i = s . j by A1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: s . i = s . j
then dom s = NAT by FUNCT_2:def_1;
then ( i in dom s & j in dom s ) by ORDINAL1:def_12;
hence s . i = s . j by FUNCT_1:def_10; ::_thesis: verum
end;
end;
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 V29()
proof
let X be non empty set ; ::_thesis: for s being sequence of X st ( for i, j being Nat holds s . i = s . j ) holds
s is V29()
let s be sequence of X; ::_thesis: ( ( for i, j being Nat holds s . i = s . j ) implies s is V29() )
assume for i, j being Nat holds s . i = s . j ; ::_thesis: s is V29()
then for x, y being set st x in dom s & y in dom s holds
s . x = s . y ;
hence s is V29() by FUNCT_1:def_10; ::_thesis: verum
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 V29()
proof
let X be non empty set ; ::_thesis: for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds
s is V29()
let s be sequence of X; ::_thesis: ( ( for i being Nat holds s . i = s . (i + 1) ) implies s is V29() )
assume A1: for i being Nat holds s . i = s . (i + 1) ; ::_thesis: s is V29()
now__::_thesis:_for_i,_j_being_Nat_holds_s_._i_=_s_._j
let i, j be Nat; ::_thesis: s . i = s . j
A2: now__::_thesis:_for_i,_j_being_Nat_st_i_<=_j_holds_
s_._i_=_s_._j
let i, j be Nat; ::_thesis: ( i <= j implies s . i = s . j )
assume A3: i <= j ; ::_thesis: s . i = s . j
defpred S1[ Nat] means ( i <= $1 implies s . i = s . $1 );
A4: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A5: S1[j] ; ::_thesis: S1[j + 1]
assume i <= j + 1 ; ::_thesis: s . i = s . (j + 1)
then ( i < j + 1 or i = j + 1 ) by XXREAL_0:1;
hence s . i = s . (j + 1) by A1, A5, NAT_1:13; ::_thesis: verum
end;
A6: S1[ 0 ] by NAT_1:3;
for j being Nat holds S1[j] from NAT_1:sch_2(A6, A4);
hence s . i = s . j by A3; ::_thesis: verum
end;
( i <= j or j <= i ) ;
hence s . i = s . j by A2; ::_thesis: verum
end;
hence s is V29() by Th24; ::_thesis: verum
end;
theorem :: VALUED_0:26
for X being non empty set
for s, s1 being sequence of X st s is V29() & s1 is subsequence of s holds
s = s1
proof
let X be non empty set ; ::_thesis: for s, s1 being sequence of X st s is V29() & s1 is subsequence of s holds
s = s1
let s, s1 be sequence of X; ::_thesis: ( s is V29() & s1 is subsequence of s implies s = s1 )
assume that
A1: s is V29() and
A2: s1 is subsequence of s ; ::_thesis: s = s1
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: s . n = s1 . n
consider N being increasing sequence of NAT such that
A3: s1 = s * N by A2, Def17;
thus s1 . n = s . (N . n) by A3, FUNCT_2:15
.= s . n by A1, Th23 ; ::_thesis: verum
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
let X, Y be non empty set ; ::_thesis: 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)
let s be sequence of X; ::_thesis: for h being PartFunc of X,Y
for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)
let h be PartFunc of X,Y; ::_thesis: for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)
let n be Nat; ::_thesis: ( rng s c= dom h implies (h /* s) ^\ n = h /* (s ^\ n) )
assume A1: rng s c= dom h ; ::_thesis: (h /* s) ^\ n = h /* (s ^\ n)
let m be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((h /* s) ^\ n) . m = (h /* (s ^\ n)) . m
A2: rng (s ^\ n) c= rng s by Th21;
thus ((h /* s) ^\ n) . m = (h /* s) . (m + n) by NAT_1:def_3
.= h . (s . (m + n)) by A1, FUNCT_2:108
.= h . ((s ^\ n) . m) by NAT_1:def_3
.= (h /* (s ^\ n)) . m by A1, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for s being sequence of X
for n being Nat holds s . n in rng s
let s be sequence of X; ::_thesis: for n being Nat holds s . n in rng s
let n be Nat; ::_thesis: s . n in rng s
n in NAT by ORDINAL1:def_12;
hence s . n in rng s by FUNCT_2:112; ::_thesis: verum
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
let X, Y be non empty set ; ::_thesis: 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
let s be sequence of X; ::_thesis: for h being PartFunc of X,Y
for n being Nat st h is total holds
h /* (s ^\ n) = (h /* s) ^\ n
let h be PartFunc of X,Y; ::_thesis: for n being Nat st h is total holds
h /* (s ^\ n) = (h /* s) ^\ n
let n be Nat; ::_thesis: ( h is total implies h /* (s ^\ n) = (h /* s) ^\ n )
assume h is total ; ::_thesis: h /* (s ^\ n) = (h /* s) ^\ n
then dom h = X by PARTFUN1:def_2;
then rng s c= dom h ;
hence h /* (s ^\ n) = (h /* s) ^\ n by Th27; ::_thesis: verum
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
let X, Y be non empty set ; ::_thesis: 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)
let s be sequence of X; ::_thesis: for h being PartFunc of X,Y st rng s c= dom h holds
h .: (rng s) = rng (h /* s)
let h be PartFunc of X,Y; ::_thesis: ( rng s c= dom h implies h .: (rng s) = rng (h /* s) )
assume A1: rng s c= dom h ; ::_thesis: h .: (rng s) = rng (h /* s)
now__::_thesis:_for_r_being_Element_of_Y_holds_
(_(_r_in_h_.:_(rng_s)_implies_r_in_rng_(h_/*_s)_)_&_(_r_in_rng_(h_/*_s)_implies_r_in_h_.:_(rng_s)_)_)
let r be Element of Y; ::_thesis: ( ( r in h .: (rng s) implies r in rng (h /* s) ) & ( r in rng (h /* s) implies r in h .: (rng s) ) )
thus ( r in h .: (rng s) implies r in rng (h /* s) ) ::_thesis: ( r in rng (h /* s) implies r in h .: (rng s) )
proof
assume r in h .: (rng s) ; ::_thesis: r in rng (h /* s)
then consider p being Element of X such that
p in dom h and
A2: p in rng s and
A3: r = h . p by PARTFUN2:59;
consider n being Element of NAT such that
A4: p = s . n by A2, FUNCT_2:113;
r = (h /* s) . n by A1, A3, A4, FUNCT_2:108;
hence r in rng (h /* s) by Th28; ::_thesis: verum
end;
assume r in rng (h /* s) ; ::_thesis: r in h .: (rng s)
then consider n being Element of NAT such that
A5: (h /* s) . n = r by FUNCT_2:113;
A6: s . n in rng s by Th28;
r = h . (s . n) by A1, A5, FUNCT_2:108;
hence r in h .: (rng s) by A1, A6, FUNCT_1:def_6; ::_thesis: verum
end;
hence h .: (rng s) = rng (h /* s) by SUBSET_1:3; ::_thesis: verum
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
let X, Y be non empty set ; ::_thesis: 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
let Z be set ; ::_thesis: 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
let s be sequence of X; ::_thesis: 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
let h1 be PartFunc of X,Y; ::_thesis: for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
let h2 be PartFunc of Y,Z; ::_thesis: ( rng s c= dom (h2 * h1) implies h2 /* (h1 /* s) = (h2 * h1) /* s )
assume A1: rng s c= dom (h2 * h1) ; ::_thesis: h2 /* (h1 /* s) = (h2 * h1) /* s
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h2_*_h1)_/*_s)_._n_=_(h2_/*_(h1_/*_s))_._n
let n be Element of NAT ; ::_thesis: ((h2 * h1) /* s) . n = (h2 /* (h1 /* s)) . n
A2: rng s c= dom h1 by A1, FUNCT_1:101;
h1 .: (rng s) c= dom h2 by A1, FUNCT_1:101;
then A3: rng (h1 /* s) c= dom h2 by A2, Th30;
s . n in rng s by Th28;
then A4: s . n in dom h1 by A1, FUNCT_1:11;
thus ((h2 * h1) /* s) . n = (h2 * h1) . (s . n) by A1, FUNCT_2:108
.= h2 . (h1 . (s . n)) by A4, FUNCT_1:13
.= h2 . ((h1 /* s) . n) by A2, FUNCT_2:108
.= (h2 /* (h1 /* s)) . n by A3, FUNCT_2:108 ; ::_thesis: verum
end;
hence h2 /* (h1 /* s) = (h2 * h1) /* s by FUNCT_2:63; ::_thesis: verum
end;
definition
let f be ext-real-valued Function;
attrf 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 for set ;
coherence
for b1 being Relation st b1 is COMPLEX -valued holds
b1 is complex-valued
proof
let R be Relation; ::_thesis: ( R is COMPLEX -valued implies R is complex-valued )
assume R is COMPLEX -valued ; ::_thesis: R is complex-valued
hence rng R c= COMPLEX by RELAT_1:def_19; :: according to VALUED_0:def_1 ::_thesis: verum
end;
cluster Relation-like ExtREAL -valued -> ext-real-valued for set ;
coherence
for b1 being Relation st b1 is ExtREAL -valued holds
b1 is ext-real-valued
proof
let R be Relation; ::_thesis: ( R is ExtREAL -valued implies R is ext-real-valued )
assume R is ExtREAL -valued ; ::_thesis: R is ext-real-valued
hence rng R c= ExtREAL by RELAT_1:def_19; :: according to VALUED_0:def_2 ::_thesis: verum
end;
cluster Relation-like REAL -valued -> real-valued for set ;
coherence
for b1 being Relation st b1 is REAL -valued holds
b1 is real-valued
proof
let R be Relation; ::_thesis: ( R is REAL -valued implies R is real-valued )
assume R is REAL -valued ; ::_thesis: R is real-valued
hence rng R c= REAL by RELAT_1:def_19; :: according to VALUED_0:def_3 ::_thesis: verum
end;
cluster Relation-like NAT -valued -> natural-valued for set ;
coherence
for b1 being Relation st b1 is NAT -valued holds
b1 is natural-valued
proof
let R be Relation; ::_thesis: ( R is NAT -valued implies R is natural-valued )
assume R is NAT -valued ; ::_thesis: R is natural-valued
hence rng R c= NAT by RELAT_1:def_19; :: according to VALUED_0:def_6 ::_thesis: verum
end;
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
A1: dom s = NAT by PARTFUN1:def_2;
hereby ::_thesis: ( ex x being set st
for n being Nat holds s . n = x implies s is constant )
assume A2: s is constant ; ::_thesis: ex x being set st
for n being Nat holds s . n = x
take x = s . 0; ::_thesis: for n being Nat holds s . n = x
let n be Nat; ::_thesis: s . n = x
( 0 in dom s & n in dom s ) by A1, ORDINAL1:def_12;
hence s . n = x by A2, FUNCT_1:def_10; ::_thesis: verum
end;
given x being set such that A3: for n being Nat holds s . n = x ; ::_thesis: s is constant
let n1, n2 be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not n1 in dom s or not n2 in dom s or s . n1 = s . n2 )
assume A4: ( n1 in dom s & n2 in dom s ) ; ::_thesis: s . n1 = s . n2
hence s . n1 = x by A3
.= s . n2 by A3, A4 ;
::_thesis: verum
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 b1 being ManySortedSet of X st b1 is natural-valued
proof
take X --> 0 ; ::_thesis: X --> 0 is natural-valued
thus X --> 0 is natural-valued ; ::_thesis: verum
end;
end;