:: Cousin's Lemma :: by Roland Coghetto :: :: Received December 31, 2015 :: Copyright (c) 2015-2021 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 ORDINAL1, 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;