let r, s be real number ; :: thesis: for n, m being natural number
for F being Subset-Family of (Closed-Interval-TSpace r,s)
for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m holds
lower_bound (C /. n) <= lower_bound (C /. m)
let n, m be natural number ; :: thesis: for F being Subset-Family of (Closed-Interval-TSpace r,s)
for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m holds
lower_bound (C /. n) <= lower_bound (C /. m)
let F be Subset-Family of (Closed-Interval-TSpace r,s); :: thesis: for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m holds
lower_bound (C /. n) <= lower_bound (C /. m)
let C be IntervalCover of F; :: thesis: ( F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m implies lower_bound (C /. n) <= lower_bound (C /. m) )
assume that
A1:
F is Cover of (Closed-Interval-TSpace r,s)
and
A2:
F is open
and
A3:
F is connected
and
A4:
r <= s
and
A5:
n in dom C
and
A6:
m in dom C
and
A7:
n < m
; :: thesis: lower_bound (C /. n) <= lower_bound (C /. m)
defpred S2[ natural number ] means ( $1 in dom C & n < $1 implies lower_bound (C /. n) <= lower_bound (C /. $1) );
A8:
S2[ 0 ]
;
A9:
for k being natural number st S2[k] holds
S2[k + 1]
proof
let k be
natural number ;
:: thesis: ( S2[k] implies S2[k + 1] )
assume that A10:
S2[
k]
and A11:
k + 1
in dom C
and A12:
n < k + 1
;
:: thesis: lower_bound (C /. n) <= lower_bound (C /. (k + 1))
per cases
( k = 0 or k in dom C )
by A11, TOPREALA:23;
suppose A13:
k in dom C
;
:: thesis: lower_bound (C /. n) <= lower_bound (C /. (k + 1))A14:
n <= k
by A12, NAT_1:13;
A15:
1
<= k
by A13, FINSEQ_3:27;
k + 1
<= len C
by A11, FINSEQ_3:27;
then
lower_bound (C /. k) <= lower_bound (C /. (k + 1))
by A1, A2, A3, A4, A15, Def2;
hence
lower_bound (C /. n) <= lower_bound (C /. (k + 1))
by A10, A13, A14, XXREAL_0:1, XXREAL_0:2;
:: thesis: verum end;
end;
for k being natural number holds S2[k]
from NAT_1:sch 2(A8, A9);
hence
lower_bound (C /. n) <= lower_bound (C /. m)
by A6, A7; :: thesis: verum