:: 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 b₁ being SetSequence of (REAL 1) st
for i being Nat holds b₁ . i = product <*[.(a . i),(b . i).]*>

proof end;

uniqueness
for b₁, b₂ being SetSequence of (REAL 1) st ( for i being Nat holds b₁ . i = product <*[.(a . i),(b . i).]*> ) & ( for i being Nat holds b₂ . i = product <*[.(a . i),(b . i).]*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines IntervalSequence COUSIN:def 1 :
for a, b being Real_Sequence
for b₃ being SetSequence of (REAL 1) holds
( b₃ = IntervalSequence (a,b) iff for i being Nat holds b₃ . 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 b₁ being Subset of (REAL *) st
for x being object holds
( x in b₁ 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 b₁, b₂ being Subset of (REAL *) st ( for x being object holds
( x in b₁ 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 b₂ 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
b₁ = b₂

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 b₃ being Subset of (REAL *) holds
( b₃ = set_of_tagged_Division D iff for x being object holds
( x in b₃ 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 b₁ being object ex D being Division of I ex T being Element of set_of_tagged_Division D st b₁ = [D,T]

proof end;

end;

:: deftheorem Def3 defines tagged_division COUSIN:def 3 :
for I being non empty closed_interval Subset of REAL
for b₂ being object holds
( b₂ is tagged_division of I iff ex D being Division of I ex T being Element of set_of_tagged_Division D st b₂ = [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 b₁ 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 b₁ being Element of set_of_tagged_Division D holds not b₁ 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 b₁, D being Division of I ex T being Element of set_of_tagged_Division D st
( b₁ = D & TD = [D,T] )

proof end;

uniqueness
for b₁, b₂ being Division of I st ex D being Division of I ex T being Element of set_of_tagged_Division D st
( b₁ = D & TD = [D,T] ) & ex D being Division of I ex T being Element of set_of_tagged_Division D st
( b₂ = D & TD = [D,T] ) holds
b₁ = b₂ 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 b₃ being Division of I holds
( b₃ = division_of TD iff ex D being Division of I ex T being Element of set_of_tagged_Division D st
( b₃ = 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;

:: 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 b₁ being tagged_division of I st b₁ is jauge -fine by Th47;

end;