let r, s be Real; :: 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 holds
G is increasing
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 holds
G is increasing
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 holds
G is increasing
let G be IntervalCoverPts of C; :: thesis: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r < s implies G is increasing )
assume that
A1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected ) and
A2: r < s ; :: thesis: G is increasing
let m, n be Nat; :: according to SEQM_3:def 1 :: thesis: ( not m in dom G or not n in dom G or n <= m or not G . n <= G . m )
assume A3: ( m in dom G & n in dom G & m < n ) ; :: thesis: not G . n <= G . m
defpred S2[ Nat] means ( m < $1 & m in dom G & $1 in dom G implies G . m < G . $1 );
A4: for k being Nat st S2[k] holds
S2[k + 1]
proof
A5: len G = (len C) + 1 by A1, A2, Def3;
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume that
A6: S2[k] and
A7: m < k + 1 and
A8: m in dom G and
A9: k + 1 in dom G ; :: thesis: G . m < G . (k + 1)
A10: 1 <= m by A8, FINSEQ_3:25;
A11: k + 1 <= len G by A9, FINSEQ_3:25;
k + 0 <= k + 1 by XREAL_1:6;
then A12: k <= len G by A11, XXREAL_0:2;
A13: m <= k by A7, NAT_1:13;
then A14: 1 <= k by A10, XXREAL_0:2;
per cases ( ( 1 < k & k + 1 < len G ) or k = 1 or k + 1 = len G ) by A14, A11, XXREAL_0:1;
suppose that A15: 1 < k and
A16: k + 1 < len G ; :: thesis: G . m < G . (k + 1)
G . (k + 1) in ].(lower_bound (C /. (k + 1))),(upper_bound (C /. k)).[ by A1, A2, A15, A16, Def3;
then A17: lower_bound (C /. (k + 1)) < G . (k + 1) by XXREAL_1:4;
k < len C by A5, A16, XREAL_1:6;
then G . k <= lower_bound (C /. (k + 1)) by A1, A2, A15, Th64;
then G . k < G . (k + 1) by A17, XXREAL_0:2;
hence G . m < G . (k + 1) by A6, A8, A13, A12, A15, FINSEQ_3:25, XXREAL_0:1, XXREAL_0:2; :: thesis: verum
end;
suppose A18: k = 1 ; :: thesis: G . m < G . (k + 1)
A19: 1 <= len C by A1, A2, Th51;
A20: m <= 1 by A7, A18, NAT_1:13;
per cases ( 1 < len C or 1 = len C ) by A19, XXREAL_0:1;
suppose A21: 1 < len C ; :: thesis: G . m < G . (k + 1)
then 1 + 1 <= len C by NAT_1:13;
then A22: lower_bound (C /. 2) < G . 2 by A1, A2, Th63;
G . 1 <= lower_bound (C /. (1 + 1)) by A1, A2, A21, Th64;
then G . 1 < G . 2 by A22, XXREAL_0:2;
hence G . m < G . (k + 1) by A10, A18, A20, XXREAL_0:1; :: thesis: verum
end;
suppose 1 = len C ; :: thesis: G . m < G . (k + 1)
then G = <*r,s*> by A1, A2, Th61;
then ( G . 1 = r & G . 2 = s ) ;
hence G . m < G . (k + 1) by A2, A10, A18, A20, XXREAL_0:1; :: thesis: verum
end;
end;
end;
suppose A23: k + 1 = len G ; :: thesis: G . m < G . (k + 1)
then A24: G . (k + 1) = s by A1, A2, Def3;
per cases ( 1 < m or m = 1 ) by A10, XXREAL_0:1;
suppose A25: 1 < m ; :: thesis: G . m < G . (k + 1)
set z = m -' 1;
1 - 1 <= m - 1 by A10, XREAL_1:9;
then A26: m -' 1 = m - 1 by XREAL_0:def 2;
then A27: (m -' 1) + 1 < len G by A7, A23;
then A28: m -' 1 <= len C by A5, XREAL_1:6;
1 + 1 <= m by A25, NAT_1:13;
then A29: (1 + 1) - 1 <= m - 1 by XREAL_1:9;
then A30: 1 <= m -' 1 by XREAL_0:def 2;
then A31: not C /. (m -' 1) is empty by A1, A2, A28, Def2;
A32: rng C c= F by A1, A2, Def2;
A33: m -' 1 in dom C by A30, A28, FINSEQ_3:25;
then C . (m -' 1) in rng C by FUNCT_1:def 3;
then C . (m -' 1) in F by A32;
then C /. (m -' 1) in F by A33, PARTFUN1:def 6;
then C /. (m -' 1) c= the carrier of (Closed-Interval-TSpace (r,s)) ;
then A34: C /. (m -' 1) c= [.r,s.] by A2, TOPMETR:18;
then C /. (m -' 1) is bounded_above by XXREAL_2:43;
then upper_bound (C /. (m -' 1)) in [.r,s.] by A34, A31, Th2;
then A35: upper_bound (C /. (m -' 1)) <= s by XXREAL_1:1;
G . m < upper_bound (C /. (m -' 1)) by A1, A2, A26, A29, A27, Th62;
hence G . m < G . (k + 1) by A24, A35, XXREAL_0:2; :: thesis: verum
end;
suppose m = 1 ; :: thesis: G . m < G . (k + 1)
hence G . m < G . (k + 1) by A1, A2, A24, Def3; :: thesis: verum
end;
end;
end;
end;
end;
A36: S2[ 0 ] ;
for k being Nat holds S2[k] from NAT_1:sch 2(A36, A4);
 hence not G . n <= G . m by A3; :: thesis: verum