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