:: by Roland Coghetto

::

:: Received December 31, 2015

:: Copyright (c) 2015-2019 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

p ^ q is non empty increasing FinSequence of REAL

proof end;

theorem :: COUSIN:10

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).||

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 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 )

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 )

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;

registration
end;

definition

let a, b be Real_Sequence;

ex b_{1} being SetSequence of (REAL 1) st

for i being Nat holds b_{1} . i = product <*[.(a . i),(b . i).]*>

for b_{1}, b_{2} being SetSequence of (REAL 1) st ( for i being Nat holds b_{1} . i = product <*[.(a . i),(b . i).]*> ) & ( for i being Nat holds b_{2} . i = product <*[.(a . i),(b . i).]*> ) holds

b_{1} = b_{2}

end;
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 for i being Nat holds it . i = product <*[.(a . i),(b . i).]*>;

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines IntervalSequence COUSIN:def 1 :

for a, b being Real_Sequence

for b_{3} being SetSequence of (REAL 1) holds

( b_{3} = IntervalSequence (a,b) iff for i being Nat holds b_{3} . i = product <*[.(a . i),(b . i).]*> );

for a, b being Real_Sequence

for b

( b

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).|

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

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

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)

( 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()

( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ) holds

IntervalSequence (a,b) is V238()

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

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 )

( 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

( ( 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) )

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 )

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

( ( 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 )

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

( ( 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 ) )

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 :: 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.] )

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;

ex b_{1} being Subset of (REAL *) st

for x being object holds

( x in b_{1} 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 b_{1}, b_{2} being Subset of (REAL *) st ( for x being object holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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) ) ) );

ex b

for x being object holds

( x in b

( 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

( x in b

( 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

( x = s & dom s = dom D & ( for i being Nat st i in dom s holds

s . i in divset (D,i) ) ) ) ) holds

b

proof 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_{3} being Subset of (REAL *) holds

( b_{3} = set_of_tagged_Division D iff for x being object holds

( x in b_{3} 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 A being non empty closed_interval Subset of REAL

for D being Division of A

for b

( b

( x in b

( 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

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

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;

ex b_{1} being object ex D being Division of I ex T being Element of set_of_tagged_Division D st b_{1} = [D,T]

end;
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 D being Division of I ex T being Element of set_of_tagged_Division D st it = [D,T];

ex b

proof end;

:: deftheorem Def3 defines tagged_division COUSIN:def 3 :

for I being non empty closed_interval Subset of REAL

for b_{2} being object holds

( b_{2} is tagged_division of I iff ex D being Division of I ex T being Element of set_of_tagged_Division D st b_{2} = [D,T] );

for I being non empty closed_interval Subset of REAL

for b

( b

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;

end;
let jauge be positive-yielding Function of I,REAL;

let TD be tagged_division of I;

:: 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) ) ) );

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: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;

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).] )

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 ;

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_{1} being non empty increasing FinSequence of REAL holds verum;

end;
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 Dac ^ Dcb if Dcb . 1 <> upper_bound Iac

otherwise Dac ^ (Dcb /^ 1);

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

proof 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) ) );

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

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

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

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;

coherence

not set_of_tagged_Division D is empty by Th34;

end;
let D be Division of I;

coherence

not set_of_tagged_Division D is empty by Th34;

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

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

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 )

( 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).] ) )

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

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;

coherence

for b_{1} being Element of set_of_tagged_Division D holds not b_{1} is empty

end;
let D be Division of I;

coherence

for b

proof 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

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;

ex b_{1}, D being Division of I ex T being Element of set_of_tagged_Division D st

( b_{1} = D & TD = [D,T] )

for b_{1}, b_{2} being Division of I st ex D being Division of I ex T being Element of set_of_tagged_Division D st

( b_{1} = D & TD = [D,T] ) & ex D being Division of I ex T being Element of set_of_tagged_Division D st

( b_{2} = D & TD = [D,T] ) holds

b_{1} = b_{2}
by XTUPLE_0:1;

end;
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 D being Division of I ex T being Element of set_of_tagged_Division D st

( it = D & TD = [D,T] );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: 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_{3} being Division of I holds

( b_{3} = division_of TD iff ex D being Division of I ex T being Element of set_of_tagged_Division D st

( b_{3} = D & TD = [D,T] ) );

for I being non empty closed_interval Subset of REAL

for TD being tagged_division of I

for b

( b

( b

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))

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))

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

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

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.[ ) ) ) ) )

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.] ) )

( ( 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 ) ) )

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 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 ) )

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

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

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*>

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

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

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)) ) ) )

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

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;

existence

ex b_{1} being tagged_division of I st b_{1} is jauge -fine
by Th47;

end;
let jauge be positive-yielding Function of I,REAL;

existence

ex b