let r, s be Real; for n being Nat
for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len C holds
G . n <= lower_bound (C /. (n + 1))
let n be Nat; for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len C holds
G . n <= lower_bound (C /. (n + 1))
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len C holds
G . n <= lower_bound (C /. (n + 1))
let C be IntervalCover of F; for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len C holds
G . n <= lower_bound (C /. (n + 1))
let G be IntervalCoverPts of C; ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len C implies G . n <= lower_bound (C /. (n + 1)) )
assume that
A1:
( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected )
and
A2:
r <= s
; ( not 1 <= n or not n < len C or G . n <= lower_bound (C /. (n + 1)) )
set w = n -' 1;
assume that
A3:
1 <= n
and
A4:
n < len C
; G . n <= lower_bound (C /. (n + 1))
A5:
n + 1 <= len C
by A4, NAT_1:13;
per cases
( n = 1 or 1 < n )
by A3, XXREAL_0:1;
suppose A6:
n = 1
;
G . n <= lower_bound (C /. (n + 1))
0 + 1
<= n + 1
by XREAL_1:6;
then A7:
not
C /. (n + 1) is
empty
by A1, A2, A5, Def2;
A8:
G . 1
= r
by A1, A2, Def3;
A9:
rng C c= F
by A1, A2, Def2;
1
+ 1
<= len C
by A4, A6, NAT_1:13;
then A10:
2
in dom C
by FINSEQ_3:25;
then
C . 2
in rng C
by FUNCT_1:def 3;
then
C . 2
in F
by A9;
then
C /. 2
in F
by A10, PARTFUN1:def 6;
then
C /. (n + 1) c= the
carrier of
(Closed-Interval-TSpace (r,s))
by A6;
then A11:
C /. (n + 1) c= [.r,s.]
by A2, TOPMETR:18;
then
C /. (n + 1) is
bounded_below
by XXREAL_2:44;
then
lower_bound (C /. (n + 1)) in [.r,s.]
by A7, A11, Th1;
hence
G . n <= lower_bound (C /. (n + 1))
by A6, A8, XXREAL_1:1;
verum end; suppose
1
< n
;
G . n <= lower_bound (C /. (n + 1))then A12:
1
- 1
< n - 1
by XREAL_1:9;
then A13:
n -' 1
= n - 1
by XREAL_0:def 2;
then A14:
0 + 1
<= n -' 1
by A12, NAT_1:13;
len G = (len C) + 1
by A1, A2, Def3;
then A15:
n + 1
< ((len G) - 1) + 1
by A4, XREAL_1:6;
n - 1
< n - 0
by XREAL_1:15;
then
(n -' 1) + 1
< n + 1
by A13, XREAL_1:6;
then
(n -' 1) + 1
< len G
by A15, XXREAL_0:2;
then A16:
G . ((n -' 1) + 1) < upper_bound (C /. (n -' 1))
by A1, A2, A14, Th62;
n + 1
<= len C
by A4, NAT_1:13;
then
upper_bound (C /. (n -' 1)) <= lower_bound (C /. ((n -' 1) + 2))
by A1, A2, A13, A14, Def2;
hence
G . n <= lower_bound (C /. (n + 1))
by A13, A16, XXREAL_0:2;
verum end;