:: Cousin's Lemma
:: by Roland Coghetto
::
:: Received December 31, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


theorem Th1: :: COUSIN:1
for p, q being non empty increasing FinSequence of REAL st p . (len p) < q . 1 holds
p ^ q is non empty increasing FinSequence of REAL
proof end;

theorem :: COUSIN:2
for a, b being Real st 1 < a & 0 < b & b < 1 holds
log (a,b) < 0
proof end;

theorem Th2: :: COUSIN:3
for a, b being Real st 1 < a & 1 < b holds
0 < log (a,b)
proof end;

theorem Th5: :: COUSIN:4
for x being object holds product <*{x}*> = {<*x*>}
proof end;

theorem Th6: :: COUSIN:5
for x being Element of REAL 1 ex rx being Real st x = <*rx*>
proof end;

theorem Th7: :: COUSIN:6
for a being Real holds <*a*> is Point of (Euclid 1)
proof end;

theorem Th8: :: COUSIN:7
for a, b being Real st a <= b holds
( a <= (a + b) / 2 & (a + b) / 2 <= b )
proof end;

theorem :: COUSIN:8
for a, b, c being Real st a <= b & b < c holds
a < (b + c) / 2
proof end;

theorem :: COUSIN:9
for a, b being Real st a < b holds
(a + b) / 2 < b
proof end;

theorem :: COUSIN:10
for a, b being Real st a <= b holds
[.a,b.] is non empty compact Subset of REAL by XXREAL_1:30;

theorem :: COUSIN:11
for f being FinSequence st 2 <= len f holds
(f /^ 1) . (len (f /^ 1)) = f . (len f)
proof end;

theorem Th9: :: COUSIN:12
for n being Nat
for x, y being Element of (Euclid n)
for g, h being Point of (REAL-NS n) st x = g & y = h holds
dist (x,y) = ||.(g - h).||
proof end;

theorem Th10: :: COUSIN:13
for n being Nat holds the carrier of (REAL-NS n) = the carrier of (Euclid n)
proof end;

theorem Th11: :: COUSIN:14
for n being Nat
for s1 being sequence of (Euclid n)
for s2 being sequence of (REAL-NS n) st s1 = s2 holds
( s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm )
proof end;

theorem Th12: :: COUSIN:15
for n being Nat
for s1 being sequence of (Euclid n)
for s2 being sequence of (REAL-NS n) st s1 = s2 holds
( s1 is convergent iff s2 is convergent )
proof end;

theorem Th13: :: COUSIN:16
for n being Nat
for S2 being sequence of (Euclid n) st S2 is Cauchy holds
S2 is convergent
proof end;

theorem :: COUSIN:17
for n being Nat holds Euclid n is complete by Th13;

theorem Th14: :: COUSIN:18
for n being Nat holds distance_by_norm_of (REAL-NS n) = Pitag_dist n
proof end;

theorem Th15: :: COUSIN:19
for n being Nat holds MetricSpaceNorm (REAL-NS n) = Euclid n
proof end;

registration
let n be Nat;
cluster Euclid n -> complete ;
coherence
Euclid n is complete
proof end;
end;

definition
let a, b be Real_Sequence;
func IntervalSequence (a,b) -> SetSequence of (REAL 1) means :Def1: :: COUSIN:def 1
 for i being Nat holds it . i = product <*[.(a . i),(b . i).]*>;
