:: Cousin's Lemma
:: by Roland Coghetto
::
:: Received December 31, 2015
:: Copyright (c) 2015-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XREAL_0, VALUED_1, INT_1, NEWTON, MEMBERED, PARTFUN1, RCOMP_3,
TOPMETR, SEQ_4, INTEGRA1, MEASURE7, COUSIN, NORMSP_2, SETFAM_1, RELAT_1,
COMPL_SP, PROB_1, FUNCT_2, NUMBERS, SUBSET_1, NAT_1, FUNCT_1, ARYTM_3,
FINSEQ_2, ZFMISC_1, COMPLEX1, STRUCT_0, XBOOLE_0, NORMSP_1, EUCLID,
PRE_TOPC, REAL_1, CARD_1, XXREAL_0, ARYTM_1, FINSEQ_1, CARD_3, ORDINAL4,
TARSKI, SQUARE_1, SEQ_2, ORDINAL2, SEQ_1, RSSPACE3, REWRITE1, METRIC_1,
BHSP_3, REAL_NS1, NORMSP_0, XXREAL_2, XXREAL_1, MEASURE5, RCOMP_1,
PCOMPS_1, POWER, RFINSEQ, RELAT_2, PARTFUN3, VALUED_0;
notations INT_1, NEWTON, VALUED_1, MEMBERED, PARTFUN1, CONNSP_1, SETFAM_1,
TOPS_2, TOPMETR, XXREAL_2, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, XCMPLX_0,
XXREAL_0, FINSEQ_1, RFINSEQ, METRIC_1, ZFMISC_1, SUBSET_1, BINOP_1,
PRE_TOPC, NAT_1, FINSEQ_2, FUNCT_2, STRUCT_0, NUMBERS, XREAL_0, SQUARE_1,
COMPLEX1, RLVECT_1, SEQ_1, SEQ_2, RVSUM_1, NORMSP_0, NORMSP_1, RSSPACE3,
REAL_NS1, TBSP_1, EUCLID, PROB_1, KURATO_0, RELSET_1, PCOMPS_1, CARD_3,
KURATO_2, NORMSP_2, COMPL_SP, RCOMP_1, MEASURE5, SEQ_4, INTEGRA1, SEQM_3,
PARTFUN3, RCOMP_3, MATRPROB, POWER;
constructors NEWTON, CONNSP_1, TOPS_2, RCOMP_3, SQUARE_1, RSSPACE3, LOPBAN_1,
RVSUM_1, COMSEQ_2, REAL_NS1, TBSP_1, KURATO_0, COMPL_SP, FRECHET,
NORMSP_2, SEQ_4, INTEGRA1, MEASURE6, RFINSEQ, REAL_1, PARTFUN3, MATRPROB,
POWER;
registrations SEQ_2, LOPBAN_5, VALUED_1, XXREAL_2, METRIC_1, MATRTOP1,
BORSUK_5, JORDAN5A, COMPLEX1, SUBSET_1, FUNCT_1, RELSET_1, XXREAL_0,
XREAL_0, MEMBERED, STRUCT_0, VALUED_0, FUNCT_2, EUCLID, FINSEQ_1, CARD_1,
NAT_1, REAL_NS1, COMPL_SP, MEASURE5, INTEGRA1, SEQM_3, RELAT_1, ORDINAL1,
XCMPLX_0, NUMBERS, INT_1, RVSUM_1, SEQ_4, PARTFUN3, POWER;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
begin :: Preliminaries
theorem :: 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;
theorem :: COUSIN:2
for a,b being Real st 1 < a & 0 < b < 1 holds log(a,b) < 0;
theorem :: COUSIN:3
for a,b being Real st 1 < a & 1 < b holds 0 < log(a,b);
theorem :: COUSIN:4
for x being object holds product <*{x}*> = {<*x*>};
theorem :: COUSIN:5
for x being Element of REAL 1 holds ex rx being Real st x = <*rx*>;
theorem :: COUSIN:6
for a being Real holds <*a*> is Point of Euclid 1;
theorem :: COUSIN:7
for a,b being Real st a <= b holds a <= (a+b)/2 <= b;
theorem :: COUSIN:8
for a,b,c being Real st a <= b & b < c holds a < (b+c)/2;
theorem :: COUSIN:9
for a,b being Real st a < b holds (a+b)/2 < b;
theorem :: COUSIN:10
for a,b being Real st a <= b holds
[.a,b.] is non empty compact Subset of REAL;
theorem :: COUSIN:11
for f being FinSequence st 2 <= len f holds (f /^ 1 ).len(f /^ 1) = f.len(f);
begin :: Euclid n is complete - Proof Version 1
reserve n for Nat;
reserve s1 for sequence of Euclid n,
s2 for sequence of REAL-NS n;
theorem :: COUSIN:12
for x,y being Element of Euclid n,
g,h being Point of REAL-NS n st x = g & y = h holds
dist(x,y) = ||. g - h .||;
theorem :: COUSIN:13
the carrier of REAL-NS n = the carrier of Euclid n;
theorem :: COUSIN:14
s1 = s2 implies (s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm);
theorem :: COUSIN:15
s1 = s2 implies (s1 is convergent iff s2 is convergent);
theorem :: COUSIN:16
for S2 being sequence of Euclid n st S2 is Cauchy holds S2 is convergent;
theorem :: COUSIN:17
Euclid n is complete;
begin :: Euclid n is complete - Proof Version 2
theorem :: COUSIN:18
distance_by_norm_of REAL-NS n = Pitag_dist n;
theorem :: COUSIN:19
MetricSpaceNorm REAL-NS n = Euclid n;
registration
let n be Nat;
cluster Euclid n -> complete;
end;
begin :: The Nested Intervals Theorem (1-dimensional Euclidean space)
definition
let a,b be Real_Sequence;
func IntervalSequence(a,b) -> SetSequence of REAL 1 means
:: COUSIN:def 1
for i being Nat holds it.i = product <* [.a.i,b.i.] *>;
end;
theorem :: COUSIN:20
for a,b being Real_Sequence holds
IntervalSequence(a,b) is SetSequence of Euclid 1;
theorem :: COUSIN:21
product <*REAL*> = REAL 1;
theorem :: COUSIN:22
for a,b being Real, xa,xb being Point of Euclid 1 st
xa = <*a*> & xb = <*b*> holds dist(xa,xb) = |.a - b.|;
theorem :: COUSIN:23
for a,b being Real, 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;
theorem :: COUSIN:24
for a,b being Real, S being Subset of Euclid 1 st a <= b &
S = product<*[.a,b.]*> holds S is bounded;
theorem :: 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;
theorem :: 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 non-ascending;
theorem :: COUSIN:27
for a,b,x being Real st a <= x <= b holds
<*x*> in product <*[.a,b.]*>;
theorem :: COUSIN:28
for a,b being Real, S being Subset of Euclid 1 st a <= b &
S = product <*[.a,b.]*> holds diameter S = b - a;
theorem :: 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;
theorem :: 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;
theorem :: COUSIN:31
for a,b being Real_Sequence, 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;
theorem :: COUSIN:32
for a,b being Real_Sequence, 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;
theorem :: 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,r being Real st r = 2|^i & r <> 0 holds
b.i - a.i <= (b.0-a.0) / r);
theorem :: COUSIN:34
for a,b being Real_Sequence, 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;
theorem :: 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 meet IntervalSequence(a,b) is non empty;
theorem :: COUSIN:36
for r being Real,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 be Nat holds a.j <= c <= b.j) &
ex k being Nat st c - r < a.k & b.k < c + r;
begin :: Tagged division
theorem :: COUSIN:37
for I being non empty closed_interval Subset of REAL
holds ex a,b being Real st a <= b & I = [.a,b.];
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 <= b & I1 = [.a,c.] & I2 = [.c,b.];
definition
let A be non empty closed_interval Subset of REAL,
D be Division of A;
func set_of_tagged_Division(D) -> Subset of REAL* means
:: 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);
end;
theorem :: COUSIN:39
for A being non empty closed_interval Subset of REAL,
D being Division of A holds D in set_of_tagged_Division(D);
theorem :: COUSIN:40
for a,b being Real, Iab being non empty closed_interval Subset of REAL
st Iab = [.a,b.] holds <*b*> is Division of Iab;
definition
let I be non empty closed_interval Subset of REAL;
mode tagged_division of I means
:: COUSIN:def 3
ex D being Division of I,
T being Element of set_of_tagged_Division(D) st
it = [D,T];
end;
definition
let I be non empty closed_interval Subset of REAL,
jauge be positive-yielding Function of I,REAL,
TD be tagged_division of I;
attr TD is jauge-fine means
:: COUSIN:def 4
ex D being Division of I, 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;
begin :: Division composition
theorem :: COUSIN:41
for r being Real holds vol {r} = 0;
theorem :: COUSIN:42
for I1,I2 being non empty closed_interval Subset of REAL,
jauge being positive-yielding Function of I1,REAL st I2 c= I1 holds
jauge|I2 is positive-yielding Function of I2,REAL;
theorem :: COUSIN:43
for I being non empty closed_interval Subset of REAL, 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.];
definition
let Iac,Icb be non empty closed_interval Subset of REAL,
Dac be Division of Iac,
Dcb be Division of Icb;
assume
upper_bound(Iac) <= lower_bound(Icb);
func Dac (#) Dcb -> non empty increasing FinSequence of REAL equals
:: COUSIN:def 5
Dac ^ Dcb if Dcb.1 <> upper_bound(Iac)
otherwise
Dac ^ (Dcb/^1);
end;
theorem :: COUSIN:44
for Iac,Icb being non empty closed_interval Subset of REAL,
Dac being Division of Iac, Dcb being Division of Icb st
upper_bound(Iac) = lower_bound(Icb) &
len Dcb = 1 &
Dcb.1 = lower_bound(Icb) holds
Dac (#) Dcb = Dac;
theorem :: 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;
theorem :: COUSIN:46
for I1,I2,I being non empty closed_interval Subset of REAL,
D1 being Division of I1, 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;
registration
let I be non empty closed_interval Subset of REAL,
D be Division of I;
cluster set_of_tagged_Division(D) -> non empty;
end;
theorem :: COUSIN:47
for s being non empty increasing FinSequence of REAL,
r being Real st s.len s < r holds
s ^ <*r*> is non empty increasing FinSequence of REAL;
theorem :: COUSIN:48
for s1,s2 being non empty increasing FinSequence of REAL,
r being Real st s1.len s1 < r < s2.1
holds s1 ^ <*r*> ^ s2 is non empty increasing FinSequence of REAL;
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;
theorem :: COUSIN:50
for I being non empty closed_interval Subset of REAL,
D being Division of I holds
divset(D,1) = [.lower_bound I,D.1.] &
for j be Nat st j in dom D & j <> 1 holds divset(D,j) = [.D.(j-1),D.j.];
theorem :: COUSIN:51
for r being Real, p,q being FinSequence of REAL
holds len (p ^ <*r*> ^ q) = len p + len q + 1;
registration
let I be non empty closed_interval Subset of REAL,
D be Division of I;
cluster -> non empty for Element of set_of_tagged_Division(D);
end;
theorem :: COUSIN:52
for I being non empty closed_interval Subset of REAL,
D being Division of I, T being Element of set_of_tagged_Division(D) holds
rng T c= REAL;
definition
let I be non empty closed_interval Subset of REAL,
TD be tagged_division of I;
func division_of(TD) -> Division of I means
:: COUSIN:def 6
ex D being Division of I, T being Element of set_of_tagged_Division(D) st
it = D & TD = [D,T];
end;
begin :: Examples of Division
reserve r,s for Real;
theorem :: COUSIN:53
for jauge being Function of [.r,s.],].0,+infty.[ st r <= s holds
the set of all ]. x - jauge.x, x + jauge.x .[ /\ [.r,s.] where x is Element
of [.r,s.] is Subset-Family of Closed-Interval-TSpace(r,s);
theorem :: COUSIN:54
for jauge being Function of [.r,s.],].0,+infty.[,
S being Subset-Family of Closed-Interval-TSpace(r,s) st r <= s &
S = the set of all ].x-jauge.x,x+jauge.x.[ /\ [.r,s.] where
x is Element of [.r,s.] holds
S is Cover of Closed-Interval-TSpace(r,s);
theorem :: COUSIN:55
for jauge being Function of [.r,s.],].0,+infty.[,
S being Subset-Family of Closed-Interval-TSpace(r,s) st r <= s &
S = the set of all ].x-jauge.x,x+jauge.x.[ /\ [.r,s.] where
x is Element of [.r,s.] holds S is open;
theorem :: COUSIN:56
for jauge being Function of [.r,s.],].0,+infty.[,
S being Subset-Family of Closed-Interval-TSpace(r,s)
st S = the set of all ].x-jauge.x,x+jauge.x.[ /\ [.r,s.] where
x is Element of [.r,s.] holds S is connected;
theorem :: COUSIN:57
for jauge being Function of [.r,s.],].0,+infty.[,
S be Subset-Family of Closed-Interval-TSpace(r,s)
st r <= s &
S = the set of all ].x-jauge.x,x+jauge.x.[ /\ [.r,s.] where
x is Element of [.r,s.] 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 IC/.n is non 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 ex p, q being Real st
r <= p & p < q & q <= s & IC.n = ].p,q.[ );
theorem :: 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.]);
theorem :: COUSIN:59
for r,s,t,x being Real,XT being Subset of REAL st
0 < t & r <= 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);
theorem :: COUSIN:60
for a,b being Real st a < b holds <*a,b*> is non empty increasing
FinSequence of REAL;
theorem :: COUSIN:61
for a,b,c being Real,Iac,Icb being non empty compact Subset of REAL st
a <= c <= b & Iac=[.a,c.] & Icb=[.c,b.] holds
for Dac being Division of Iac, Dcb being Division of Icb,
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);
theorem :: COUSIN:62
for a,b,c being Real,Iac,Icb being non empty compact Subset of REAL st
a <= c <= b & Iac=[.a,c.] & Icb=[.c,b.] holds
for Dac being Division of Iac, Dcb being Division of Icb,
i,j being Nat st i in dom Dac & j in dom Dcb holds
c < Dcb.1 implies Dac.i < Dcb.j;
theorem :: COUSIN:63
for a,b,c being Real,Iab,Iac,Icb being non empty compact Subset of REAL st
a <= c <= b & Iab = [.a,b.] & Iac=[.a,c.] & Icb=[.c,b.] holds
for Dac being Division of Iac, Dcb being Division of Icb st c < Dcb.1 holds
Dac ^ Dcb is Division of Iab;
theorem :: COUSIN:64
for a,b being Real,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*>;
theorem :: COUSIN:65
for a,b being Real,
Iab being non empty compact Subset of REAL,
Dab being Division of Iab st 2 <= len Dab holds
(Dab/^1) is Division of Iab;
theorem :: COUSIN:66
for a,b being Real, Iab being non empty closed_interval Subset of REAL
st a < b & Iab = [.a,b.] holds <*a,b*> is Division of Iab;
begin :: Cousin's Lemma
theorem :: COUSIN:67
for a,b being Real,
jauge being positive-yielding Function of [.a,b.],REAL st a <= b holds
ex x being non empty increasing FinSequence of REAL, 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) <= t.i) &
(for i being Nat st i in dom t holds t.i <= x.i <= t.i + jauge.(t.i));
::$N Cousin's lemma
theorem :: COUSIN:68
for I being non empty closed_interval Subset of REAL,
jauge being positive-yielding Function of I,REAL holds
ex TD being tagged_division of I st TD is jauge-fine;
registration
let I be non empty closed_interval Subset of REAL,
jauge be positive-yielding Function of I,REAL;
cluster jauge-fine for tagged_division of I;
end;