let a, b be Real; :: thesis: for s being Real_Sequence

for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds

S is convergent

let s be Real_Sequence; :: thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds

S is convergent

let S be sequence of (Closed-Interval-MSpace (a,b)); :: thesis: ( S = s & a <= b & s is non-increasing implies S is convergent )

assume that

A1: S = s and

A2: a <= b and

A3: s is non-increasing ; :: thesis: S is convergent

for n being Nat holds s . n > a - 1

hence S is convergent by A1, A2, A3, Th8; :: thesis: verum

for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds

S is convergent

let s be Real_Sequence; :: thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds

S is convergent

let S be sequence of (Closed-Interval-MSpace (a,b)); :: thesis: ( S = s & a <= b & s is non-increasing implies S is convergent )

assume that

A1: S = s and

A2: a <= b and

A3: s is non-increasing ; :: thesis: S is convergent

for n being Nat holds s . n > a - 1

proof

then
s is bounded_below
by SEQ_2:def 4;
let n be Nat; :: thesis: s . n > a - 1

a < a + 1 by XREAL_1:29;

then A4: a - 1 < a by XREAL_1:19;

A5: n in NAT by ORDINAL1:def 12;

dom S = NAT by FUNCT_2:def 1;

then A6: s . n in rng S by A1, FUNCT_1:def 3, A5;

the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A2, TOPMETR:10;

then a <= s . n by A6, XXREAL_1:1;

hence s . n > a - 1 by A4, XXREAL_0:2; :: thesis: verum

end;a < a + 1 by XREAL_1:29;

then A4: a - 1 < a by XREAL_1:19;

A5: n in NAT by ORDINAL1:def 12;

dom S = NAT by FUNCT_2:def 1;

then A6: s . n in rng S by A1, FUNCT_1:def 3, A5;

the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A2, TOPMETR:10;

then a <= s . n by A6, XXREAL_1:1;

hence s . n > a - 1 by A4, XXREAL_0:2; :: thesis: verum

hence S is convergent by A1, A2, A3, Th8; :: thesis: verum