existence
ex b1 being SetSequence of (REAL 1) st
for i being Nat holds b1 . i = product <*[.(a . i),(b . i).]*>
proof end;
uniqueness
for b1, b2 being SetSequence of (REAL 1) st ( for i being Nat holds b1 . i = product <*[.(a . i),(b . i).]*> ) & ( for i being Nat holds b2 . i = product <*[.(a . i),(b . i).]*> ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines IntervalSequence COUSIN:def 1 :
for a, b being Real_Sequence
for b3 being SetSequence of (REAL 1) holds
( b3 = IntervalSequence (a,b) iff for i being Nat holds b3 . i = product <*[.(a . i),(b . i).]*> );

theorem Th17: :: COUSIN:20
for a, b being Real_Sequence holds IntervalSequence (a,b) is SetSequence of (Euclid 1)
proof end;

theorem Th18: :: COUSIN:21
product <*REAL*> = REAL 1
proof end;

theorem Th19: :: COUSIN:22
for a, b being Real
for xa, xb being Point of (Euclid 1) st xa = <*a*> & xb = <*b*> holds
dist (xa,xb) = |.(a - b).|
proof end;

theorem Th20: :: COUSIN:23
for a, b being Real
for S being Subset of (Euclid 1) st a <= b & S = product <*[.a,b.]*> holds
for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= b - a
proof end;

theorem Th21: :: COUSIN:24
for a, b being Real
for S being Subset of (Euclid 1) st a <= b & S = product <*[.a,b.]*> holds
S is bounded
proof end;

theorem Th22: :: COUSIN:25
for a, b being Real_Sequence st ( for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ) holds
IntervalSequence (a,b) is non-empty pointwise_bounded closed SetSequence of (Euclid 1)
proof end;

theorem Th23: :: COUSIN:26
for a, b being Real_Sequence st ( for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ) holds
IntervalSequence (a,b) is V238()
proof end;

theorem Th24: :: COUSIN:27
for a, b, x being Real st a <= x & x <= b holds
<*x*> in product <*[.a,b.]*>
proof end;

theorem Th25: :: COUSIN:28
for a, b being Real
for S being Subset of (Euclid 1) st a <= b & S = product <*[.a,b.]*> holds
diameter S = b - a
proof end;

theorem Th26: :: COUSIN:29
for a, b being Real_Sequence st ( for i being Nat holds a . i <= b . i ) & a is non-decreasing & b is non-increasing holds
( a is convergent & b is convergent )
proof end;

theorem Th27: :: COUSIN:30
for a, b being Real_Sequence st a . 0 <= b . 0 & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
for i being Nat holds a . i <= b . i
proof end;

theorem Th28: :: COUSIN:31
for a, b being Real_Sequence
for S being SetSequence of (Euclid 1) st a . 0 <= b . 0 & S = IntervalSequence (a,b) & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i & (diameter S) . i = (b . i) - (a . i) )
proof end;

theorem Th29: :: COUSIN:32
for a, b being Real_Sequence
for S being SetSequence of (Euclid 1) st a . 0 = b . 0 & S = IntervalSequence (a,b) & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
for i being Nat holds
( a . i = a . 0 & b . i = b . 0 & (diameter S) . i = 0 )
proof end;

theorem Th30: :: COUSIN:33
for a, b being Real_Sequence st ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
for i being Nat
for r being Real st r = 2 |^ i & r <> 0 holds
(b . i) - (a . i) <= ((b . 0) - (a . 0)) / r
proof end;

theorem Th31: :: COUSIN:34
for a, b being Real_Sequence
for S being SetSequence of (Euclid 1) st a . 0 <= b . 0 & S = IntervalSequence (a,b) & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
( diameter S is convergent & lim (diameter S) = 0 )
proof end;

theorem Th32: :: COUSIN:35
for a, b being Real_Sequence st a . 0 <= b . 0 & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
not meet (IntervalSequence (a,b)) is empty
proof end;

theorem :: COUSIN:36
for r being Real
for a, b being Real_Sequence st 0 < r & a . 0 <= b . 0 & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
ex c being Real st
( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) )
proof end;

theorem Th33: :: COUSIN:37
for I being non empty closed_interval Subset of REAL ex a, b being Real st
( a <= b & I = [.a,b.] )
proof end;

theorem :: COUSIN:38
for I1, I2 being non empty closed_interval Subset of REAL st upper_bound I1 = lower_bound I2 holds
ex a, b, c being Real st
( a <= c & c <= b & I1 = [.a,c.] & I2 = [.c,b.] )
proof end;

definition
let A be non empty closed_interval Subset of REAL;
let D be Division of A;
func set_of_tagged_Division D -> Subset of (REAL *) means :Def2: :: COUSIN:def 2
 for x being object holds
