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 G holds
[.(G . n),(G . (n + 1)).] c= C . n
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 G holds
[.(G . n),(G . (n + 1)).] c= C . n
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 G holds
[.(G . n),(G . (n + 1)).] c= C . n
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 G holds
[.(G . n),(G . (n + 1)).] c= C . n
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 G implies [.(G . n),(G . (n + 1)).] c= C . n )
set L = Closed-Interval-TSpace r,s;
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:
1 <= n
and
A6:
n < len G
; :: thesis: [.(G . n),(G . (n + 1)).] c= C . n
A7:
n + 1 <= len G
by A6, NAT_1:13;
A8:
n in dom G
by A5, A6, FINSEQ_3:27;
0 + 1 <= n + 1
by XREAL_1:8;
then A9:
n + 1 in dom G
by A7, FINSEQ_3:27;
A10:
len G = (len C) + 1
by A1, A2, A3, A4, Def3;
then A11:
n <= len C
by A6, NAT_1:13;
then A12:
C /. n = C . n
by A5, FINSEQ_4:24;
n in dom C
by A5, A11, FINSEQ_3:27;
then A13:
C . n in rng C
by FUNCT_1:def 5;
rng C c= F
by A1, A2, A3, A4, Def2;
then
C /. n in F
by A12, A13;
then
C /. n is connected Subset of (Closed-Interval-TSpace r,s)
by A3, Def1;
then A14:
C /. n is connected
by Th56;
A15:
not C /. n is empty
by A1, A2, A3, A4, A5, A11, Def2;
A16:
n + 0 < n + 1
by XREAL_1:8;
per cases
( r = s or r < s )
by A4, XXREAL_0:1;
suppose
r = s
;
:: thesis: [.(G . n),(G . (n + 1)).] c= C . nthen
C = <*[.r,r.]*>
by A1, A2, A3, Th64;
then A17:
len C = 1
by FINSEQ_1:57;
then
G = <*r,s*>
by A1, A2, A3, A4, Th75;
then A18:
(
G . 1
= r &
G . 2
= s )
by FINSEQ_1:61;
A19:
n = 1
by A5, A11, A17, XXREAL_0:1;
C = <*[.r,s.]*>
by A1, A2, A3, A4, A17, Th66;
hence
[.(G . n),(G . (n + 1)).] c= C . n
by A18, A19, FINSEQ_1:57;
:: thesis: verum end; suppose
r < s
;
:: thesis: [.(G . n),(G . (n + 1)).] c= C . nthen
G is
increasing
by A1, A2, A3, Th79;
then A20:
G . n < G . (n + 1)
by A8, A9, A16, SEQM_3:def 1;
A21:
2
<= len G
by A1, A2, A3, A4, Th74;
per cases
( ( n = 1 & len G = 2 ) or ( n = 1 & 1 + 1 < len G ) or ( 1 < n & len G = n + 1 ) or ( 1 < n & n + 1 < len G ) )
by A5, A7, A21, XXREAL_0:1;
suppose that A22:
n = 1
and A23:
len G = 2
;
:: thesis: [.(G . n),(G . (n + 1)).] c= C . n
G = <*r,s*>
by A1, A2, A3, A4, A10, A23, Th75;
then A24:
(
G . 1
= r &
G . 2
= s )
by FINSEQ_1:61;
C = <*[.r,s.]*>
by A1, A2, A3, A4, A10, A23, Th66;
hence
[.(G . n),(G . (n + 1)).] c= C . n
by A22, A24, FINSEQ_1:57;
:: thesis: verum end; suppose that A25:
n = 1
and A26:
1
+ 1
< len G
;
:: thesis: [.(G . n),(G . (n + 1)).] c= C . nA27:
G . (1 + 1) in ].(lower_bound (C /. (1 + 1))),(upper_bound (C /. 1)).[
by A1, A2, A3, A4, A26, Def3;
A28:
G . 1
= r
by A1, A2, A3, A4, Def3;
A29:
1
+ 1
<= len C
by A10, A26, NAT_1:13;
A30:
r in C /. 1
by A1, A2, A3, A4, Th71;
A31:
G . (n + 1) < upper_bound (C /. n)
by A1, A2, A3, A4, A25, A26, Th76;
A32:
lower_bound (C /. 1) <= lower_bound (C /. (1 + 1))
by A1, A2, A3, A4, A29, Def2;
lower_bound (C /. (1 + 1)) < G . 2
by A27, XXREAL_1:4;
then
lower_bound (C /. n) < G . (n + 1)
by A25, A32, XXREAL_0:2;
then
G . (n + 1) in C . n
by A12, A14, A15, A31, Th42;
hence
[.(G . n),(G . (n + 1)).] c= C . n
by A12, A14, A25, A28, A30, JCT_MISC:def 1;
:: thesis: verum end; suppose that A33:
1
< n
and A34:
len G = n + 1
;
:: thesis: [.(G . n),(G . (n + 1)).] c= C . nA35:
G . (len G) = s
by A1, A2, A3, A4, Def3;
A36:
lower_bound (C /. n) < G . n
by A1, A2, A3, A4, A10, A33, A34, Th77;
A37:
1
- 1
< n - 1
by A33, XREAL_1:11;
then A38:
0 + 1
<= n - 1
by INT_1:20;
A39:
n - 1 is
Element of
NAT
by A37, INT_1:16;
then
G . ((n - 1) + 1) in ].(lower_bound (C /. ((n - 1) + 1))),(upper_bound (C /. (n - 1))).[
by A1, A2, A3, A4, A16, A34, A38, Def3;
then A40:
G . n < upper_bound (C /. (n - 1))
by XXREAL_1:4;
upper_bound (C /. (n - 1)) <= upper_bound (C /. ((n - 1) + 1))
by A1, A2, A3, A4, A10, A34, A38, A39, Def2;
then
G . n < upper_bound (C /. n)
by A40, XXREAL_0:2;
then A41:
G . n in C . n
by A12, A14, A15, A36, Th42;
G . (n + 1) in C . n
by A1, A2, A3, A4, A10, A12, A34, A35, Th73;
hence
[.(G . n),(G . (n + 1)).] c= C . n
by A12, A14, A41, JCT_MISC:def 1;
:: thesis: verum end; suppose that A42:
1
< n
and A43:
n + 1
< len G
;
:: thesis: [.(G . n),(G . (n + 1)).] c= C . n
n <= len C
by A6, A10, NAT_1:13;
then A44:
lower_bound (C /. n) < G . n
by A1, A2, A3, A4, A42, Th77;
A45:
G . (n + 1) < upper_bound (C /. n)
by A1, A2, A3, A4, A5, A43, Th76;
then
G . n < upper_bound (C /. n)
by A20, XXREAL_0:2;
then A46:
G . n in C . n
by A12, A14, A15, A44, Th42;
lower_bound (C /. n) < G . (n + 1)
by A20, A44, XXREAL_0:2;
then
G . (n + 1) in C . n
by A12, A14, A15, A45, Th42;
hence
[.(G . n),(G . (n + 1)).] c= C . n
by A12, A14, A46, JCT_MISC:def 1;
:: thesis: verum end; end;