let r, s be real number ; :: thesis: for n being natural number
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 natural number ; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)
and
A2:
F is open
and
A3:
F is connected
and
A4:
r <= s
; :: thesis: ( not 1 <= n or not n < len C or G . n <= lower_bound (C /. (n + 1)) )
set w = n -' 1;
assume that
A5:
1 <= n
and
A6:
n < len C
; :: thesis: G . n <= lower_bound (C /. (n + 1))
A7:
n + 1 <= len C
by A6, NAT_1:13;
per cases
( n = 1 or 1 < n )
by A5, XXREAL_0:1;
suppose A8:
n = 1
;
:: thesis: G . n <= lower_bound (C /. (n + 1))A9:
G . 1
= r
by A1, A2, A3, A4, Def3;
A10:
rng C c= F
by A1, A2, A3, A4, Def2;
0 + 1
<= n + 1
by XREAL_1:8;
then A11:
not
C /. (n + 1) is
empty
by A1, A2, A3, A4, A7, Def2;
1
+ 1
<= len C
by A6, A8, NAT_1:13;
then A12:
2
in dom C
by FINSEQ_3:27;
then
C . 2
in rng C
by FUNCT_1:def 5;
then
C . 2
in F
by A10;
then
C /. 2
in F
by A12, PARTFUN1:def 8;
then
C /. (n + 1) c= the
carrier of
(Closed-Interval-TSpace r,s)
by A8;
then A13:
C /. (n + 1) c= [.r,s.]
by A4, TOPMETR:25;
then
C /. (n + 1) is
bounded_below
by XXREAL_2:44;
then
lower_bound (C /. (n + 1)) in [.r,s.]
by A11, A13, Th1;
hence
G . n <= lower_bound (C /. (n + 1))
by A8, A9, XXREAL_1:1;
:: thesis: verum end; suppose
1
< n
;
:: thesis: G . n <= lower_bound (C /. (n + 1))then A14:
1
- 1
< n - 1
by XREAL_1:11;
then A15:
n -' 1
= n - 1
by XREAL_0:def 2;
then A16:
0 + 1
<= n -' 1
by A14, NAT_1:13;
n - 1
< n - 0
by XREAL_1:17;
then A17:
(n -' 1) + 1
< n + 1
by A15, XREAL_1:8;
len G = (len C) + 1
by A1, A2, A3, A4, Def3;
then
n + 1
< ((len G) - 1) + 1
by A6, XREAL_1:8;
then
(n -' 1) + 1
< len G
by A17, XXREAL_0:2;
then A18:
G . ((n -' 1) + 1) < upper_bound (C /. (n -' 1))
by A1, A2, A3, A4, A16, Th76;
n + 1
<= len C
by A6, NAT_1:13;
then
upper_bound (C /. (n -' 1)) <= lower_bound (C /. ((n -' 1) + 2))
by A1, A2, A3, A4, A15, A16, Def2;
hence
G . n <= lower_bound (C /. (n + 1))
by A15, A18, XXREAL_0:2;
:: thesis: verum end;