( x in it iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) );
existence
ex b1 being Subset of (REAL *) st
for x being object holds
( x in b1 iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of (REAL *) st ( for x being object holds
( x in b1 iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) ) ) & ( for x being object holds
( x in b2 iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines set_of_tagged_Division COUSIN:def 2 :
for A being non empty closed_interval Subset of REAL
for D being Division of A
for b3 being Subset of (REAL *) holds
( b3 = set_of_tagged_Division D iff for x being object holds
( x in b3 iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) ) );

theorem Th34: :: COUSIN:39
for A being non empty closed_interval Subset of REAL
for D being Division of A holds D in set_of_tagged_Division D
proof end;

theorem Th35: :: COUSIN:40
for a, b being Real
for Iab being non empty closed_interval Subset of REAL st Iab = [.a,b.] holds
<*b*> is Division of Iab
proof end;

definition
let I be non empty closed_interval Subset of REAL;
mode tagged_division of I -> object means :Def3: :: COUSIN:def 3
 ex D being Division of I ex T being Element of set_of_tagged_Division D st it = [D,T];
existence
ex b1 being object ex D being Division of I ex T being Element of set_of_tagged_Division D st b1 = [D,T]
proof end;
end;

:: deftheorem Def3 defines tagged_division COUSIN:def 3 :
for I being non empty closed_interval Subset of REAL
for b2 being object holds
( b2 is tagged_division of I iff ex D being Division of I ex T being Element of set_of_tagged_Division D st b2 = [D,T] );

definition
let I be non empty closed_interval Subset of REAL;
let jauge be positive-yielding Function of I,REAL;
let TD be tagged_division of I;
attr TD is jauge -fine means :: COUSIN:def 4
 ex D being Division of I ex T being Element of set_of_tagged_Division D st
( TD = [D,T] & ( for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) ) );
end;

:: deftheorem defines -fine COUSIN:def 4 :
for I being non empty closed_interval Subset of REAL
for jauge being positive-yielding Function of I,REAL
for TD being tagged_division of I holds
( TD is jauge -fine iff ex D being Division of I ex T being Element of set_of_tagged_Division D st
( TD = [D,T] & ( for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) ) ) );

theorem :: COUSIN:41
for r being Real holds vol {r} = 0
proof end;

theorem :: COUSIN:42
for I1, I2 being non empty closed_interval Subset of REAL
for jauge being positive-yielding Function of I1,REAL st I2 c= I1 holds
jauge | I2 is positive-yielding Function of I2,REAL by FUNCT_2:32;

theorem :: COUSIN:43
for I being non empty closed_interval Subset of REAL
for c being Real st c in I holds
( [.(lower_bound I),c.] is non empty closed_interval Subset of REAL & [.c,(upper_bound I).] is non empty closed_interval Subset of REAL & upper_bound [.(lower_bound I),c.] = lower_bound [.c,(upper_bound I).] )
proof end;

