let k be Nat; :: thesis: for seq being ExtREAL_sequence st seq is non-increasing holds
( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )
let seq be ExtREAL_sequence; :: thesis: ( seq is non-increasing implies ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq is non-increasing ; :: thesis: ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )
now :: thesis: for n, m being Nat st m <= n holds
(seq ^\ k) . n <= (seq ^\ k) . m
let n, m be Nat; :: thesis: ( m <= n implies (seq ^\ k) . n <= (seq ^\ k) . m )
assume m <= n ; :: thesis: (seq ^\ k) . n <= (seq ^\ k) . m
then k + m <= k + n by XREAL_1:6;
then seq . (k + n) <= seq . (k + m) by A1, Th7;
then (seq ^\ k) . n <= seq . (k + m) by NAT_1:def 3;
hence (seq ^\ k) . n <= (seq ^\ k) . m by NAT_1:def 3; :: thesis: verum
end;
hence seq ^\ k is non-increasing ; :: thesis: inf seq = inf (seq ^\ k)
now :: thesis: for y being ExtReal st y in rng seq holds
inf (rng (seq ^\ k)) <= y
let y be ExtReal; :: thesis: ( y in rng seq implies inf (rng (seq ^\ k)) <= y )
assume y in rng seq ; :: thesis: inf (rng (seq ^\ k)) <= y
then consider n being object such that
A2: n in dom seq and
A3: y = seq . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A2;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;
then A4: inf (seq ^\ k) <= seq . (n + k) by Th23;
n <= n + k by NAT_1:11;
then seq . (n + k) <= seq . n by A1, Th7;
hence inf (rng (seq ^\ k)) <= y by A3, A4, XXREAL_0:2; :: thesis: verum
end;
then inf (rng (seq ^\ k)) is LowerBound of rng seq by XXREAL_2:def 2;
then A5: inf (rng (seq ^\ k)) <= inf (rng seq) by XXREAL_2:def 4;
now :: thesis: for y being ExtReal st y in rng (seq ^\ k) holds
inf (rng seq) <= y
let y be ExtReal; :: thesis: ( y in rng (seq ^\ k) implies inf (rng seq) <= y )
assume y in rng (seq ^\ k) ; :: thesis: inf (rng seq) <= y
then consider n being object such that
A6: n in dom (seq ^\ k) and
A7: y = (seq ^\ k) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A6;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;
then inf seq <= (seq ^\ k) . n by Th23;
hence inf (rng seq) <= y by A7; :: thesis: verum
end;
then inf (rng seq) is LowerBound of rng (seq ^\ k) by XXREAL_2:def 2;
then inf (rng seq) <= inf (rng (seq ^\ k)) by XXREAL_2:def 4;
hence inf seq = inf (seq ^\ k) by A5, XXREAL_0:1; :: thesis: verum