:: RFUNCT_2 semantic presentation
begin
theorem Th1: :: RFUNCT_2:1
for seq1, seq2, seq3 being Real_Sequence holds
( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
proof
let seq1, seq2, seq3 be Real_Sequence; ::_thesis: ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
thus ( seq1 = seq2 - seq3 implies for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 )
proof
assume A1: seq1 = seq2 - seq3 ; ::_thesis: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n)
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_._n)_-_(seq3_._n)
let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 . n) - (seq3 . n)
seq1 . n = (seq2 . n) + ((- seq3) . n) by A1, SEQ_1:7;
then seq1 . n = (seq2 . n) + (- (seq3 . n)) by SEQ_1:10;
hence seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum
end;
hence for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: seq1 = seq2 - seq3
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_._n)_+_((-_seq3)_._n)
let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 . n) + ((- seq3) . n)
thus seq1 . n = (seq2 . n) - (seq3 . n) by A2
.= (seq2 . n) + (- (seq3 . n))
.= (seq2 . n) + ((- seq3) . n) by SEQ_1:10 ; ::_thesis: verum
end;
hence seq1 = seq2 - seq3 by SEQ_1:7; ::_thesis: verum
end;
theorem Th2: :: RFUNCT_2:2
for seq1, seq2 being Real_Sequence
for Ns being V37() sequence of NAT holds
( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )
proof
let seq1, seq2 be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds
( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )
let Ns be V37() sequence of NAT; ::_thesis: ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_+_(seq2_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((seq1 + seq2) * Ns) . n = ((seq1 * Ns) + (seq2 * Ns)) . n
thus ((seq1 + seq2) * Ns) . n = (seq1 + seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) + (seq2 . (Ns . n)) by SEQ_1:7
.= ((seq1 * Ns) . n) + (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) + ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) + (seq2 * Ns)) . n by SEQ_1:7 ; ::_thesis: verum
end;
hence (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) by FUNCT_2:63; ::_thesis: ( (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_-_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_-_(seq2_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((seq1 - seq2) * Ns) . n = ((seq1 * Ns) - (seq2 * Ns)) . n
thus ((seq1 - seq2) * Ns) . n = (seq1 - seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) - (seq2 . (Ns . n)) by Th1
.= ((seq1 * Ns) . n) - (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) - ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) - (seq2 * Ns)) . n by Th1 ; ::_thesis: verum
end;
hence (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) by FUNCT_2:63; ::_thesis: (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_(#)_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_(#)_(seq2_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((seq1 (#) seq2) * Ns) . n = ((seq1 * Ns) (#) (seq2 * Ns)) . n
thus ((seq1 (#) seq2) * Ns) . n = (seq1 (#) seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) * (seq2 . (Ns . n)) by SEQ_1:8
.= ((seq1 * Ns) . n) * (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) * ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) (#) (seq2 * Ns)) . n by SEQ_1:8 ; ::_thesis: verum
end;
hence (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th3: :: RFUNCT_2:3
for p being Element of REAL
for seq being Real_Sequence
for Ns being V37() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)
proof
let p be Element of REAL ; ::_thesis: for seq being Real_Sequence
for Ns being V37() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)
let seq be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)
let Ns be V37() sequence of NAT; ::_thesis: (p (#) seq) * Ns = p (#) (seq * Ns)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((p_(#)_seq)_*_Ns)_._n_=_(p_(#)_(seq_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((p (#) seq) * Ns) . n = (p (#) (seq * Ns)) . n
thus ((p (#) seq) * Ns) . n = (p (#) seq) . (Ns . n) by FUNCT_2:15
.= p * (seq . (Ns . n)) by SEQ_1:9
.= p * ((seq * Ns) . n) by FUNCT_2:15
.= (p (#) (seq * Ns)) . n by SEQ_1:9 ; ::_thesis: verum
end;
hence (p (#) seq) * Ns = p (#) (seq * Ns) by FUNCT_2:63; ::_thesis: verum
end;
theorem :: RFUNCT_2:4
for seq being Real_Sequence
for Ns being V37() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )
proof
let seq be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )
let Ns be V37() sequence of NAT; ::_thesis: ( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )
thus (- seq) * Ns = ((- 1) (#) seq) * Ns
.= (- 1) (#) (seq * Ns) by Th3
.= - (seq * Ns) ; ::_thesis: (abs seq) * Ns = abs (seq * Ns)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((abs_seq)_*_Ns)_._n_=_(abs_(seq_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((abs seq) * Ns) . n = (abs (seq * Ns)) . n
thus ((abs seq) * Ns) . n = (abs seq) . (Ns . n) by FUNCT_2:15
.= abs (seq . (Ns . n)) by SEQ_1:12
.= abs ((seq * Ns) . n) by FUNCT_2:15
.= (abs (seq * Ns)) . n by SEQ_1:12 ; ::_thesis: verum
end;
hence (abs seq) * Ns = abs (seq * Ns) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th5: :: RFUNCT_2:5
for seq being Real_Sequence
for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns
proof
let seq be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns
let Ns be V37() sequence of NAT; ::_thesis: (seq * Ns) " = (seq ") * Ns
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_*_Ns)_")_._n_=_((seq_")_*_Ns)_._n
let n be Element of NAT ; ::_thesis: ((seq * Ns) ") . n = ((seq ") * Ns) . n
thus ((seq * Ns) ") . n = ((seq * Ns) . n) " by VALUED_1:10
.= (seq . (Ns . n)) " by FUNCT_2:15
.= (seq ") . (Ns . n) by VALUED_1:10
.= ((seq ") * Ns) . n by FUNCT_2:15 ; ::_thesis: verum
end;
hence (seq * Ns) " = (seq ") * Ns by FUNCT_2:63; ::_thesis: verum
end;
theorem :: RFUNCT_2:6
for seq1, seq being Real_Sequence
for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
proof
let seq1, seq be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
let Ns be V37() sequence of NAT; ::_thesis: (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
thus (seq1 /" seq) * Ns = (seq1 (#) (seq ")) * Ns
.= (seq1 * Ns) (#) ((seq ") * Ns) by Th2
.= (seq1 * Ns) (#) ((seq * Ns) ") by Th5
.= (seq1 * Ns) /" (seq * Ns) ; ::_thesis: verum
end;
theorem :: RFUNCT_2:7
for seq being Real_Sequence st seq is convergent & ( for n being Element of NAT holds seq . n <= 0 ) holds
lim seq <= 0
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & ( for n being Element of NAT holds seq . n <= 0 ) implies lim seq <= 0 )
assume that
A1: seq is convergent and
A2: for n being Element of NAT holds seq . n <= 0 ; ::_thesis: lim seq <= 0
set seq1 = - seq;
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_-_0_<=_(-_seq)_._n
let n be Element of NAT ; ::_thesis: - 0 <= (- seq) . n
( (- seq) . n = - (seq . n) & seq . n <= 0 ) by A2, SEQ_1:10;
hence - 0 <= (- seq) . n by XREAL_1:24; ::_thesis: verum
end;
- seq is convergent by A1, SEQ_2:9;
then 0 <= lim (- seq) by A3, SEQ_2:17;
then - 0 <= - (lim seq) by A1, SEQ_2:10;
hence lim seq <= 0 by XREAL_1:24; ::_thesis: verum
end;
theorem Th8: :: RFUNCT_2:8
for W being non empty set
for h1, h2 being PartFunc of W,REAL
for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
proof
let W be non empty set ; ::_thesis: for h1, h2 being PartFunc of W,REAL
for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
let h1, h2 be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
let seq be sequence of W; ::_thesis: ( rng seq c= (dom h1) /\ (dom h2) implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) )
A1: (dom h1) /\ (dom h2) c= dom h1 by XBOOLE_1:17;
A2: (dom h1) /\ (dom h2) c= dom h2 by XBOOLE_1:17;
assume A3: rng seq c= (dom h1) /\ (dom h2) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
then A4: rng seq c= dom (h1 + h2) by VALUED_1:def_1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_+_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_+_((h2_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)
A5: seq . n in rng seq by VALUED_0:28;
thus ((h1 + h2) /* seq) . n = (h1 + h2) . (seq . n) by A4, FUNCT_2:108
.= (h1 . (seq . n)) + (h2 . (seq . n)) by A4, A5, VALUED_1:def_1
.= ((h1 /* seq) . n) + (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1
.= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum
end;
hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by SEQ_1:7; ::_thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
A6: rng seq c= dom (h1 - h2) by A3, VALUED_1:12;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_-_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_-_((h2_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)
A7: seq . n in rng seq by VALUED_0:28;
thus ((h1 - h2) /* seq) . n = (h1 - h2) . (seq . n) by A6, FUNCT_2:108
.= (h1 . (seq . n)) - (h2 . (seq . n)) by A6, A7, VALUED_1:13
.= ((h1 /* seq) . n) - (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1
.= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum
end;
hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by Th1; ::_thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)
A8: rng seq c= dom (h1 (#) h2) by A3, VALUED_1:def_4;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_(#)_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_*_((h2_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((h1 (#) h2) /* seq) . n = ((h1 /* seq) . n) * ((h2 /* seq) . n)
thus ((h1 (#) h2) /* seq) . n = (h1 (#) h2) . (seq . n) by A8, FUNCT_2:108
.= (h1 . (seq . n)) * (h2 . (seq . n)) by VALUED_1:5
.= ((h1 /* seq) . n) * (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1
.= ((h1 /* seq) . n) * ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum
end;
hence (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by SEQ_1:8; ::_thesis: verum
end;
theorem Th9: :: RFUNCT_2:9
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W
for r being real number st rng seq c= dom h holds
(r (#) h) /* seq = r (#) (h /* seq)
proof
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL
for seq being sequence of W
for r being real number st rng seq c= dom h holds
(r (#) h) /* seq = r (#) (h /* seq)
let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W
for r being real number st rng seq c= dom h holds
(r (#) h) /* seq = r (#) (h /* seq)
let seq be sequence of W; ::_thesis: for r being real number st rng seq c= dom h holds
(r (#) h) /* seq = r (#) (h /* seq)
let r be real number ; ::_thesis: ( rng seq c= dom h implies (r (#) h) /* seq = r (#) (h /* seq) )
assume A1: rng seq c= dom h ; ::_thesis: (r (#) h) /* seq = r (#) (h /* seq)
then A2: rng seq c= dom (r (#) h) by VALUED_1:def_5;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_h)_/*_seq)_._n_=_r_*_((h_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((r (#) h) /* seq) . n = r * ((h /* seq) . n)
A3: seq . n in rng seq by VALUED_0:28;
thus ((r (#) h) /* seq) . n = (r (#) h) . (seq . n) by A2, FUNCT_2:108
.= r * (h . (seq . n)) by A2, A3, VALUED_1:def_5
.= r * ((h /* seq) . n) by A1, FUNCT_2:108 ; ::_thesis: verum
end;
hence (r (#) h) /* seq = r (#) (h /* seq) by SEQ_1:9; ::_thesis: verum
end;
theorem :: RFUNCT_2:10
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom h holds
( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq )
proof
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom h holds
( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq )
let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom h holds
( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq )
let seq be sequence of W; ::_thesis: ( rng seq c= dom h implies ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq ) )
assume A1: rng seq c= dom h ; ::_thesis: ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq )
then A2: rng seq c= dom (abs h) by VALUED_1:def_11;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(h_/*_seq))_._n_=_((abs_h)_/*_seq)_._n
let n be Element of NAT ; ::_thesis: (abs (h /* seq)) . n = ((abs h) /* seq) . n
thus (abs (h /* seq)) . n = abs ((h /* seq) . n) by SEQ_1:12
.= abs (h . (seq . n)) by A1, FUNCT_2:108
.= (abs h) . (seq . n) by VALUED_1:18
.= ((abs h) /* seq) . n by A2, FUNCT_2:108 ; ::_thesis: verum
end;
hence abs (h /* seq) = (abs h) /* seq by FUNCT_2:63; ::_thesis: - (h /* seq) = (- h) /* seq
thus - (h /* seq) = (- 1) (#) (h /* seq)
.= ((- 1) (#) h) /* seq by A1, Th9
.= (- h) /* seq ; ::_thesis: verum
end;
theorem :: RFUNCT_2:11
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h ^) holds
h /* seq is non-zero
proof
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h ^) holds
h /* seq is non-zero
let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom (h ^) holds
h /* seq is non-zero
let seq be sequence of W; ::_thesis: ( rng seq c= dom (h ^) implies h /* seq is non-zero )
assume A1: rng seq c= dom (h ^) ; ::_thesis: h /* seq is non-zero
then A2: ( (dom h) \ (h " {0}) c= dom h & rng seq c= (dom h) \ (h " {0}) ) by RFUNCT_1:def_2, XBOOLE_1:36;
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(h_/*_seq)_._n_=_0
given n being Element of NAT such that A3: (h /* seq) . n = 0 ; ::_thesis: contradiction
seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h ^) by A1;
then seq . n in (dom h) \ (h " {0}) by RFUNCT_1:def_2;
then ( seq . n in dom h & not seq . n in h " {0} ) by XBOOLE_0:def_5;
then A4: not h . (seq . n) in {0} by FUNCT_1:def_7;
h . (seq . n) = 0 by A2, A3, FUNCT_2:108, XBOOLE_1:1;
hence contradiction by A4, TARSKI:def_1; ::_thesis: verum
end;
hence h /* seq is non-zero by SEQ_1:5; ::_thesis: verum
end;
theorem :: RFUNCT_2:12
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h ^) holds
(h ^) /* seq = (h /* seq) "
proof
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h ^) holds
(h ^) /* seq = (h /* seq) "
let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom (h ^) holds
(h ^) /* seq = (h /* seq) "
let seq be sequence of W; ::_thesis: ( rng seq c= dom (h ^) implies (h ^) /* seq = (h /* seq) " )
assume A1: rng seq c= dom (h ^) ; ::_thesis: (h ^) /* seq = (h /* seq) "
then A2: ( (dom h) \ (h " {0}) c= dom h & rng seq c= (dom h) \ (h " {0}) ) by RFUNCT_1:def_2, XBOOLE_1:36;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_^)_/*_seq)_._n_=_((h_/*_seq)_")_._n
let n be Element of NAT ; ::_thesis: ((h ^) /* seq) . n = ((h /* seq) ") . n
A3: seq . n in rng seq by VALUED_0:28;
thus ((h ^) /* seq) . n = (h ^) . (seq . n) by A1, FUNCT_2:108
.= (h . (seq . n)) " by A1, A3, RFUNCT_1:def_2
.= ((h /* seq) . n) " by A2, FUNCT_2:108, XBOOLE_1:1
.= ((h /* seq) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence (h ^) /* seq = (h /* seq) " by FUNCT_2:63; ::_thesis: verum
end;
theorem :: RFUNCT_2:13
for W being non empty set
for h1, h2 being PartFunc of W,REAL
for seq being sequence of W st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
proof
let W be non empty set ; ::_thesis: for h1, h2 being PartFunc of W,REAL
for seq being sequence of W st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
let h1, h2 be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
let seq be sequence of W; ::_thesis: ( h1 is total & h2 is total implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) )
assume ( h1 is total & h2 is total ) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
then dom (h1 + h2) = W by PARTFUN1:def_2;
then (dom h1) /\ (dom h2) = W by VALUED_1:def_1;
then A1: rng seq c= (dom h1) /\ (dom h2) ;
hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by Th8; ::_thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, Th8; ::_thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)
thus (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by A1, Th8; ::_thesis: verum
end;
theorem :: RFUNCT_2:14
for r being Element of REAL
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
proof
let r be Element of REAL ; ::_thesis: for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL
for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
let seq be sequence of W; ::_thesis: ( h is total implies (r (#) h) /* seq = r (#) (h /* seq) )
assume h is total ; ::_thesis: (r (#) h) /* seq = r (#) (h /* seq)
then dom h = W by PARTFUN1:def_2;
then rng seq c= dom h ;
hence (r (#) h) /* seq = r (#) (h /* seq) by Th9; ::_thesis: verum
end;
theorem :: RFUNCT_2:15
for X being set
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) holds
abs ((h | X) /* seq) = ((abs h) | X) /* seq
proof
let X be set ; ::_thesis: for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) holds
abs ((h | X) /* seq) = ((abs h) | X) /* seq
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) holds
abs ((h | X) /* seq) = ((abs h) | X) /* seq
let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom (h | X) holds
abs ((h | X) /* seq) = ((abs h) | X) /* seq
let seq be sequence of W; ::_thesis: ( rng seq c= dom (h | X) implies abs ((h | X) /* seq) = ((abs h) | X) /* seq )
assume A1: rng seq c= dom (h | X) ; ::_thesis: abs ((h | X) /* seq) = ((abs h) | X) /* seq
A2: dom (h | X) = (dom h) /\ X by RELAT_1:61
.= (dom (abs h)) /\ X by VALUED_1:def_11
.= dom ((abs h) | X) by RELAT_1:61 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_((h_|_X)_/*_seq))_._n_=_(((abs_h)_|_X)_/*_seq)_._n
let n be Element of NAT ; ::_thesis: (abs ((h | X) /* seq)) . n = (((abs h) | X) /* seq) . n
A3: seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h | X) by A1;
then seq . n in (dom h) /\ X by RELAT_1:61;
then A4: seq . n in X by XBOOLE_0:def_4;
thus (abs ((h | X) /* seq)) . n = abs (((h | X) /* seq) . n) by SEQ_1:12
.= abs ((h | X) . (seq . n)) by A1, FUNCT_2:108
.= abs (h . (seq . n)) by A1, A3, FUNCT_1:47
.= (abs h) . (seq . n) by VALUED_1:18
.= ((abs h) | X) . (seq . n) by A4, FUNCT_1:49
.= (((abs h) | X) /* seq) . n by A1, A2, FUNCT_2:108 ; ::_thesis: verum
end;
hence abs ((h | X) /* seq) = ((abs h) | X) /* seq by FUNCT_2:63; ::_thesis: verum
end;
theorem :: RFUNCT_2:16
for X being set
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
proof
let X be set ; ::_thesis: for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
let seq be sequence of W; ::_thesis: ( rng seq c= dom (h | X) & h " {0} = {} implies ((h ^) | X) /* seq = ((h | X) /* seq) " )
assume that
A1: rng seq c= dom (h | X) and
A2: h " {0} = {} ; ::_thesis: ((h ^) | X) /* seq = ((h | X) /* seq) "
now__::_thesis:_for_x_being_set_st_x_in_rng_seq_holds_
x_in_dom_((h_^)_|_X)
let x be set ; ::_thesis: ( x in rng seq implies x in dom ((h ^) | X) )
assume x in rng seq ; ::_thesis: x in dom ((h ^) | X)
then x in dom (h | X) by A1;
then A3: x in (dom h) /\ X by RELAT_1:61;
then x in (dom h) \ (h " {0}) by A2, XBOOLE_0:def_4;
then A4: x in dom (h ^) by RFUNCT_1:def_2;
x in X by A3, XBOOLE_0:def_4;
then x in (dom (h ^)) /\ X by A4, XBOOLE_0:def_4;
hence x in dom ((h ^) | X) by RELAT_1:61; ::_thesis: verum
end;
then A5: rng seq c= dom ((h ^) | X) by TARSKI:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(((h_^)_|_X)_/*_seq)_._n_=_(((h_|_X)_/*_seq)_")_._n
let n be Element of NAT ; ::_thesis: (((h ^) | X) /* seq) . n = (((h | X) /* seq) ") . n
A6: seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h | X) by A1;
then A7: seq . n in (dom h) /\ X by RELAT_1:61;
then A8: seq . n in X by XBOOLE_0:def_4;
seq . n in (dom h) \ (h " {0}) by A2, A7, XBOOLE_0:def_4;
then A9: seq . n in dom (h ^) by RFUNCT_1:def_2;
thus (((h ^) | X) /* seq) . n = ((h ^) | X) . (seq . n) by A5, FUNCT_2:108
.= (h ^) . (seq . n) by A8, FUNCT_1:49
.= (h . (seq . n)) " by A9, RFUNCT_1:def_2
.= ((h | X) . (seq . n)) " by A1, A6, FUNCT_1:47
.= (((h | X) /* seq) . n) " by A1, FUNCT_2:108
.= (((h | X) /* seq) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence ((h ^) | X) /* seq = ((h | X) /* seq) " by FUNCT_2:63; ::_thesis: verum
end;
registration
let Z be set ;
let f be one-to-one Function;
clusterf | Z -> one-to-one ;
coherence
f | Z is one-to-one by FUNCT_1:52;
end;
theorem :: RFUNCT_2:17
for X being set
for h being one-to-one Function holds (h | X) " = (h ") | (h .: X)
proof
let X be set ; ::_thesis: for h being one-to-one Function holds (h | X) " = (h ") | (h .: X)
let h be one-to-one Function; ::_thesis: (h | X) " = (h ") | (h .: X)
reconsider hX = h | X as one-to-one Function ;
now__::_thesis:_for_r_being_set_holds_
(_(_r_in_dom_((h_|_X)_")_implies_r_in_dom_((h_")_|_(h_.:_X))_)_&_(_r_in_dom_((h_")_|_(h_.:_X))_implies_r_in_dom_((h_|_X)_")_)_)
let r be set ; ::_thesis: ( ( r in dom ((h | X) ") implies r in dom ((h ") | (h .: X)) ) & ( r in dom ((h ") | (h .: X)) implies r in dom ((h | X) ") ) )
thus ( r in dom ((h | X) ") implies r in dom ((h ") | (h .: X)) ) ::_thesis: ( r in dom ((h ") | (h .: X)) implies r in dom ((h | X) ") )
proof
assume r in dom ((h | X) ") ; ::_thesis: r in dom ((h ") | (h .: X))
then r in rng hX by FUNCT_1:33;
then consider g being set such that
A1: g in dom (h | X) and
A2: (h | X) . g = r by FUNCT_1:def_3;
A3: h . g = r by A1, A2, FUNCT_1:47;
A4: g in (dom h) /\ X by A1, RELAT_1:61;
then g in dom h by XBOOLE_0:def_4;
then r in rng h by A3, FUNCT_1:def_3;
then A5: r in dom (h ") by FUNCT_1:33;
( g in dom h & g in X ) by A4, XBOOLE_0:def_4;
then r in h .: X by A3, FUNCT_1:def_6;
then r in (dom (h ")) /\ (h .: X) by A5, XBOOLE_0:def_4;
hence r in dom ((h ") | (h .: X)) by RELAT_1:61; ::_thesis: verum
end;
assume r in dom ((h ") | (h .: X)) ; ::_thesis: r in dom ((h | X) ")
then r in (dom (h ")) /\ (h .: X) by RELAT_1:61;
then r in h .: X by XBOOLE_0:def_4;
then consider t being set such that
A6: t in dom h and
A7: t in X and
A8: h . t = r by FUNCT_1:def_6;
t in (dom h) /\ X by A6, A7, XBOOLE_0:def_4;
then A9: t in dom (h | X) by RELAT_1:61;
(h | X) . t = r by A7, A8, FUNCT_1:49;
then r in rng hX by A9, FUNCT_1:def_3;
hence r in dom ((h | X) ") by FUNCT_1:33; ::_thesis: verum
end;
then A10: dom (hX ") = dom ((h ") | (h .: X)) by TARSKI:1;
now__::_thesis:_for_r_being_set_holds_
(_not_r_in_dom_((h_|_X)_")_or_not_((h_|_X)_")_._r_<>_((h_")_|_(h_.:_X))_._r_)
given r being set such that A11: r in dom ((h | X) ") and
A12: ((h | X) ") . r <> ((h ") | (h .: X)) . r ; ::_thesis: contradiction
r in (dom (h ")) /\ (h .: X) by A10, A11, RELAT_1:61;
then r in h .: X by XBOOLE_0:def_4;
then consider t being set such that
t in dom h and
t in X and
A13: h . t = r by FUNCT_1:def_6;
r in rng hX by A11, FUNCT_1:33;
then consider g being set such that
A14: g in dom (h | X) and
A15: (h | X) . g = r by FUNCT_1:def_3;
A16: h . g = r by A14, A15, FUNCT_1:47;
g in (dom h) /\ X by A14, RELAT_1:61;
then A17: g in dom h by XBOOLE_0:def_4;
(hX ") . r <> (h ") . r by A10, A11, A12, FUNCT_1:47;
then g <> (h ") . (h . t) by A14, A15, A13, FUNCT_1:34;
hence contradiction by A13, A17, A16, FUNCT_1:34; ::_thesis: verum
end;
hence (h | X) " = (h ") | (h .: X) by A10, FUNCT_1:2; ::_thesis: verum
end;
theorem Th18: :: RFUNCT_2:18
for W being non empty set
for h being PartFunc of W,REAL st rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) holds
h is V8()
proof
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL st rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) holds
h is V8()
let h be PartFunc of W,REAL; ::_thesis: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) implies h is V8() )
assume A1: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) ) ; ::_thesis: h is V8()
assume h is V8() ; ::_thesis: contradiction
then consider x1, x2 being set such that
A2: ( x1 in dom h & x2 in dom h ) and
A3: h . x1 <> h . x2 by FUNCT_1:def_10;
( h . x1 in rng h & h . x2 in rng h ) by A2, FUNCT_1:def_3;
hence contradiction by A1, A3, SEQ_4:12; ::_thesis: verum
end;
theorem :: RFUNCT_2:19
for Y being set
for W being non empty set
for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is V8()
proof
let Y be set ; ::_thesis: for W being non empty set
for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is V8()
let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is V8()
let h be PartFunc of W,REAL; ::_thesis: ( h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) implies h | Y is V8() )
rng (h | Y) = h .: Y by RELAT_1:115;
hence ( h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) implies h | Y is V8() ) by Th18; ::_thesis: verum
end;
definition
let h be PartFunc of REAL,REAL;
redefine attr h is increasing means :Def1: :: RFUNCT_2:def 1
for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2;
compatibility
( h is increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2 )
proof
thus ( h is increasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2 ) by VALUED_0:def_13; ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2 ) implies h is increasing )
assume A1: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2 ; ::_thesis: h is increasing
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for b1 being set holds
( not e1 in dom h or not b1 in dom h or b1 <= e1 or not h . b1 <= h . e1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom h or not e2 in dom h or e2 <= e1 or not h . e2 <= h . e1 )
thus ( not e1 in dom h or not e2 in dom h or e2 <= e1 or not h . e2 <= h . e1 ) by A1; ::_thesis: verum
end;
redefine attr h is decreasing means :Def2: :: RFUNCT_2:def 2
for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1;
compatibility
( h is decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1 )
proof
thus ( h is decreasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 > h . r2 ) by VALUED_0:def_14; ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1 ) implies h is decreasing )
assume A2: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 > h . r2 ; ::_thesis: h is decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for b1 being set holds
( not e1 in dom h or not b1 in dom h or b1 <= e1 or not h . e1 <= h . b1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom h or not e2 in dom h or e2 <= e1 or not h . e1 <= h . e2 )
thus ( not e1 in dom h or not e2 in dom h or e2 <= e1 or not h . e1 <= h . e2 ) by A2; ::_thesis: verum
end;
redefine attr h is non-decreasing means :Def3: :: RFUNCT_2:def 3
for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2;
compatibility
( h is non-decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 )
proof
thus ( h is non-decreasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 ) by VALUED_0:def_15; ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 ) implies h is non-decreasing )
assume A3: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 ; ::_thesis: h is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for b1 being set holds
( not e1 in dom h or not b1 in dom h or not e1 <= b1 or h . e1 <= h . b1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom h or not e2 in dom h or not e1 <= e2 or h . e1 <= h . e2 )
assume A4: ( e1 in dom h & e2 in dom h ) ; ::_thesis: ( not e1 <= e2 or h . e1 <= h . e2 )
assume e1 <= e2 ; ::_thesis: h . e1 <= h . e2
then ( e1 < e2 or e1 = e2 ) by XXREAL_0:1;
hence h . e1 <= h . e2 by A3, A4; ::_thesis: verum
end;
redefine attr h is non-increasing means :Def4: :: RFUNCT_2:def 4
for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1;
compatibility
( h is non-increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1 )
proof
thus ( h is non-increasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 >= h . r2 ) by VALUED_0:def_16; ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1 ) implies h is non-increasing )
assume A5: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 >= h . r2 ; ::_thesis: h is non-increasing
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for b1 being set holds
( not e1 in dom h or not b1 in dom h or not e1 <= b1 or h . b1 <= h . e1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom h or not e2 in dom h or not e1 <= e2 or h . e2 <= h . e1 )
assume A6: ( e1 in dom h & e2 in dom h ) ; ::_thesis: ( not e1 <= e2 or h . e2 <= h . e1 )
assume e1 <= e2 ; ::_thesis: h . e2 <= h . e1
then ( e1 < e2 or e1 = e2 ) by XXREAL_0:1;
hence h . e2 <= h . e1 by A5, A6; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines increasing RFUNCT_2:def_1_:_
for h being PartFunc of REAL,REAL holds
( h is increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2 );
:: deftheorem Def2 defines decreasing RFUNCT_2:def_2_:_
for h being PartFunc of REAL,REAL holds
( h is decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1 );
:: deftheorem Def3 defines non-decreasing RFUNCT_2:def_3_:_
for h being PartFunc of REAL,REAL holds
( h is non-decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 );
:: deftheorem Def4 defines non-increasing RFUNCT_2:def_4_:_
for h being PartFunc of REAL,REAL holds
( h is non-increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1 );
theorem Th20: :: RFUNCT_2:20
for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 )
proof
let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds
( h | Y is increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 )
let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 )
thus ( h | Y is increasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 > h . r1 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 ) implies h | Y is increasing )
proof
assume A1: h | Y is increasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 > h . r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 > h . r1 )
assume that
A2: r1 in Y /\ (dom h) and
A3: r2 in Y /\ (dom h) and
A4: r1 < r2 ; ::_thesis: h . r2 > h . r1
A5: r2 in dom (h | Y) by A3, RELAT_1:61;
then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47;
A7: r1 in dom (h | Y) by A2, RELAT_1:61;
then (h | Y) . r1 = h . r1 by FUNCT_1:47;
hence h . r2 > h . r1 by A1, A4, A7, A5, A6, Def1; ::_thesis: verum
end;
assume A8: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 > h . r1 ; ::_thesis: h | Y is increasing
let r1 be Element of REAL ; :: according to RFUNCT_2:def_1 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r1 < (h | Y) . r2
let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 < (h | Y) . r2 )
assume that
A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and
A10: r1 < r2 ; ::_thesis: (h | Y) . r1 < (h | Y) . r2
A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61;
hence (h | Y) . r1 < (h | Y) . r2 by A8, A10, A11; ::_thesis: verum
end;
theorem Th21: :: RFUNCT_2:21
for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 )
proof
let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds
( h | Y is decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 )
let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 )
thus ( h | Y is decreasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 ) implies h | Y is decreasing )
proof
assume A1: h | Y is decreasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 < h . r1 )
assume that
A2: r1 in Y /\ (dom h) and
A3: r2 in Y /\ (dom h) and
A4: r1 < r2 ; ::_thesis: h . r2 < h . r1
A5: r2 in dom (h | Y) by A3, RELAT_1:61;
then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47;
A7: r1 in dom (h | Y) by A2, RELAT_1:61;
then (h | Y) . r1 = h . r1 by FUNCT_1:47;
hence h . r2 < h . r1 by A1, A4, A7, A5, A6, Def2; ::_thesis: verum
end;
assume A8: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 ; ::_thesis: h | Y is decreasing
let r1 be Element of REAL ; :: according to RFUNCT_2:def_2 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r2 < (h | Y) . r1
let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r2 < (h | Y) . r1 )
assume that
A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and
A10: r1 < r2 ; ::_thesis: (h | Y) . r2 < (h | Y) . r1
A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61;
hence (h | Y) . r2 < (h | Y) . r1 by A8, A10, A11; ::_thesis: verum
end;
theorem Th22: :: RFUNCT_2:22
for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 )
proof
let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds
( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 )
let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 )
thus ( h | Y is non-decreasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 ) implies h | Y is non-decreasing )
proof
assume A1: h | Y is non-decreasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r1 <= h . r2 )
assume that
A2: r1 in Y /\ (dom h) and
A3: r2 in Y /\ (dom h) and
A4: r1 < r2 ; ::_thesis: h . r1 <= h . r2
A5: r2 in dom (h | Y) by A3, RELAT_1:61;
then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47;
A7: r1 in dom (h | Y) by A2, RELAT_1:61;
then (h | Y) . r1 = h . r1 by FUNCT_1:47;
hence h . r1 <= h . r2 by A1, A4, A7, A5, A6, Def3; ::_thesis: verum
end;
assume A8: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 ; ::_thesis: h | Y is non-decreasing
let r1 be Element of REAL ; :: according to RFUNCT_2:def_3 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r1 <= (h | Y) . r2
let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 <= (h | Y) . r2 )
assume that
A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and
A10: r1 < r2 ; ::_thesis: (h | Y) . r1 <= (h | Y) . r2
A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61;
hence (h | Y) . r1 <= (h | Y) . r2 by A8, A10, A11; ::_thesis: verum
end;
theorem Th23: :: RFUNCT_2:23
for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1 )
proof
let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds
( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1 )
let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1 )
thus ( h | Y is non-increasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1 ) implies h | Y is non-increasing )
proof
assume A1: h | Y is non-increasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 <= h . r1 )
assume that
A2: r1 in Y /\ (dom h) and
A3: r2 in Y /\ (dom h) and
A4: r1 < r2 ; ::_thesis: h . r2 <= h . r1
A5: r2 in dom (h | Y) by A3, RELAT_1:61;
then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47;
A7: r1 in dom (h | Y) by A2, RELAT_1:61;
then (h | Y) . r1 = h . r1 by FUNCT_1:47;
hence h . r2 <= h . r1 by A1, A4, A7, A5, A6, Def4; ::_thesis: verum
end;
assume A8: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1 ; ::_thesis: h | Y is non-increasing
let r1 be Element of REAL ; :: according to RFUNCT_2:def_4 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r2 <= (h | Y) . r1
let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r2 <= (h | Y) . r1 )
assume that
A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and
A10: r1 < r2 ; ::_thesis: (h | Y) . r2 <= (h | Y) . r1
A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61;
hence (h | Y) . r2 <= (h | Y) . r1 by A8, A10, A11; ::_thesis: verum
end;
definition
let h be PartFunc of REAL,REAL;
attrh is monotone means :Def5: :: RFUNCT_2:def 5
( h is non-decreasing or h is non-increasing );
end;
:: deftheorem Def5 defines monotone RFUNCT_2:def_5_:_
for h being PartFunc of REAL,REAL holds
( h is monotone iff ( h is non-decreasing or h is non-increasing ) );
registration
cluster Function-like non-decreasing -> monotone for Element of bool [:REAL,REAL:];
coherence
for b1 being PartFunc of REAL,REAL st b1 is non-decreasing holds
b1 is monotone by Def5;
cluster Function-like non-increasing -> monotone for Element of bool [:REAL,REAL:];
coherence
for b1 being PartFunc of REAL,REAL st b1 is non-increasing holds
b1 is monotone by Def5;
cluster Function-like non monotone -> non non-decreasing non non-increasing for Element of bool [:REAL,REAL:];
coherence
for b1 being PartFunc of REAL,REAL st not b1 is monotone holds
( not b1 is non-decreasing & not b1 is non-increasing ) ;
end;
theorem Th24: :: RFUNCT_2:24
for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 )
proof
let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds
( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 )
let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 )
thus ( h | Y is non-decreasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 ) implies h | Y is non-decreasing )
proof
assume A1: h | Y is non-decreasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 implies h . r1 <= h . r2 )
assume that
A2: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) and
A3: r1 <= r2 ; ::_thesis: h . r1 <= h . r2
now__::_thesis:_h_._r1_<=_h_._r2
percases ( r1 < r2 or r1 = r2 ) by A3, XXREAL_0:1;
suppose r1 < r2 ; ::_thesis: h . r1 <= h . r2
hence h . r1 <= h . r2 by A1, A2, Th22; ::_thesis: verum
end;
suppose r1 = r2 ; ::_thesis: h . r1 <= h . r2
hence h . r1 <= h . r2 ; ::_thesis: verum
end;
end;
end;
hence h . r1 <= h . r2 ; ::_thesis: verum
end;
assume A4: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 ; ::_thesis: h | Y is non-decreasing
let r1 be Element of REAL ; :: according to RFUNCT_2:def_3 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r1 <= (h | Y) . r2
let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 <= (h | Y) . r2 )
assume that
A5: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and
A6: r1 < r2 ; ::_thesis: (h | Y) . r1 <= (h | Y) . r2
A7: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A5, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A5, RELAT_1:61;
hence (h | Y) . r1 <= (h | Y) . r2 by A4, A6, A7; ::_thesis: verum
end;
theorem Th25: :: RFUNCT_2:25
for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r2 <= h . r1 )
proof
let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds
( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r2 <= h . r1 )
let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r2 <= h . r1 )
thus ( h | Y is non-increasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r2 <= h . r1 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r2 <= h . r1 ) implies h | Y is non-increasing )
proof
assume A1: h | Y is non-increasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r2 <= h . r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 implies h . r2 <= h . r1 )
assume that
A2: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) and
A3: r1 <= r2 ; ::_thesis: h . r2 <= h . r1
now__::_thesis:_h_._r2_<=_h_._r1
percases ( r1 < r2 or r1 = r2 ) by A3, XXREAL_0:1;
suppose r1 < r2 ; ::_thesis: h . r2 <= h . r1
hence h . r2 <= h . r1 by A1, A2, Th23; ::_thesis: verum
end;
suppose r1 = r2 ; ::_thesis: h . r2 <= h . r1
hence h . r2 <= h . r1 ; ::_thesis: verum
end;
end;
end;
hence h . r2 <= h . r1 ; ::_thesis: verum
end;
assume A4: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r2 <= h . r1 ; ::_thesis: h | Y is non-increasing
let r1 be Element of REAL ; :: according to RFUNCT_2:def_4 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r2 <= (h | Y) . r1
let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r2 <= (h | Y) . r1 )
assume that
A5: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and
A6: r1 < r2 ; ::_thesis: (h | Y) . r2 <= (h | Y) . r1
A7: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A5, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A5, RELAT_1:61;
hence (h | Y) . r2 <= (h | Y) . r1 by A4, A6, A7; ::_thesis: verum
end;
registration
cluster Function-like non-decreasing non-increasing -> V8() for Element of bool [:REAL,REAL:];
coherence
for b1 being PartFunc of REAL,REAL st b1 is non-decreasing & b1 is non-increasing holds
b1 is V8()
proof
let h be PartFunc of REAL,REAL; ::_thesis: ( h is non-decreasing & h is non-increasing implies h is V8() )
assume A1: ( h is non-decreasing & h is non-increasing ) ; ::_thesis: h is V8()
let r1, r2 be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not r1 in dom h or not r2 in dom h or h . r1 = h . r2 )
assume A2: ( r1 in dom h & r2 in dom h ) ; ::_thesis: h . r1 = h . r2
then reconsider r1 = r1, r2 = r2 as Real ;
( r1 < r2 or r1 = r2 or r2 < r1 ) by XXREAL_0:1;
then ( h . r1 <= h . r2 & h . r2 <= h . r1 ) by A1, A2, Def3, Def4;
hence h . r1 = h . r2 by XXREAL_0:1; ::_thesis: verum
end;
end;
registration
cluster Function-like V8() -> non-decreasing non-increasing for Element of bool [:REAL,REAL:];
coherence
for b1 being PartFunc of REAL,REAL st b1 is V8() holds
( b1 is non-increasing & b1 is non-decreasing )
proof
let h be PartFunc of REAL,REAL; ::_thesis: ( h is V8() implies ( h is non-increasing & h is non-decreasing ) )
assume A1: h is V8() ; ::_thesis: ( h is non-increasing & h is non-decreasing )
thus h is non-increasing ::_thesis: h is non-decreasing
proof
let r1 be Element of REAL ; :: according to RFUNCT_2:def_4 ::_thesis: for r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1
let r2 be Element of REAL ; ::_thesis: ( r1 in dom h & r2 in dom h & r1 < r2 implies h . r2 <= h . r1 )
assume ( r1 in dom h & r2 in dom h ) ; ::_thesis: ( not r1 < r2 or h . r2 <= h . r1 )
hence ( not r1 < r2 or h . r2 <= h . r1 ) by A1, FUNCT_1:def_10; ::_thesis: verum
end;
let r1 be Element of REAL ; :: according to RFUNCT_2:def_3 ::_thesis: for r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2
let r2 be Element of REAL ; ::_thesis: ( r1 in dom h & r2 in dom h & r1 < r2 implies h . r1 <= h . r2 )
assume ( r1 in dom h & r2 in dom h ) ; ::_thesis: ( not r1 < r2 or h . r1 <= h . r2 )
hence ( not r1 < r2 or h . r1 <= h . r2 ) by A1, FUNCT_1:def_10; ::_thesis: verum
end;
end;
registration
cluster Relation-like REAL -defined REAL -valued Function-like trivial complex-valued ext-real-valued real-valued for Element of bool [:REAL,REAL:];
existence
ex b1 being PartFunc of REAL,REAL st b1 is trivial
proof
reconsider f = {} as PartFunc of REAL,REAL by RELSET_1:12;
take f ; ::_thesis: f is trivial
thus f is trivial ; ::_thesis: verum
end;
end;
registration
let h be increasing PartFunc of REAL,REAL;
let X be set ;
clusterh | X -> increasing for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is increasing
proof
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_dom_(h_|_X)_&_r2_in_dom_(h_|_X)_&_r1_<_r2_holds_
(h_|_X)_._r1_<_(h_|_X)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | X) & r2 in dom (h | X) & r1 < r2 implies (h | X) . r1 < (h | X) . r2 )
assume A1: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; ::_thesis: ( r1 < r2 implies (h | X) . r1 < (h | X) . r2 )
then A2: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by FUNCT_1:47;
assume A3: r1 < r2 ; ::_thesis: (h | X) . r1 < (h | X) . r2
( r1 in dom h & r2 in dom h ) by A1, RELAT_1:57;
hence (h | X) . r1 < (h | X) . r2 by A2, A3, Def1; ::_thesis: verum
end;
hence for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is increasing by Def1; ::_thesis: verum
end;
end;
registration
let h be decreasing PartFunc of REAL,REAL;
let X be set ;
clusterh | X -> decreasing for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is decreasing
proof
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_dom_(h_|_X)_&_r2_in_dom_(h_|_X)_&_r1_<_r2_holds_
(h_|_X)_._r1_>_(h_|_X)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | X) & r2 in dom (h | X) & r1 < r2 implies (h | X) . r1 > (h | X) . r2 )
assume A1: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; ::_thesis: ( r1 < r2 implies (h | X) . r1 > (h | X) . r2 )
then A2: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by FUNCT_1:47;
assume A3: r1 < r2 ; ::_thesis: (h | X) . r1 > (h | X) . r2
( r1 in dom h & r2 in dom h ) by A1, RELAT_1:57;
hence (h | X) . r1 > (h | X) . r2 by A2, A3, Def2; ::_thesis: verum
end;
hence for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is decreasing by Def2; ::_thesis: verum
end;
end;
registration
let h be non-decreasing PartFunc of REAL,REAL;
let X be set ;
clusterh | X -> non-decreasing for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is non-decreasing
proof
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_dom_(h_|_X)_&_r2_in_dom_(h_|_X)_&_r1_<_r2_holds_
(h_|_X)_._r1_<=_(h_|_X)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | X) & r2 in dom (h | X) & r1 < r2 implies (h | X) . r1 <= (h | X) . r2 )
assume A1: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; ::_thesis: ( r1 < r2 implies (h | X) . r1 <= (h | X) . r2 )
then A2: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by FUNCT_1:47;
assume A3: r1 < r2 ; ::_thesis: (h | X) . r1 <= (h | X) . r2
( r1 in dom h & r2 in dom h ) by A1, RELAT_1:57;
hence (h | X) . r1 <= (h | X) . r2 by A2, A3, Def3; ::_thesis: verum
end;
hence for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is non-decreasing by Def3; ::_thesis: verum
end;
end;
theorem :: RFUNCT_2:26
for Y being set
for h being PartFunc of REAL,REAL st Y misses dom h holds
( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
proof
let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st Y misses dom h holds
( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
let h be PartFunc of REAL,REAL; ::_thesis: ( Y misses dom h implies ( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone ) )
assume A1: Y /\ (dom h) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
then for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 ;
hence h | Y is increasing by Th20; ::_thesis: ( h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 by A1;
hence h | Y is decreasing by Th21; ::_thesis: ( h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 by A1;
hence h | Y is non-decreasing by Th22; ::_thesis: ( h | Y is non-increasing & h | Y is monotone )
A2: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1 by A1;
hence h | Y is non-increasing by Th23; ::_thesis: h | Y is monotone
thus h | Y is monotone by A2, Th23; ::_thesis: verum
end;
theorem :: RFUNCT_2:27
for Y, X being set
for h being PartFunc of REAL,REAL st h | Y is non-decreasing & h | X is non-increasing holds
h | (Y /\ X) is V8()
proof
let Y, X be set ; ::_thesis: for h being PartFunc of REAL,REAL st h | Y is non-decreasing & h | X is non-increasing holds
h | (Y /\ X) is V8()
let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-decreasing & h | X is non-increasing implies h | (Y /\ X) is V8() )
assume A1: ( h | Y is non-decreasing & h | X is non-increasing ) ; ::_thesis: h | (Y /\ X) is V8()
now__::_thesis:_h_|_(Y_/\_X)_is_V8()
percases ( (Y /\ X) /\ (dom h) = {} or (Y /\ X) /\ (dom h) <> {} ) ;
suppose (Y /\ X) /\ (dom h) = {} ; ::_thesis: h | (Y /\ X) is V8()
then Y /\ X misses dom h by XBOOLE_0:def_7;
hence h | (Y /\ X) is V8() by PARTFUN2:39; ::_thesis: verum
end;
supposeA2: (Y /\ X) /\ (dom h) <> {} ; ::_thesis: h | (Y /\ X) is V8()
set x = the Element of (Y /\ X) /\ (dom h);
the Element of (Y /\ X) /\ (dom h) in dom h by A2, XBOOLE_0:def_4;
then reconsider x = the Element of (Y /\ X) /\ (dom h) as Real ;
now__::_thesis:_ex_r1_being_Element_of_REAL_st_
for_p_being_Element_of_REAL_st_p_in_(Y_/\_X)_/\_(dom_h)_holds_
h_._p_=_r1
take r1 = h . x; ::_thesis: for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = r1
now__::_thesis:_for_p_being_Element_of_REAL_st_p_in_(Y_/\_X)_/\_(dom_h)_holds_
h_._p_=_r1
let p be Element of REAL ; ::_thesis: ( p in (Y /\ X) /\ (dom h) implies h . p = r1 )
assume A3: p in (Y /\ X) /\ (dom h) ; ::_thesis: h . p = r1
then A4: p in Y /\ X by XBOOLE_0:def_4;
A5: p in dom h by A3, XBOOLE_0:def_4;
p in X by A4, XBOOLE_0:def_4;
then A6: p in X /\ (dom h) by A5, XBOOLE_0:def_4;
A7: x in dom h by A2, XBOOLE_0:def_4;
A8: x in Y /\ X by A2, XBOOLE_0:def_4;
then x in Y by XBOOLE_0:def_4;
then A9: x in Y /\ (dom h) by A7, XBOOLE_0:def_4;
x in X by A8, XBOOLE_0:def_4;
then A10: x in X /\ (dom h) by A7, XBOOLE_0:def_4;
p in Y by A4, XBOOLE_0:def_4;
then A11: p in Y /\ (dom h) by A5, XBOOLE_0:def_4;
now__::_thesis:_h_._p_=_h_._x
percases ( x <= p or p <= x ) ;
suppose x <= p ; ::_thesis: h . p = h . x
then ( h . x <= h . p & h . p <= h . x ) by A1, A11, A6, A9, A10, Th24, Th25;
hence h . p = h . x by XXREAL_0:1; ::_thesis: verum
end;
suppose p <= x ; ::_thesis: h . p = h . x
then ( h . p <= h . x & h . x <= h . p ) by A1, A11, A6, A9, A10, Th24, Th25;
hence h . p = h . x by XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence h . p = r1 ; ::_thesis: verum
end;
hence for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = r1 ; ::_thesis: verum
end;
hence h | (Y /\ X) is V8() by PARTFUN2:57; ::_thesis: verum
end;
end;
end;
hence h | (Y /\ X) is V8() ; ::_thesis: verum
end;
theorem :: RFUNCT_2:28
for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is increasing holds
h | X is increasing
proof
let X, Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is increasing holds
h | X is increasing
let h be PartFunc of REAL,REAL; ::_thesis: ( X c= Y & h | Y is increasing implies h | X is increasing )
assume that
A1: X c= Y and
A2: h | Y is increasing ; ::_thesis: h | X is increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_X_/\_(dom_h)_&_r2_in_X_/\_(dom_h)_&_r1_<_r2_holds_
h_._r1_<_h_._r2
A3: X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26;
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 < h . r2 )
assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; ::_thesis: h . r1 < h . r2
hence h . r1 < h . r2 by A2, A3, Th20; ::_thesis: verum
end;
hence h | X is increasing by Th20; ::_thesis: verum
end;
theorem :: RFUNCT_2:29
for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is decreasing holds
h | X is decreasing
proof
let X, Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is decreasing holds
h | X is decreasing
let h be PartFunc of REAL,REAL; ::_thesis: ( X c= Y & h | Y is decreasing implies h | X is decreasing )
assume that
A1: X c= Y and
A2: h | Y is decreasing ; ::_thesis: h | X is decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_X_/\_(dom_h)_&_r2_in_X_/\_(dom_h)_&_r1_<_r2_holds_
h_._r1_>_h_._r2
A3: X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26;
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 > h . r2 )
assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; ::_thesis: h . r1 > h . r2
hence h . r1 > h . r2 by A2, A3, Th21; ::_thesis: verum
end;
hence h | X is decreasing by Th21; ::_thesis: verum
end;
theorem :: RFUNCT_2:30
for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-decreasing holds
h | X is non-decreasing
proof
let X, Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-decreasing holds
h | X is non-decreasing
let h be PartFunc of REAL,REAL; ::_thesis: ( X c= Y & h | Y is non-decreasing implies h | X is non-decreasing )
assume that
A1: X c= Y and
A2: h | Y is non-decreasing ; ::_thesis: h | X is non-decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_X_/\_(dom_h)_&_r2_in_X_/\_(dom_h)_&_r1_<_r2_holds_
h_._r1_<=_h_._r2
A3: X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26;
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 <= h . r2 )
assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; ::_thesis: h . r1 <= h . r2
hence h . r1 <= h . r2 by A2, A3, Th22; ::_thesis: verum
end;
hence h | X is non-decreasing by Th22; ::_thesis: verum
end;
theorem :: RFUNCT_2:31
for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-increasing holds
h | X is non-increasing
proof
let X, Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-increasing holds
h | X is non-increasing
let h be PartFunc of REAL,REAL; ::_thesis: ( X c= Y & h | Y is non-increasing implies h | X is non-increasing )
assume that
A1: X c= Y and
A2: h | Y is non-increasing ; ::_thesis: h | X is non-increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_X_/\_(dom_h)_&_r2_in_X_/\_(dom_h)_&_r1_<_r2_holds_
h_._r1_>=_h_._r2
A3: X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26;
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 >= h . r2 )
assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; ::_thesis: h . r1 >= h . r2
hence h . r1 >= h . r2 by A2, A3, Th23; ::_thesis: verum
end;
hence h | X is non-increasing by Th23; ::_thesis: verum
end;
theorem Th32: :: RFUNCT_2:32
for Y being set
for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) )
proof
let Y be set ; ::_thesis: for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) )
let r be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL holds
( ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) )
let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) )
thus ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) ::_thesis: ( ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) )
proof
assume that
A1: h | Y is increasing and
A2: 0 < r ; ::_thesis: (r (#) h) | Y is increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_
(r_(#)_h)_._r1_<_(r_(#)_h)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 < (r (#) h) . r2 )
assume that
A3: r1 in Y /\ (dom (r (#) h)) and
A4: r2 in Y /\ (dom (r (#) h)) and
A5: r1 < r2 ; ::_thesis: (r (#) h) . r1 < (r (#) h) . r2
A6: r2 in Y by A4, XBOOLE_0:def_4;
A7: r2 in dom (r (#) h) by A4, XBOOLE_0:def_4;
then r2 in dom h by VALUED_1:def_5;
then A8: r2 in Y /\ (dom h) by A6, XBOOLE_0:def_4;
A9: r1 in Y by A3, XBOOLE_0:def_4;
A10: r1 in dom (r (#) h) by A3, XBOOLE_0:def_4;
then r1 in dom h by VALUED_1:def_5;
then r1 in Y /\ (dom h) by A9, XBOOLE_0:def_4;
then h . r1 < h . r2 by A1, A5, A8, Th20;
then r * (h . r1) < r * (h . r2) by A2, XREAL_1:68;
then (r (#) h) . r1 < r * (h . r2) by A10, VALUED_1:def_5;
hence (r (#) h) . r1 < (r (#) h) . r2 by A7, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is increasing by Th20; ::_thesis: verum
end;
thus ( r = 0 implies (r (#) h) | Y is V8() ) ::_thesis: ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing )
proof
assume A11: r = 0 ; ::_thesis: (r (#) h) | Y is V8()
now__::_thesis:_for_r1_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_holds_
(r_(#)_h)_._r1_=_0
let r1 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) implies (r (#) h) . r1 = 0 )
assume r1 in Y /\ (dom (r (#) h)) ; ::_thesis: (r (#) h) . r1 = 0
then A12: r1 in dom (r (#) h) by XBOOLE_0:def_4;
r * (h . r1) = 0 by A11;
hence (r (#) h) . r1 = 0 by A12, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is V8() by PARTFUN2:57; ::_thesis: verum
end;
assume that
A13: h | Y is increasing and
A14: r < 0 ; ::_thesis: (r (#) h) | Y is decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_
(r_(#)_h)_._r2_<_(r_(#)_h)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 < (r (#) h) . r1 )
assume that
A15: r1 in Y /\ (dom (r (#) h)) and
A16: r2 in Y /\ (dom (r (#) h)) and
A17: r1 < r2 ; ::_thesis: (r (#) h) . r2 < (r (#) h) . r1
A18: r2 in Y by A16, XBOOLE_0:def_4;
A19: r2 in dom (r (#) h) by A16, XBOOLE_0:def_4;
then r2 in dom h by VALUED_1:def_5;
then A20: r2 in Y /\ (dom h) by A18, XBOOLE_0:def_4;
A21: r1 in Y by A15, XBOOLE_0:def_4;
A22: r1 in dom (r (#) h) by A15, XBOOLE_0:def_4;
then r1 in dom h by VALUED_1:def_5;
then r1 in Y /\ (dom h) by A21, XBOOLE_0:def_4;
then h . r1 < h . r2 by A13, A17, A20, Th20;
then r * (h . r2) < r * (h . r1) by A14, XREAL_1:69;
then (r (#) h) . r2 < r * (h . r1) by A19, VALUED_1:def_5;
hence (r (#) h) . r2 < (r (#) h) . r1 by A22, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is decreasing by Th21; ::_thesis: verum
end;
theorem :: RFUNCT_2:33
for Y being set
for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) )
proof
let Y be set ; ::_thesis: for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) )
let r be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL holds
( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) )
let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) )
thus ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) ::_thesis: ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing )
proof
assume that
A1: h | Y is decreasing and
A2: 0 < r ; ::_thesis: (r (#) h) | Y is decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_
(r_(#)_h)_._r2_<_(r_(#)_h)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 < (r (#) h) . r1 )
assume that
A3: r1 in Y /\ (dom (r (#) h)) and
A4: r2 in Y /\ (dom (r (#) h)) and
A5: r1 < r2 ; ::_thesis: (r (#) h) . r2 < (r (#) h) . r1
A6: r2 in Y by A4, XBOOLE_0:def_4;
A7: r2 in dom (r (#) h) by A4, XBOOLE_0:def_4;
then r2 in dom h by VALUED_1:def_5;
then A8: r2 in Y /\ (dom h) by A6, XBOOLE_0:def_4;
A9: r1 in Y by A3, XBOOLE_0:def_4;
A10: r1 in dom (r (#) h) by A3, XBOOLE_0:def_4;
then r1 in dom h by VALUED_1:def_5;
then r1 in Y /\ (dom h) by A9, XBOOLE_0:def_4;
then h . r2 < h . r1 by A1, A5, A8, Th21;
then r * (h . r2) < r * (h . r1) by A2, XREAL_1:68;
then (r (#) h) . r2 < r * (h . r1) by A7, VALUED_1:def_5;
hence (r (#) h) . r2 < (r (#) h) . r1 by A10, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is decreasing by Th21; ::_thesis: verum
end;
assume that
A11: h | Y is decreasing and
A12: r < 0 ; ::_thesis: (r (#) h) | Y is increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_
(r_(#)_h)_._r1_<_(r_(#)_h)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 < (r (#) h) . r2 )
assume that
A13: r1 in Y /\ (dom (r (#) h)) and
A14: r2 in Y /\ (dom (r (#) h)) and
A15: r1 < r2 ; ::_thesis: (r (#) h) . r1 < (r (#) h) . r2
A16: r2 in Y by A14, XBOOLE_0:def_4;
A17: r2 in dom (r (#) h) by A14, XBOOLE_0:def_4;
then r2 in dom h by VALUED_1:def_5;
then A18: r2 in Y /\ (dom h) by A16, XBOOLE_0:def_4;
A19: r1 in Y by A13, XBOOLE_0:def_4;
A20: r1 in dom (r (#) h) by A13, XBOOLE_0:def_4;
then r1 in dom h by VALUED_1:def_5;
then r1 in Y /\ (dom h) by A19, XBOOLE_0:def_4;
then h . r2 < h . r1 by A11, A15, A18, Th21;
then r * (h . r1) < r * (h . r2) by A12, XREAL_1:69;
then (r (#) h) . r1 < r * (h . r2) by A20, VALUED_1:def_5;
hence (r (#) h) . r1 < (r (#) h) . r2 by A17, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is increasing by Th20; ::_thesis: verum
end;
theorem Th34: :: RFUNCT_2:34
for Y being set
for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) )
proof
let Y be set ; ::_thesis: for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) )
let r be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL holds
( ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) )
let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) )
thus ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) ::_thesis: ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing )
proof
assume that
A1: h | Y is non-decreasing and
A2: 0 <= r ; ::_thesis: (r (#) h) | Y is non-decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_
(r_(#)_h)_._r1_<=_(r_(#)_h)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 <= (r (#) h) . r2 )
assume that
A3: r1 in Y /\ (dom (r (#) h)) and
A4: r2 in Y /\ (dom (r (#) h)) and
A5: r1 < r2 ; ::_thesis: (r (#) h) . r1 <= (r (#) h) . r2
A6: r2 in Y by A4, XBOOLE_0:def_4;
A7: r2 in dom (r (#) h) by A4, XBOOLE_0:def_4;
then r2 in dom h by VALUED_1:def_5;
then A8: r2 in Y /\ (dom h) by A6, XBOOLE_0:def_4;
A9: r1 in Y by A3, XBOOLE_0:def_4;
A10: r1 in dom (r (#) h) by A3, XBOOLE_0:def_4;
then r1 in dom h by VALUED_1:def_5;
then r1 in Y /\ (dom h) by A9, XBOOLE_0:def_4;
then h . r1 <= h . r2 by A1, A5, A8, Th22;
then r * (h . r1) <= (h . r2) * r by A2, XREAL_1:64;
then (r (#) h) . r1 <= r * (h . r2) by A10, VALUED_1:def_5;
hence (r (#) h) . r1 <= (r (#) h) . r2 by A7, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is non-decreasing by Th22; ::_thesis: verum
end;
assume that
A11: h | Y is non-decreasing and
A12: r <= 0 ; ::_thesis: (r (#) h) | Y is non-increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_
(r_(#)_h)_._r2_<=_(r_(#)_h)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 <= (r (#) h) . r1 )
assume that
A13: r1 in Y /\ (dom (r (#) h)) and
A14: r2 in Y /\ (dom (r (#) h)) and
A15: r1 < r2 ; ::_thesis: (r (#) h) . r2 <= (r (#) h) . r1
A16: r2 in Y by A14, XBOOLE_0:def_4;
A17: r2 in dom (r (#) h) by A14, XBOOLE_0:def_4;
then r2 in dom h by VALUED_1:def_5;
then A18: r2 in Y /\ (dom h) by A16, XBOOLE_0:def_4;
A19: r1 in Y by A13, XBOOLE_0:def_4;
A20: r1 in dom (r (#) h) by A13, XBOOLE_0:def_4;
then r1 in dom h by VALUED_1:def_5;
then r1 in Y /\ (dom h) by A19, XBOOLE_0:def_4;
then h . r1 <= h . r2 by A11, A15, A18, Th22;
then r * (h . r2) <= r * (h . r1) by A12, XREAL_1:65;
then (r (#) h) . r2 <= r * (h . r1) by A17, VALUED_1:def_5;
hence (r (#) h) . r2 <= (r (#) h) . r1 by A20, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is non-increasing by Th23; ::_thesis: verum
end;
theorem :: RFUNCT_2:35
for Y being set
for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) )
proof
let Y be set ; ::_thesis: for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) )
let r be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL holds
( ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) )
let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) )
thus ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) ::_thesis: ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing )
proof
assume that
A1: h | Y is non-increasing and
A2: 0 <= r ; ::_thesis: (r (#) h) | Y is non-increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_
(r_(#)_h)_._r2_<=_(r_(#)_h)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 <= (r (#) h) . r1 )
assume that
A3: r1 in Y /\ (dom (r (#) h)) and
A4: r2 in Y /\ (dom (r (#) h)) and
A5: r1 < r2 ; ::_thesis: (r (#) h) . r2 <= (r (#) h) . r1
A6: r2 in Y by A4, XBOOLE_0:def_4;
A7: r2 in dom (r (#) h) by A4, XBOOLE_0:def_4;
then r2 in dom h by VALUED_1:def_5;
then A8: r2 in Y /\ (dom h) by A6, XBOOLE_0:def_4;
A9: r1 in Y by A3, XBOOLE_0:def_4;
A10: r1 in dom (r (#) h) by A3, XBOOLE_0:def_4;
then r1 in dom h by VALUED_1:def_5;
then r1 in Y /\ (dom h) by A9, XBOOLE_0:def_4;
then h . r2 <= h . r1 by A1, A5, A8, Th23;
then r * (h . r2) <= (h . r1) * r by A2, XREAL_1:64;
then (r (#) h) . r2 <= r * (h . r1) by A7, VALUED_1:def_5;
hence (r (#) h) . r2 <= (r (#) h) . r1 by A10, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is non-increasing by Th23; ::_thesis: verum
end;
assume that
A11: h | Y is non-increasing and
A12: r <= 0 ; ::_thesis: (r (#) h) | Y is non-decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_
(r_(#)_h)_._r1_<=_(r_(#)_h)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 <= (r (#) h) . r2 )
assume that
A13: r1 in Y /\ (dom (r (#) h)) and
A14: r2 in Y /\ (dom (r (#) h)) and
A15: r1 < r2 ; ::_thesis: (r (#) h) . r1 <= (r (#) h) . r2
A16: r2 in Y by A14, XBOOLE_0:def_4;
A17: r2 in dom (r (#) h) by A14, XBOOLE_0:def_4;
then r2 in dom h by VALUED_1:def_5;
then A18: r2 in Y /\ (dom h) by A16, XBOOLE_0:def_4;
A19: r1 in Y by A13, XBOOLE_0:def_4;
A20: r1 in dom (r (#) h) by A13, XBOOLE_0:def_4;
then r1 in dom h by VALUED_1:def_5;
then r1 in Y /\ (dom h) by A19, XBOOLE_0:def_4;
then h . r2 <= h . r1 by A11, A15, A18, Th23;
then r * (h . r1) <= r * (h . r2) by A12, XREAL_1:65;
then (r (#) h) . r1 <= r * (h . r2) by A20, VALUED_1:def_5;
hence (r (#) h) . r1 <= (r (#) h) . r2 by A17, VALUED_1:def_5; ::_thesis: verum
end;
hence (r (#) h) | Y is non-decreasing by Th22; ::_thesis: verum
end;
theorem Th36: :: RFUNCT_2:36
for X, Y being set
for r being Element of REAL
for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds
( r in X /\ (dom h1) & r in Y /\ (dom h2) )
proof
let X, Y be set ; ::_thesis: for r being Element of REAL
for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds
( r in X /\ (dom h1) & r in Y /\ (dom h2) )
let r be Element of REAL ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds
( r in X /\ (dom h1) & r in Y /\ (dom h2) )
let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( r in (X /\ Y) /\ (dom (h1 + h2)) implies ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) )
assume A1: r in (X /\ Y) /\ (dom (h1 + h2)) ; ::_thesis: ( r in X /\ (dom h1) & r in Y /\ (dom h2) )
then r in dom (h1 + h2) by XBOOLE_0:def_4;
then r in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then A2: ( r in dom h1 & r in dom h2 ) by XBOOLE_0:def_4;
r in X /\ Y by A1, XBOOLE_0:def_4;
then ( r in X & r in Y ) by XBOOLE_0:def_4;
hence ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: RFUNCT_2:37
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) )
proof
let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) )
let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( ( h1 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) )
thus ( h1 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) ::_thesis: ( ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) )
proof
assume that
A1: h1 | X is increasing and
A2: h2 | Y is increasing ; ::_thesis: (h1 + h2) | (X /\ Y) is increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r1_<_(h1_+_h2)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 < (h1 + h2) . r2 )
assume that
A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r1 < r2 ; ::_thesis: (h1 + h2) . r1 < (h1 + h2) . r2
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A3, A4, Th36;
then A6: h2 . r1 < h2 . r2 by A2, A5, Th20;
A7: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4;
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A3, A4, Th36;
then h1 . r1 < h1 . r2 by A1, A5, Th20;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A6, XREAL_1:8;
then A8: (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A7, VALUED_1:def_1;
r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by A8, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is increasing by Th20; ::_thesis: verum
end;
thus ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) ::_thesis: ( ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) )
proof
assume that
A9: h1 | X is decreasing and
A10: h2 | Y is decreasing ; ::_thesis: (h1 + h2) | (X /\ Y) is decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r2_<_(h1_+_h2)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 )
assume that
A11: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A12: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A13: r1 < r2 ; ::_thesis: (h1 + h2) . r2 < (h1 + h2) . r1
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A11, A12, Th36;
then A14: h2 . r2 < h2 . r1 by A10, A13, Th21;
A15: r2 in dom (h1 + h2) by A12, XBOOLE_0:def_4;
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A11, A12, Th36;
then h1 . r2 < h1 . r1 by A9, A13, Th21;
then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A14, XREAL_1:8;
then A16: (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A15, VALUED_1:def_1;
r1 in dom (h1 + h2) by A11, XBOOLE_0:def_4;
hence (h1 + h2) . r2 < (h1 + h2) . r1 by A16, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is decreasing by Th21; ::_thesis: verum
end;
thus ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) ::_thesis: ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing )
proof
assume that
A17: h1 | X is non-decreasing and
A18: h2 | Y is non-decreasing ; ::_thesis: (h1 + h2) | (X /\ Y) is non-decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r1_<=_(h1_+_h2)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 <= (h1 + h2) . r2 )
assume that
A19: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A20: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A21: r1 < r2 ; ::_thesis: (h1 + h2) . r1 <= (h1 + h2) . r2
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A19, A20, Th36;
then A22: h2 . r1 <= h2 . r2 by A18, A21, Th22;
A23: r1 in dom (h1 + h2) by A19, XBOOLE_0:def_4;
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A19, A20, Th36;
then h1 . r1 <= h1 . r2 by A17, A21, Th22;
then (h1 . r1) + (h2 . r1) <= (h1 . r2) + (h2 . r2) by A22, XREAL_1:7;
then A24: (h1 + h2) . r1 <= (h1 . r2) + (h2 . r2) by A23, VALUED_1:def_1;
r2 in dom (h1 + h2) by A20, XBOOLE_0:def_4;
hence (h1 + h2) . r1 <= (h1 + h2) . r2 by A24, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is non-decreasing by Th22; ::_thesis: verum
end;
assume that
A25: h1 | X is non-increasing and
A26: h2 | Y is non-increasing ; ::_thesis: (h1 + h2) | (X /\ Y) is non-increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r2_<=_(h1_+_h2)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 <= (h1 + h2) . r1 )
assume that
A27: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A28: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A29: r1 < r2 ; ::_thesis: (h1 + h2) . r2 <= (h1 + h2) . r1
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A27, A28, Th36;
then A30: h2 . r2 <= h2 . r1 by A26, A29, Th23;
A31: r2 in dom (h1 + h2) by A28, XBOOLE_0:def_4;
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A27, A28, Th36;
then h1 . r2 <= h1 . r1 by A25, A29, Th23;
then (h1 . r2) + (h2 . r2) <= (h1 . r1) + (h2 . r1) by A30, XREAL_1:7;
then A32: (h1 + h2) . r2 <= (h1 . r1) + (h2 . r1) by A31, VALUED_1:def_1;
r1 in dom (h1 + h2) by A27, XBOOLE_0:def_4;
hence (h1 + h2) . r2 <= (h1 + h2) . r1 by A32, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is non-increasing by Th23; ::_thesis: verum
end;
theorem :: RFUNCT_2:38
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )
proof
let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )
let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )
thus ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) ::_thesis: ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing )
proof
assume that
A1: h1 | X is increasing and
A2: h2 | Y is V8() ; ::_thesis: (h1 + h2) | (X /\ Y) is increasing
consider r being Element of REAL such that
A3: for p being Element of REAL st p in Y /\ (dom h2) holds
h2 . p = r by A2, PARTFUN2:57;
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r1_<_(h1_+_h2)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 < (h1 + h2) . r2 )
assume that
A4: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A6: r1 < r2 ; ::_thesis: (h1 + h2) . r1 < (h1 + h2) . r2
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A4, A5, Th36;
then h1 . r1 < h1 . r2 by A1, A6, Th20;
then A7: (h1 . r1) + r < (h1 . r2) + r by XREAL_1:6;
r1 in Y /\ (dom h2) by A4, Th36;
then A8: (h1 . r1) + (h2 . r1) < (h1 . r2) + r by A3, A7;
A9: r1 in dom (h1 + h2) by A4, XBOOLE_0:def_4;
r2 in Y /\ (dom h2) by A5, Th36;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A3, A8;
then A10: (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A9, VALUED_1:def_1;
r2 in dom (h1 + h2) by A5, XBOOLE_0:def_4;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by A10, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is increasing by Th20; ::_thesis: verum
end;
assume that
A11: h1 | X is decreasing and
A12: h2 | Y is V8() ; ::_thesis: (h1 + h2) | (X /\ Y) is decreasing
consider r being Element of REAL such that
A13: for p being Element of REAL st p in Y /\ (dom h2) holds
h2 . p = r by A12, PARTFUN2:57;
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r2_<_(h1_+_h2)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 )
assume that
A14: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A15: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A16: r1 < r2 ; ::_thesis: (h1 + h2) . r2 < (h1 + h2) . r1
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A14, A15, Th36;
then h1 . r2 < h1 . r1 by A11, A16, Th21;
then A17: (h1 . r2) + r < (h1 . r1) + r by XREAL_1:6;
r2 in Y /\ (dom h2) by A15, Th36;
then A18: (h1 . r2) + (h2 . r2) < (h1 . r1) + r by A13, A17;
A19: r2 in dom (h1 + h2) by A15, XBOOLE_0:def_4;
r1 in Y /\ (dom h2) by A14, Th36;
then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A13, A18;
then A20: (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A19, VALUED_1:def_1;
r1 in dom (h1 + h2) by A14, XBOOLE_0:def_4;
hence (h1 + h2) . r2 < (h1 + h2) . r1 by A20, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is decreasing by Th21; ::_thesis: verum
end;
theorem :: RFUNCT_2:39
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is increasing & h2 | Y is non-decreasing holds
(h1 + h2) | (X /\ Y) is increasing
proof
let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is increasing & h2 | Y is non-decreasing holds
(h1 + h2) | (X /\ Y) is increasing
let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( h1 | X is increasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is increasing )
assume that
A1: h1 | X is increasing and
A2: h2 | Y is non-decreasing ; ::_thesis: (h1 + h2) | (X /\ Y) is increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r1_<_(h1_+_h2)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 < (h1 + h2) . r2 )
assume that
A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r1 < r2 ; ::_thesis: (h1 + h2) . r1 < (h1 + h2) . r2
A6: r2 in X /\ Y by A4, XBOOLE_0:def_4;
then A7: r2 in Y by XBOOLE_0:def_4;
A8: r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4;
then A9: r2 in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then r2 in dom h2 by XBOOLE_0:def_4;
then A10: r2 in Y /\ (dom h2) by A7, XBOOLE_0:def_4;
A11: r1 in X /\ Y by A3, XBOOLE_0:def_4;
then A12: r1 in Y by XBOOLE_0:def_4;
A13: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4;
then A14: r1 in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then r1 in dom h2 by XBOOLE_0:def_4;
then r1 in Y /\ (dom h2) by A12, XBOOLE_0:def_4;
then A15: h2 . r1 <= h2 . r2 by A2, A5, A10, Th22;
A16: r2 in X by A6, XBOOLE_0:def_4;
A17: r1 in X by A11, XBOOLE_0:def_4;
r2 in dom h1 by A9, XBOOLE_0:def_4;
then A18: r2 in X /\ (dom h1) by A16, XBOOLE_0:def_4;
r1 in dom h1 by A14, XBOOLE_0:def_4;
then r1 in X /\ (dom h1) by A17, XBOOLE_0:def_4;
then h1 . r1 < h1 . r2 by A1, A5, A18, Th20;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A15, XREAL_1:8;
then (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A13, VALUED_1:def_1;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by A8, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is increasing by Th20; ::_thesis: verum
end;
theorem :: RFUNCT_2:40
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-increasing & h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-increasing
proof
let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-increasing & h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-increasing
let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( h1 | X is non-increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is non-increasing )
assume that
A1: h1 | X is non-increasing and
A2: h2 | Y is V8() ; ::_thesis: (h1 + h2) | (X /\ Y) is non-increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r2_<=_(h1_+_h2)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 <= (h1 + h2) . r1 )
assume that
A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r1 < r2 ; ::_thesis: (h1 + h2) . r2 <= (h1 + h2) . r1
A6: r2 in X /\ Y by A4, XBOOLE_0:def_4;
then A7: r2 in X by XBOOLE_0:def_4;
A8: r2 in Y by A6, XBOOLE_0:def_4;
A9: r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4;
then A10: r2 in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then r2 in dom h2 by XBOOLE_0:def_4;
then A11: r2 in Y /\ (dom h2) by A8, XBOOLE_0:def_4;
r2 in dom h1 by A10, XBOOLE_0:def_4;
then A12: r2 in X /\ (dom h1) by A7, XBOOLE_0:def_4;
A13: r1 in X /\ Y by A3, XBOOLE_0:def_4;
then A14: r1 in X by XBOOLE_0:def_4;
A15: r1 in Y by A13, XBOOLE_0:def_4;
A16: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4;
then A17: r1 in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then r1 in dom h2 by XBOOLE_0:def_4;
then r1 in Y /\ (dom h2) by A15, XBOOLE_0:def_4;
then A18: h2 . r2 = h2 . r1 by A2, A11, PARTFUN2:58;
r1 in dom h1 by A17, XBOOLE_0:def_4;
then r1 in X /\ (dom h1) by A14, XBOOLE_0:def_4;
then h1 . r2 <= h1 . r1 by A1, A5, A12, Th23;
then (h1 . r2) + (h2 . r2) <= (h1 . r1) + (h2 . r1) by A18, XREAL_1:6;
then (h1 + h2) . r2 <= (h1 . r1) + (h2 . r1) by A9, VALUED_1:def_1;
hence (h1 + h2) . r2 <= (h1 + h2) . r1 by A16, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is non-increasing by Th23; ::_thesis: verum
end;
theorem :: RFUNCT_2:41
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is decreasing & h2 | Y is non-increasing holds
(h1 + h2) | (X /\ Y) is decreasing
proof
let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is decreasing & h2 | Y is non-increasing holds
(h1 + h2) | (X /\ Y) is decreasing
let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( h1 | X is decreasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is decreasing )
assume that
A1: h1 | X is decreasing and
A2: h2 | Y is non-increasing ; ::_thesis: (h1 + h2) | (X /\ Y) is decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r2_<_(h1_+_h2)_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 )
assume that
A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r1 < r2 ; ::_thesis: (h1 + h2) . r2 < (h1 + h2) . r1
A6: r2 in X /\ Y by A4, XBOOLE_0:def_4;
then A7: r2 in Y by XBOOLE_0:def_4;
A8: r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4;
then A9: r2 in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then r2 in dom h2 by XBOOLE_0:def_4;
then A10: r2 in Y /\ (dom h2) by A7, XBOOLE_0:def_4;
A11: r1 in X /\ Y by A3, XBOOLE_0:def_4;
then A12: r1 in Y by XBOOLE_0:def_4;
A13: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4;
then A14: r1 in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then r1 in dom h2 by XBOOLE_0:def_4;
then r1 in Y /\ (dom h2) by A12, XBOOLE_0:def_4;
then A15: h2 . r2 <= h2 . r1 by A2, A5, A10, Th23;
A16: r2 in X by A6, XBOOLE_0:def_4;
A17: r1 in X by A11, XBOOLE_0:def_4;
r2 in dom h1 by A9, XBOOLE_0:def_4;
then A18: r2 in X /\ (dom h1) by A16, XBOOLE_0:def_4;
r1 in dom h1 by A14, XBOOLE_0:def_4;
then r1 in X /\ (dom h1) by A17, XBOOLE_0:def_4;
then h1 . r2 < h1 . r1 by A1, A5, A18, Th21;
then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A15, XREAL_1:8;
then (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A8, VALUED_1:def_1;
hence (h1 + h2) . r2 < (h1 + h2) . r1 by A13, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is decreasing by Th21; ::_thesis: verum
end;
theorem :: RFUNCT_2:42
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-decreasing & h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-decreasing
proof
let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-decreasing & h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-decreasing
let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( h1 | X is non-decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is non-decreasing )
assume that
A1: h1 | X is non-decreasing and
A2: h2 | Y is V8() ; ::_thesis: (h1 + h2) | (X /\ Y) is non-decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_
(h1_+_h2)_._r1_<=_(h1_+_h2)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 <= (h1 + h2) . r2 )
assume that
A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r1 < r2 ; ::_thesis: (h1 + h2) . r1 <= (h1 + h2) . r2
A6: r2 in X /\ Y by A4, XBOOLE_0:def_4;
then A7: r2 in X by XBOOLE_0:def_4;
A8: r2 in Y by A6, XBOOLE_0:def_4;
A9: r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4;
then A10: r2 in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then r2 in dom h2 by XBOOLE_0:def_4;
then A11: r2 in Y /\ (dom h2) by A8, XBOOLE_0:def_4;
r2 in dom h1 by A10, XBOOLE_0:def_4;
then A12: r2 in X /\ (dom h1) by A7, XBOOLE_0:def_4;
A13: r1 in X /\ Y by A3, XBOOLE_0:def_4;
then A14: r1 in X by XBOOLE_0:def_4;
A15: r1 in Y by A13, XBOOLE_0:def_4;
A16: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4;
then A17: r1 in (dom h1) /\ (dom h2) by VALUED_1:def_1;
then r1 in dom h2 by XBOOLE_0:def_4;
then r1 in Y /\ (dom h2) by A15, XBOOLE_0:def_4;
then A18: h2 . r2 = h2 . r1 by A2, A11, PARTFUN2:58;
r1 in dom h1 by A17, XBOOLE_0:def_4;
then r1 in X /\ (dom h1) by A14, XBOOLE_0:def_4;
then h1 . r1 <= h1 . r2 by A1, A5, A12, Th22;
then (h1 . r1) + (h2 . r1) <= (h1 . r2) + (h2 . r2) by A18, XREAL_1:6;
then (h1 + h2) . r1 <= (h1 . r2) + (h2 . r2) by A16, VALUED_1:def_1;
hence (h1 + h2) . r1 <= (h1 + h2) . r2 by A9, VALUED_1:def_1; ::_thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is non-decreasing by Th22; ::_thesis: verum
end;
theorem :: RFUNCT_2:43
for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-increasing
proof
let x be set ; ::_thesis: for h being PartFunc of REAL,REAL holds h | {x} is non-increasing
let h be PartFunc of REAL,REAL; ::_thesis: h | {x} is non-increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_{x}_/\_(dom_h)_&_r2_in_{x}_/\_(dom_h)_&_r1_<_r2_holds_
h_._r1_>=_h_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r1 >= h . r2 )
assume that
A1: r1 in {x} /\ (dom h) and
A2: r2 in {x} /\ (dom h) and
r1 < r2 ; ::_thesis: h . r1 >= h . r2
r1 in {x} by A1, XBOOLE_0:def_4;
then A3: r1 = x by TARSKI:def_1;
r2 in {x} by A2, XBOOLE_0:def_4;
hence h . r1 >= h . r2 by A3, TARSKI:def_1; ::_thesis: verum
end;
hence h | {x} is non-increasing by Th23; ::_thesis: verum
end;
theorem :: RFUNCT_2:44
for x being set
for h being PartFunc of REAL,REAL holds h | {x} is decreasing
proof
let x be set ; ::_thesis: for h being PartFunc of REAL,REAL holds h | {x} is decreasing
let h be PartFunc of REAL,REAL; ::_thesis: h | {x} is decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_{x}_/\_(dom_h)_&_r2_in_{x}_/\_(dom_h)_&_r1_<_r2_holds_
h_._r1_>_h_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r1 > h . r2 )
assume that
A1: r1 in {x} /\ (dom h) and
A2: r2 in {x} /\ (dom h) and
A3: r1 < r2 ; ::_thesis: h . r1 > h . r2
r1 in {x} by A1, XBOOLE_0:def_4;
then A4: r1 = x by TARSKI:def_1;
r2 in {x} by A2, XBOOLE_0:def_4;
hence h . r1 > h . r2 by A3, A4, TARSKI:def_1; ::_thesis: verum
end;
hence h | {x} is decreasing by Th21; ::_thesis: verum
end;
theorem :: RFUNCT_2:45
for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-decreasing
proof
let x be set ; ::_thesis: for h being PartFunc of REAL,REAL holds h | {x} is non-decreasing
let h be PartFunc of REAL,REAL; ::_thesis: h | {x} is non-decreasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_{x}_/\_(dom_h)_&_r2_in_{x}_/\_(dom_h)_&_r1_<_r2_holds_
h_._r1_<=_h_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r1 <= h . r2 )
assume that
A1: r1 in {x} /\ (dom h) and
A2: r2 in {x} /\ (dom h) and
r1 < r2 ; ::_thesis: h . r1 <= h . r2
r1 in {x} by A1, XBOOLE_0:def_4;
then A3: r1 = x by TARSKI:def_1;
r2 in {x} by A2, XBOOLE_0:def_4;
hence h . r1 <= h . r2 by A3, TARSKI:def_1; ::_thesis: verum
end;
hence h | {x} is non-decreasing by Th22; ::_thesis: verum
end;
theorem :: RFUNCT_2:46
for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-increasing
proof
let x be set ; ::_thesis: for h being PartFunc of REAL,REAL holds h | {x} is non-increasing
let h be PartFunc of REAL,REAL; ::_thesis: h | {x} is non-increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_{x}_/\_(dom_h)_&_r2_in_{x}_/\_(dom_h)_&_r1_<_r2_holds_
h_._r2_<=_h_._r1
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r2 <= h . r1 )
assume that
A1: r1 in {x} /\ (dom h) and
A2: r2 in {x} /\ (dom h) and
r1 < r2 ; ::_thesis: h . r2 <= h . r1
r1 in {x} by A1, XBOOLE_0:def_4;
then A3: r1 = x by TARSKI:def_1;
r2 in {x} by A2, XBOOLE_0:def_4;
hence h . r2 <= h . r1 by A3, TARSKI:def_1; ::_thesis: verum
end;
hence h | {x} is non-increasing by Th23; ::_thesis: verum
end;
theorem :: RFUNCT_2:47
for R being Subset of REAL holds (id R) | R is increasing
proof
let R be Subset of REAL; ::_thesis: (id R) | R is increasing
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_R_/\_(dom_(id_R))_&_r2_in_R_/\_(dom_(id_R))_&_r1_<_r2_holds_
(id_R)_._r1_<_(id_R)_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in R /\ (dom (id R)) & r2 in R /\ (dom (id R)) & r1 < r2 implies (id R) . r1 < (id R) . r2 )
assume that
A1: r1 in R /\ (dom (id R)) and
A2: r2 in R /\ (dom (id R)) and
A3: r1 < r2 ; ::_thesis: (id R) . r1 < (id R) . r2
r1 in R by A1, XBOOLE_0:def_4;
then A4: (id R) . r1 = r1 by FUNCT_1:18;
r2 in R by A2, XBOOLE_0:def_4;
hence (id R) . r1 < (id R) . r2 by A3, A4, FUNCT_1:18; ::_thesis: verum
end;
hence (id R) | R is increasing by Th20; ::_thesis: verum
end;
theorem :: RFUNCT_2:48
for X being set
for h being PartFunc of REAL,REAL st h | X is increasing holds
(- h) | X is decreasing
proof
let X be set ; ::_thesis: for h being PartFunc of REAL,REAL st h | X is increasing holds
(- h) | X is decreasing
let h be PartFunc of REAL,REAL; ::_thesis: ( h | X is increasing implies (- h) | X is decreasing )
assume h | X is increasing ; ::_thesis: (- h) | X is decreasing
then ((- 1) (#) h) | X is decreasing by Th32;
hence (- h) | X is decreasing ; ::_thesis: verum
end;
theorem :: RFUNCT_2:49
for X being set
for h being PartFunc of REAL,REAL st h | X is non-decreasing holds
(- h) | X is non-increasing
proof
let X be set ; ::_thesis: for h being PartFunc of REAL,REAL st h | X is non-decreasing holds
(- h) | X is non-increasing
let h be PartFunc of REAL,REAL; ::_thesis: ( h | X is non-decreasing implies (- h) | X is non-increasing )
assume h | X is non-decreasing ; ::_thesis: (- h) | X is non-increasing
then ((- 1) (#) h) | X is non-increasing by Th34;
hence (- h) | X is non-increasing ; ::_thesis: verum
end;
theorem :: RFUNCT_2:50
for p, g being Element of REAL
for h being PartFunc of REAL,REAL st ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) holds
h | [.p,g.] is one-to-one
proof
let p, g be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL st ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) holds
h | [.p,g.] is one-to-one
let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) implies h | [.p,g.] is one-to-one )
assume A1: ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) ; ::_thesis: h | [.p,g.] is one-to-one
now__::_thesis:_h_|_[.p,g.]_is_one-to-one
percases ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) by A1;
supposeA2: h | [.p,g.] is increasing ; ::_thesis: h | [.p,g.] is one-to-one
now__::_thesis:_for_p1,_p2_being_Element_of_REAL_st_p1_in_dom_(h_|_[.p,g.])_&_p2_in_dom_(h_|_[.p,g.])_&_(h_|_[.p,g.])_._p1_=_(h_|_[.p,g.])_._p2_holds_
p1_=_p2
let p1, p2 be Element of REAL ; ::_thesis: ( p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 implies p1 = p2 )
assume that
A3: p1 in dom (h | [.p,g.]) and
A4: p2 in dom (h | [.p,g.]) and
A5: (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 ; ::_thesis: p1 = p2
A6: ( p1 in [.p,g.] /\ (dom h) & p2 in [.p,g.] /\ (dom h) ) by A3, A4, RELAT_1:61;
A7: h . p1 = (h | [.p,g.]) . p2 by A3, A5, FUNCT_1:47
.= h . p2 by A4, FUNCT_1:47 ;
thus p1 = p2 ::_thesis: verum
proof
assume A8: p1 <> p2 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( p1 < p2 or p2 < p1 ) by A8, XXREAL_0:1;
suppose p1 < p2 ; ::_thesis: contradiction
hence contradiction by A2, A7, A6, Th20; ::_thesis: verum
end;
suppose p2 < p1 ; ::_thesis: contradiction
hence contradiction by A2, A7, A6, Th20; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
hence h | [.p,g.] is one-to-one by PARTFUN1:8; ::_thesis: verum
end;
supposeA9: h | [.p,g.] is decreasing ; ::_thesis: h | [.p,g.] is one-to-one
now__::_thesis:_for_p1,_p2_being_Element_of_REAL_st_p1_in_dom_(h_|_[.p,g.])_&_p2_in_dom_(h_|_[.p,g.])_&_(h_|_[.p,g.])_._p1_=_(h_|_[.p,g.])_._p2_holds_
p1_=_p2
let p1, p2 be Element of REAL ; ::_thesis: ( p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 implies p1 = p2 )
assume that
A10: p1 in dom (h | [.p,g.]) and
A11: p2 in dom (h | [.p,g.]) and
A12: (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 ; ::_thesis: p1 = p2
A13: ( p1 in [.p,g.] /\ (dom h) & p2 in [.p,g.] /\ (dom h) ) by A10, A11, RELAT_1:61;
A14: h . p1 = (h | [.p,g.]) . p2 by A10, A12, FUNCT_1:47
.= h . p2 by A11, FUNCT_1:47 ;
thus p1 = p2 ::_thesis: verum
proof
assume A15: p1 <> p2 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( p1 < p2 or p2 < p1 ) by A15, XXREAL_0:1;
suppose p1 < p2 ; ::_thesis: contradiction
hence contradiction by A9, A14, A13, Th21; ::_thesis: verum
end;
suppose p2 < p1 ; ::_thesis: contradiction
hence contradiction by A9, A14, A13, Th21; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
hence h | [.p,g.] is one-to-one by PARTFUN1:8; ::_thesis: verum
end;
end;
end;
hence h | [.p,g.] is one-to-one ; ::_thesis: verum
end;
theorem :: RFUNCT_2:51
for p, g being Element of REAL
for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is increasing holds
((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing
proof
let p, g be Element of REAL ; ::_thesis: for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is increasing holds
((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing
let h be one-to-one PartFunc of REAL,REAL; ::_thesis: ( h | [.p,g.] is increasing implies ((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing )
assume that
A1: h | [.p,g.] is increasing and
A2: not ((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing ; ::_thesis: contradiction
consider y1, y2 being Real such that
A3: y1 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) and
A4: y2 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) and
A5: y1 < y2 and
A6: ((h | [.p,g.]) ") . y1 >= ((h | [.p,g.]) ") . y2 by A2, Th20;
y1 in h .: [.p,g.] by A3, XBOOLE_0:def_4;
then A7: y1 in rng (h | [.p,g.]) by RELAT_1:115;
y2 in h .: [.p,g.] by A4, XBOOLE_0:def_4;
then A8: y2 in rng (h | [.p,g.]) by RELAT_1:115;
A9: (h | [.p,g.]) | [.p,g.] is increasing by A1;
now__::_thesis:_contradiction
percases ( ((h | [.p,g.]) ") . y1 = ((h | [.p,g.]) ") . y2 or ((h | [.p,g.]) ") . y1 <> ((h | [.p,g.]) ") . y2 ) ;
suppose ((h | [.p,g.]) ") . y1 = ((h | [.p,g.]) ") . y2 ; ::_thesis: contradiction
then y1 = (h | [.p,g.]) . (((h | [.p,g.]) ") . y2) by A7, FUNCT_1:35
.= y2 by A8, FUNCT_1:35 ;
hence contradiction by A5; ::_thesis: verum
end;
supposeA10: ((h | [.p,g.]) ") . y1 <> ((h | [.p,g.]) ") . y2 ; ::_thesis: contradiction
A11: dom (h | [.p,g.]) = dom ((h | [.p,g.]) | [.p,g.]) by RELAT_1:72
.= [.p,g.] /\ (dom (h | [.p,g.])) by RELAT_1:61 ;
A12: ( ((h | [.p,g.]) ") . y2 in dom (h | [.p,g.]) & ((h | [.p,g.]) ") . y1 in dom (h | [.p,g.]) ) by A7, A8, PARTFUN2:60;
((h | [.p,g.]) ") . y2 < ((h | [.p,g.]) ") . y1 by A6, A10, XXREAL_0:1;
then (h | [.p,g.]) . (((h | [.p,g.]) ") . y2) < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A9, A12, A11, Th20;
then y2 < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A8, FUNCT_1:35;
hence contradiction by A5, A7, FUNCT_1:35; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: RFUNCT_2:52
for p, g being Element of REAL
for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is decreasing holds
((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing
proof
let p, g be Element of REAL ; ::_thesis: for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is decreasing holds
((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing
let h be one-to-one PartFunc of REAL,REAL; ::_thesis: ( h | [.p,g.] is decreasing implies ((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing )
assume that
A1: h | [.p,g.] is decreasing and
A2: not ((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing ; ::_thesis: contradiction
consider y1, y2 being Real such that
A3: y1 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) and
A4: y2 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) and
A5: y1 < y2 and
A6: ((h | [.p,g.]) ") . y2 >= ((h | [.p,g.]) ") . y1 by A2, Th21;
y1 in h .: [.p,g.] by A3, XBOOLE_0:def_4;
then A7: y1 in rng (h | [.p,g.]) by RELAT_1:115;
y2 in h .: [.p,g.] by A4, XBOOLE_0:def_4;
then A8: y2 in rng (h | [.p,g.]) by RELAT_1:115;
A9: (h | [.p,g.]) | [.p,g.] is decreasing by A1;
now__::_thesis:_contradiction
percases ( ((h | [.p,g.]) ") . y1 = ((h | [.p,g.]) ") . y2 or ((h | [.p,g.]) ") . y1 <> ((h | [.p,g.]) ") . y2 ) ;
suppose ((h | [.p,g.]) ") . y1 = ((h | [.p,g.]) ") . y2 ; ::_thesis: contradiction
then y1 = (h | [.p,g.]) . (((h | [.p,g.]) ") . y2) by A7, FUNCT_1:35
.= y2 by A8, FUNCT_1:35 ;
hence contradiction by A5; ::_thesis: verum
end;
supposeA10: ((h | [.p,g.]) ") . y1 <> ((h | [.p,g.]) ") . y2 ; ::_thesis: contradiction
A11: dom (h | [.p,g.]) = dom ((h | [.p,g.]) | [.p,g.]) by RELAT_1:72
.= [.p,g.] /\ (dom (h | [.p,g.])) by RELAT_1:61 ;
A12: ( ((h | [.p,g.]) ") . y2 in dom (h | [.p,g.]) & ((h | [.p,g.]) ") . y1 in dom (h | [.p,g.]) ) by A7, A8, PARTFUN2:60;
((h | [.p,g.]) ") . y2 > ((h | [.p,g.]) ") . y1 by A6, A10, XXREAL_0:1;
then (h | [.p,g.]) . (((h | [.p,g.]) ") . y2) < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A9, A12, A11, Th21;
then y2 < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A8, FUNCT_1:35;
hence contradiction by A5, A7, FUNCT_1:35; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;