definition
let Iac, Icb be non empty closed_interval Subset of REAL;
let Dac be Division of Iac;
let Dcb be Division of Icb;
assume A1: upper_bound Iac <= lower_bound Icb ;
func Dac (#) Dcb -> non empty increasing FinSequence of REAL equals :Def4: :: COUSIN:def 5
Dac ^ Dcb if Dcb . 1 <> upper_bound Iac
otherwise Dac ^ (Dcb /^ 1);
correctness
coherence
( ( Dcb . 1 <> upper_bound Iac implies Dac ^ Dcb is non empty increasing FinSequence of REAL ) & ( not Dcb . 1 <> upper_bound Iac implies Dac ^ (Dcb /^ 1) is non empty increasing FinSequence of REAL ) );
consistency
for b1 being non empty increasing FinSequence of REAL holds verum;
proof end;
end;

:: deftheorem Def4 defines (#) COUSIN:def 5 :
for Iac, Icb being non empty closed_interval Subset of REAL
for Dac being Division of Iac
for Dcb being Division of Icb st upper_bound Iac <= lower_bound Icb holds
( ( Dcb . 1 <> upper_bound Iac implies Dac (#) Dcb = Dac ^ Dcb ) & ( not Dcb . 1 <> upper_bound Iac implies Dac (#) Dcb = Dac ^ (Dcb /^ 1) ) );

theorem :: COUSIN:44
for Iac, Icb being non empty closed_interval Subset of REAL
for Dac being Division of Iac
for Dcb being Division of Icb st upper_bound Iac = lower_bound Icb & len Dcb = 1 & Dcb . 1 = lower_bound Icb holds
Dac (#) Dcb = Dac
proof end;

theorem Th37: :: COUSIN:45
for I1, I2, I being non empty closed_interval Subset of REAL st upper_bound I1 <= lower_bound I2 & lower_bound I <= lower_bound I1 & upper_bound I2 <= upper_bound I holds
I1 \/ I2 c= I
proof end;

theorem :: COUSIN:46
for I1, I2, I being non empty closed_interval Subset of REAL
for D1 being Division of I1
for D2 being Division of I2 st upper_bound I1 <= lower_bound I2 & I = [.(lower_bound I1),(upper_bound I2).] holds
D1 (#) D2 is Division of I
proof end;

registration
let I be non empty closed_interval Subset of REAL;
let D be Division of I;
cluster set_of_tagged_Division D -> non empty ;
coherence
not set_of_tagged_Division D is empty by Th34;
end;

theorem Th38: :: COUSIN:47
for s being non empty increasing FinSequence of REAL
for r being Real st s . (len s) < r holds
s ^ <*r*> is non empty increasing FinSequence of REAL
proof end;

theorem :: COUSIN:48
for s1, s2 being non empty increasing FinSequence of REAL
for r being Real st s1 . (len s1) < r & r < s2 . 1 holds
(s1 ^ <*r*>) ^ s2 is non empty increasing FinSequence of REAL
proof end;

theorem :: COUSIN:49
for I1, I2, I being non empty closed_interval Subset of REAL st upper_bound I1 = lower_bound I2 & I = I1 \/ I2 holds
( lower_bound I = lower_bound I1 & upper_bound I = upper_bound I2 )
proof end;

theorem :: COUSIN:50
for I being non empty closed_interval Subset of REAL
for D being Division of I holds
( divset (D,1) = [.(lower_bound I),(D . 1).] & ( for j being Nat st j in dom D & j <> 1 holds
divset (D,j) = [.(D . (j - 1)),(D . j).] ) )
proof end;

theorem :: COUSIN:51
for r being Real
for p, q being FinSequence of REAL holds len ((p ^ <*r*>) ^ q) = ((len p) + (len q)) + 1
proof end;

registration
let I be non empty closed_interval Subset of REAL;
let D be Division of I;
cluster -> non empty for Element of set_of_tagged_Division D;
coherence
for b1 being Element of set_of_tagged_Division D holds not b1 is empty
proof end;
end;

theorem :: COUSIN:52
for I being non empty closed_interval Subset of REAL
for D being Division of I
for T being Element of set_of_tagged_Division D holds rng T c= REAL
proof end;

definition
let I be non empty closed_interval Subset of REAL;
let TD be tagged_division of I;
func division_of TD -> Division of I means :: COUSIN:def 6
 ex D being Division of I ex T being Element of set_of_tagged_Division D st
( it = D & TD = [D,T] );
existence
ex b1, D being Division of I ex T being Element of set_of_tagged_Division D st
( b1 = D & TD = [D,T] )
proof end;
uniqueness
for b1, b2 being Division of I st ex D being Division of I ex T being Element of set_of_tagged_Division D st
( b1 = D & TD = [D,T] ) & ex D being Division of I ex T being Element of set_of_tagged_Division D st
( b2 = D & TD = [D,T] ) holds
b1 = b2 by XTUPLE_0:1;
end;

:: deftheorem defines division_of COUSIN:def 6 :
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for b3 being Division of I holds
( b3 = division_of TD iff ex D being Division of I ex T being Element of set_of_tagged_Division D st
( b3 = D & TD = [D,T] ) );

theorem :: COUSIN:53
for r, s being Real
for jauge being Function of [.r,s.],].0,+infty.[ st r <= s holds
{ (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } is Subset-Family of (Closed-Interval-TSpace (r,s))
proof end;

theorem Th39: :: COUSIN:54
for r, s being Real
for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is Cover of (Closed-Interval-TSpace (r,s))
proof end;

theorem Th40: :: COUSIN:55
for r, s being Real
for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is open
proof end;

theorem Th41: :: COUSIN:56
for r, s being Real
for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is connected
proof end;

theorem :: COUSIN:57
for r, s being Real
for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
for IC being IntervalCover of S holds
( IC is FinSequence of bool REAL & rng IC c= S & union (rng IC) = [.r,s.] & ( for n being Nat st 1 <= n holds
( ( n <= len IC implies not IC /. n is empty ) & ( n + 1 <= len IC implies ( lower_bound (IC /. n) <= lower_bound (IC /. (n + 1)) & upper_bound (IC /. n) <= upper_bound (IC /. (n + 1)) & lower_bound (IC /. (n + 1)) < upper_bound (IC /. n) ) ) & ( n + 2 <= len IC implies upper_bound (IC /. n) <= lower_bound (IC /. (n + 2)) ) ) ) & ( [.r,s.] in S implies IC = <*[.r,s.]*> ) & ( not [.r,s.] in S implies ( ex p being Real st
( r < p & p <= s & IC . 1 = [.r,p.[ ) & ex p being Real st
( r <= p & p < s & IC . (len IC) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len IC holds
ex p, q being Real st
( r <= p & p < q & q <= s & IC . n = ].p,q.[ ) ) ) ) )
proof end;

theorem Th42: :: COUSIN:58
for r, s, t, x being Real holds
( ( r <= x - t & x + t <= s implies ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),(x + t).[ ) & ( r <= x - t & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),s.] ) & ( x - t < r & x + t <= s implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[ ) & ( x - t < r & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.] ) )
proof end;

theorem :: COUSIN:59
for r, s, t, x being Real
for XT being Subset of REAL st 0 < t & r <= x & x <= s & XT = ].(x - t),(x + t).[ /\ [.r,s.] holds
( ( r <= x - t & x + t <= s implies ( lower_bound XT = x - t & upper_bound XT = x + t ) ) & ( r <= x - t & s < x + t implies ( lower_bound XT = x - t & upper_bound XT = s ) ) & ( x - t < r & x + t <= s implies ( lower_bound XT = r & upper_bound XT = x + t ) ) & ( x - t < r & s < x + t implies ( lower_bound XT = r & upper_bound XT = s ) ) )
proof end;

theorem Th45: :: COUSIN:60
for a, b being Real st a < b holds
<*a,b*> is non empty increasing FinSequence of REAL
proof end;

theorem Th43: :: COUSIN:61
for a, b, c being Real
for Iac, Icb being non empty compact Subset of REAL st a <= c & c <= b & Iac = [.a,c.] & Icb = [.c,b.] holds
for Dac being Division of Iac
for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb holds
( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) )
proof end;

theorem Th44: :: COUSIN:62
for a, b, c being Real
for Iac, Icb being non empty compact Subset of REAL st a <= c & c <= b & Iac = [.a,c.] & Icb = [.c,b.] holds
for Dac being Division of Iac
for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb & c < Dcb . 1 holds
Dac . i < Dcb . j
proof end;

theorem :: COUSIN:63
for a, b, c being Real
for Iab, Iac, Icb being non empty compact Subset of REAL st a <= c & c <= b & Iab = [.a,b.] & Iac = [.a,c.] & Icb = [.c,b.] holds
for Dac being Division of Iac
for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab
proof end;

theorem :: COUSIN:64
for a, b being Real
for Iab being non empty closed_interval Subset of REAL st a <= b & Iab = [.a,b.] holds
for Dab being Division of Iab st len Dab = 1 holds
Dab = <*b*>
proof end;

theorem :: COUSIN:65
for a, b being Real
for Iab being non empty compact Subset of REAL
for Dab being Division of Iab st 2 <= len Dab holds
Dab /^ 1 is Division of Iab
proof end;

theorem :: COUSIN:66
for a, b being Real
for Iab being non empty closed_interval Subset of REAL st a < b & Iab = [.a,b.] holds
<*a,b*> is Division of Iab
proof end;

theorem Th46: :: COUSIN:67
for a, b being Real
for jauge being positive-yielding Function of [.a,b.],REAL st a <= b holds
ex x being non empty increasing FinSequence of REAL ex t being non empty FinSequence of REAL st
( x . 1 = a & x . (len x) = b & t . 1 = a & dom x = dom t & ( for i being Nat st i - 1 in dom t & i in dom t holds
( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) ) & ( for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) ) )
proof end;

:: WP: Cousin's lemma
theorem Th47: :: COUSIN:68
for I being non empty closed_interval Subset of REAL
for jauge being positive-yielding Function of I,REAL ex TD being tagged_division of I st TD is jauge -fine
proof end;

registration
let I be non empty closed_interval Subset of REAL;
let jauge be positive-yielding Function of I,REAL;
cluster jauge -fine for tagged_division of I;
existence
ex b1 being tagged_division of I st b1 is jauge -fine by Th47;
end;