:: Cousin's Lemma :: by Roland Coghetto :: :: Received December 31, 2015 :: Copyright (c) 2015-2016 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; definitions TARSKI; equalities NORMSP_0, SUBSET_1, METRIC_1, XBOOLE_0; expansions FUNCT_1, NORMSP_1, STRUCT_0, TARSKI, TBSP_1, METRIC_1, XBOOLE_0, SEQM_3; theorems CGAMES_1, NUMBERS, FUNCT_6, BORSUK_4, NAT_6, VALUED_1, PROB_1, TOPREAL6, NEWTON, XXREAL_2, JORDAN6, PRE_TOPC, TOPS_2, SETFAM_1, TOPMETR, RCOMP_3, XTUPLE_0, PARTFUN1, VALUED_0, JORDAN5A, INTEGRA1, SRINGS_4, TOPREALC, METRIC_1, COMPL_SP, XXREAL_1, EUCLID, BINOP_1, ABSVALUE, RSSPACE3, FINSEQ_1, FINSEQ_2, FUNCT_2, LOPBAN_1, NAT_1, SQUARE_1, FUNCT_1, FINSEQ_5, XREAL_1, XXREAL_0, ORDINAL1, TBSP_1, REAL_NS1, XBOOLE_0, TARSKI, PCOMPS_1, XBOOLE_1, CARD_3, UNIFORM1, NORMSP_2, JORDAN2B, RFINSEQ, FINSEQ_3, XCMPLX_1, INT_1, MEASURE5, SEQ_4, PARTFUN3, SEQ_1, SEQ_2, TOPREAL3, POWER, MEMBERED; schemes NAT_1, FUNCT_2, XBOOLE_0; begin :: Preliminaries theorem Th1: 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 let p,q be non empty increasing FinSequence of REAL; assume A1: p.len(p) < q.1; set pq = p ^ q; now let e1,e2 be ExtReal; assume that A2: e1 in dom pq and A3: e2 in dom pq and A4: e1 < e2; per cases by A2,A3,FINSEQ_1:25; suppose A5: e1 in dom p & e2 in dom p; then A6: pq.e1 = p.e1 & pq.e2 = p.e2 by FINSEQ_1:def 7; e1 < e2 & p is increasing by A4; hence pq.e1 < pq.e2 by A5,A6; end; suppose A7: e1 in dom p & ex n be Nat st n in dom q & e2 = len p + n; then consider n0 be Nat such that A8: n0 in dom q and A9: e2 = len p + n0; A10: pq.e1 = p.e1 & pq.e2 = q.n0 by A7,A9,FINSEQ_1:def 7; rng q <> {}; then A11: 1 in dom q by FINSEQ_3:32; 1 <= n0 by A8,FINSEQ_3:25; then 1 = n0 or 1 < n0 by XXREAL_0:1; then A12: q.1 <= q.n0 by A8,A11,VALUED_0:def 13; rng p <> {}; then 1 in dom p by FINSEQ_3:32; then 1 in Seg len p by FINSEQ_1:def 3; then 1 <= len p by FINSEQ_1:1; then A13: len p in dom p by FINSEQ_3:25; e1 <= len p by A7,FINSEQ_3:25; then e1 < len p or e1 = len p by XXREAL_0:1; then p.e1 <= p.len p by A13,A7,VALUED_0:def 13; then p.e1 < q.1 by A1,XXREAL_0:2; hence pq.e1 < pq.e2 by A10,A12,XXREAL_0:2; end; suppose A14: (ex n be Nat st n in dom q & e1 = len p + n) & e2 in dom p; then consider n0 be Nat such that n0 in dom q and A15: e1 = len p + n0; A16: len p <= e1 by A15,NAT_1:11; e2 in Seg len p by A14,FINSEQ_1:def 3; then e2 <= len p by FINSEQ_1:1; hence pq.e1 < pq.e2 by A4,A16,XXREAL_0:2; end; suppose A17: (ex n be Nat st n in dom q & e1 = len p + n) & (ex n be Nat st n in dom q & e2 = len p + n); then consider n1 be Nat such that A18: n1 in dom q and A19: e1 = len p + n1; consider n2 be Nat such that A20: n2 in dom q and A21: e2 = len p + n2 by A17; A22: len p + n1 - len p < len p + n2 - len p by A4,A19,A21,XREAL_1:14; q.n1 = pq.e1 & q.n2 = pq.e2 by A18,A19,A20,A21,FINSEQ_1:def 7; hence pq.e1 < pq.e2 by A22,A18,A20,VALUED_0:def 13; end; end; then p ^ q is increasing; hence thesis; end; theorem for a,b being Real st 1 < a & 0 < b < 1 holds log(a,b) < 0 proof let a,b be Real; assume that A1: 1 < a and A2: 0 < b < 1; log(a,1) = 0 by A1,POWER:51; hence thesis by A1,A2,POWER:57; end; theorem Th2: for a,b being Real st 1 < a & 1 < b holds 0 < log(a,b) proof let a,b be Real; assume that A1: 1 < a and A2: 1 < b; log(a,1) = 0 by A1,POWER:51; hence thesis by A1,A2,POWER:57; end; theorem Th3: for p being FinSequence,i being Nat st i in dom p holds i = 1 or 1 < i proof let p be FinSequence, i be Nat; assume i in dom p; then i in Seg len p by FINSEQ_1:def 3; then i = 1 or ... or i = len p by FINSEQ_1:91; hence thesis by XXREAL_0:1; end; theorem Th4: for p being FinSequence,i being Nat st i in dom p holds i = len p or i < len p proof let p be FinSequence, i be Nat; assume i in dom p; then i in Seg len p by FINSEQ_1:def 3; then i = 1 or ... or i = len p by FINSEQ_1:91; hence thesis by XXREAL_0:1; end; theorem Th5: for x being object holds product <*{x}*> = {<*x*>} proof let x be object; the set of all <*y*> where y is Element of {x} = {<*x*>} proof set SA = the set of all <*y*> where y is Element of {x}; A1: for t be object st t in SA holds t in {<*x*>} proof let t be object; assume t in the set of all <*y*> where y is Element of {x}; then consider y0 be Element of {x} such that A2: t = <*y0*>; t = <*x*> by A2,TARSKI:def 1; hence thesis by TARSKI:def 1; end; for t be object st t in {<*x*>} holds t in SA proof let t be object; assume t in {<*x*>}; then t = <*x*> & x is Element of {x} by TARSKI:def 1; hence thesis; end; then SA c= {<*x*>} & {<*x*>} c= SA by A1; hence thesis; end; hence thesis by SRINGS_4:24; end; theorem Th6: for x being Element of REAL 1 holds ex rx being Real st x = <*rx*> proof let x be Element of REAL 1; x is Element of TOP-REAL 1 by EUCLID:22; then consider rx be Real such that A1: x = <*rx*> by JORDAN2B:20; thus thesis by A1; end; theorem Th7: for a being Real holds <*a*> is Point of Euclid 1 proof let a be Real; reconsider ra = <*a*> as FinSequence of REAL; dom ra = Seg 1 by FINSEQ_1:def 8; then len ra = 1 by FINSEQ_1:def 3; hence thesis by TOPREAL3:45; end; theorem Th8: for a,b being Real st a <= b holds a <= (a+b)/2 <= b proof let a,b be Real; assume A1: a <= b; 2 * a = a + a; then 2 * a <= a + b by A1,XREAL_1:7; then 2 * a / 2 <= (a + b)/2 by XREAL_1:72; hence a <= (a + b)/2; a+b <= b + b by A1,XREAL_1:7; then (a+b)/2 <= 2 * b /2 by XREAL_1:72; hence thesis; end; theorem for a,b,c being Real st a <= b & b < c holds a < (b+c)/2 proof let a,b,c be Real; assume that A1: a <= b and A2: b < c; A3: a + b < b + c by A1,A2,XREAL_1:8; a + a <= a + b by A1,XREAL_1:7; then 2 * a < b + c by A3,XXREAL_0:2; then 2 * a / 2 < (b + c) / 2 by XREAL_1:74; hence thesis; end; theorem for a,b being Real st a < b holds (a+b)/2 < b proof let a,b be Real; assume a < b; then a + b < b + b by XREAL_1:8; then (a+b)/2 < 2 * b / 2 by XREAL_1:74; hence thesis; end; theorem for a,b being Real st a <= b holds [.a,b.] is non empty compact Subset of REAL by XXREAL_1:30; theorem for f being FinSequence st 2 <= len f holds (f /^ 1 ).len(f /^ 1) = f.len(f) proof let f be FinSequence; assume A1: 2 <= len f; set g = f /^ 1; A2: 1 <= len f by A1,XXREAL_0:2; then A3: len g + 1 = len f - 1 + 1 by RFINSEQ:def 1 .= len f; then 2 - 1 <= len g + 1 - 1 by A1,XREAL_1:13; then len g in Seg len g by FINSEQ_1:3; then len g in dom g by FINSEQ_1:def 3; hence thesis by A3,A2,RFINSEQ:def 1; end; 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 Th9: 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 .|| proof let x,y being Element of Euclid n,g,h being Point of REAL-NS n; assume A1: x = g & y = h; x in Euclid n & y in Euclid n; then x in TOP-REAL n & y in TOP-REAL n by EUCLID:67; then reconsider rx = x, ry = y as Element of REAL n by EUCLID:22; A2: Euclid n = MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7; reconsider g1 = g, h1 = h as Element of REAL n by REAL_NS1:def 4; reconsider z1 = g1 - h1 as Element of REAL n; ||.g - h.|| = (the normF of (REAL-NS n)).(g1 - h1) by REAL_NS1:5 .= (Euclid_norm n).z1 by REAL_NS1:def 4 .= |.z1.| by REAL_NS1:def 3; hence thesis by A1,A2,EUCLID:def 6; end; theorem Th10: s1 is sequence of REAL-NS n & s2 is sequence of Euclid n proof thus s1 is sequence of REAL-NS n proof s1 is sequence of the carrier of TOP-REAL n by EUCLID:67; then s1 is sequence of REAL n by EUCLID:22; hence thesis by REAL_NS1:def 4; end; thus s2 is sequence of Euclid n proof s2 is sequence of REAL n by REAL_NS1:def 4; then s2 is sequence of TOP-REAL n by EUCLID:22; hence thesis by EUCLID:67; end; end; theorem Th11: s1 = s2 implies (s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm) proof assume A1: s1 = s2; A2: now assume A3: s1 is Cauchy; now let r be Real; assume r > 0; then consider p be Nat such that A4: for n,m being Nat st p <= n & p <= m holds dist(s1.n,s1.m) < r by A3; take p; hereby let n0,m0 be Nat; assume A5: n0 >= p & m0 >= p; dist(s1.n0,s1.m0) = ||.s2.n0-s2.m0.|| by A1,Th9; hence ||.s2.n0-s2.m0.|| < r by A5,A4; end; end; hence s2 is Cauchy_sequence_by_Norm by RSSPACE3:8; end; now assume A9: s2 is Cauchy_sequence_by_Norm; hereby let r be Real; assume r > 0; then consider k be Nat such that A10: for n, m being Nat st n >= k & m >= k holds ||. s2.n - s2.m .|| < r by A9,RSSPACE3:8; hereby take k; hereby let n0,m0 be Nat; assume A11: k <= n0 & k <= m0; ||.s2.n0-s2.m0.|| = dist(s1.n0,s1.m0) by A1,Th9; hence dist(s1.n0,s1.m0) < r by A11,A10; end; end; hence ex p be Nat st for n,m be Nat st p <= n & p <= m holds dist(s1.n,s1.m) < r; end; hence s1 is Cauchy; end; hence thesis by A2; end; theorem Th12: s1 = s2 implies (s1 is convergent iff s2 is convergent) proof assume A1: s1 = s2; hereby assume s1 is convergent; then consider x be Element of Euclid n such that A2: for r being Real st r > 0 holds ex n0 being Nat st for m being Nat st n0 <= m holds dist(s1.m,x) < r; x is Element of TOP-REAL n by EUCLID:67; then x is Element of REAL n by EUCLID:22; then reconsider g = x as Point of REAL-NS n by REAL_NS1:def 4; now take g; hereby let r be Real; assume 0 < r; then consider n0 be Nat such that A3: for m being Nat st n0 <= m holds dist(s1.m,x) < r by A2; hereby take n0; hereby let n1 be Nat; assume n0 <= n1; then dist(s1.n1,x) < r & s1.n1 = s2.n1 by A1,A3; hence ||.s2.n1 - g .|| < r by Th9; end; end; end; end; hence s2 is convergent; end; assume s2 is convergent; then consider g be Point of REAL-NS n such that A4: for r be Real st 0 < r holds ex m be Nat st for n0 be Nat st m <= n0 holds ||.(s2.n0)-g.|| < r; g is Element of REAL n by REAL_NS1:def 4; then g is Element of TOP-REAL n by EUCLID:22; then reconsider x = g as Element of Euclid n by EUCLID:67; now take x; hereby let r be Real; assume r > 0; then consider m0 be Nat such that A5: for n0 be Nat st m0 <= n0 holds ||.(s2.n0)-g.|| < r by A4; hereby take m0; hereby let m be Nat; assume m0 <= m; then ||. s2.m - g .|| < r & s2.m = s1.m by A1,A5; hence dist(s1.m,x) < r by Th9; end; end; end; end; hence s1 is convergent; end; theorem Th13: for S2 being sequence of Euclid n st S2 is Cauchy holds S2 is convergent proof let S2 be sequence of Euclid n; assume A1: S2 is Cauchy; reconsider S2NS = S2 as sequence of REAL-NS n by Th10; S2NS is Cauchy_sequence_by_Norm by A1,Th11; then S2NS is convergent by LOPBAN_1:def 15; hence S2 is convergent by Th12; end; theorem Euclid n is complete by Th13; begin :: Euclid n is complete - Proof Version 2 theorem Th14: distance_by_norm_of (REAL-NS n) = Pitag_dist n proof the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then reconsider d1 = distance_by_norm_of(REAL-NS n) as Function of [:REAL n,REAL n:],REAL; now let x,y be set; assume A1: x in REAL n & y in REAL n; then x is Element of TOP-REAL n & y is Element of TOP-REAL n by EUCLID:22; then reconsider px = x,py = y as Element of Euclid n by EUCLID:67; reconsider g = x,h = y as Point of REAL-NS n by A1,REAL_NS1:def 4; Euclid n = MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7; hence (Pitag_dist n).(x,y) = dist(px,py) .= ||.g-h.|| by Th9 .= d1.(x,y) by NORMSP_2:def 1; end; hence thesis by BINOP_1:def 21; end; theorem Th15: MetricSpaceNorm(REAL-NS n) = Euclid n proof set MS = MetricSpaceNorm(REAL-NS n); A1: MS = MetrStruct(# the carrier of (REAL-NS n),distance_by_norm_of (REAL-NS n) #) by NORMSP_2:def 2; then A2: the carrier of MS = REAL n by REAL_NS1:def 4; Euclid n = MetrStruct(# REAL n,Pitag_dist n #) by EUCLID:def 7; hence thesis by A1,A2,Th14; end; theorem Euclid n is complete proof MetricSpaceNorm(REAL-NS n) = Euclid n by Th15; hence thesis; end; registration let n be Nat; cluster Euclid n -> complete; coherence by Th13; end; begin :: The Nested Intervals Theorem (1-dimensional Euclidean space) definition let a,b being Real_Sequence; func IntervalSequence(a,b) -> SetSequence of REAL 1 means :Def1: for i being Nat holds it.i = product <* [.a.i,b.i.] *>; existence proof defpred P[object,object] means \$2 = product <* [. a.\$1, b.\$1 .] *>; A1: for x being object st x in NAT ex y being object st y in bool REAL 1 & P[x,y] proof let x be object; assume x in NAT; set y = product <* [.a.x,b.x.] *>; take y; product <* [.a.x,b.x.] *> c= REAL 1 proof let t be object; assume t in product <* [.a.x,b.x.] *>; then consider f be Function such that A2: t = f and A3: dom f = dom <* [.a.x,b.x.] *> and A4: for i be object st i in dom <* [.a.x,b.x.] *> holds f.i in (<* [.a.x,b.x.] *>).i by CARD_3:def 5; A5: dom <* [.a.x,b.x.] *> = Seg 1 by FINSEQ_1:def 8; A6: dom f = Seg 1 by A3,FINSEQ_1:def 8; rng f c= REAL proof let u be object; assume u in rng f; then consider t be object such that A7: t in dom f and A8: u = f.t by FUNCT_1:def 3; t in {1} by FINSEQ_1:2,A7,A3,FINSEQ_1:def 8; then A9: t = 1 & 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1; u = f.1 & 1 in dom <*[.a.x,b.x.]*> by A7,A3,FINSEQ_1:2,TARSKI:def 1,A8,A5; then f.1 in (<*[.a.x,b.x.]*>).1 by A4; then u in [.a.x,b.x.] by A9,A8,FINSEQ_1:def 8; hence thesis; end; then t in Funcs(Seg 1,REAL) by A2,FUNCT_2:def 2,A6; then t in 1-tuples_on REAL by FINSEQ_2:93; hence t in REAL 1 by EUCLID:def 1; end; hence y in bool REAL 1; thus P[x,y]; end; ex f being Function of NAT,(bool(REAL 1)) st for x be object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A1); then consider f be Function of NAT,bool (REAL 1) such that A10: for x be object st x in NAT holds P[x,f.x]; now take f; for x be Nat holds P[x,f.x] by ORDINAL1:def 12,A10; hence ex f being Function of NAT,bool (REAL 1) st for x be Nat holds P[x,f.x]; end; hence thesis; end; uniqueness proof let f1,f2 being SetSequence of REAL 1 such that A11: for i be Nat holds f1.i = product <* [.a.i,b.i.] *> and A12: for i be Nat holds f2.i = product <* [.a.i,b.i.] *>; A17: dom f1 = NAT & dom f2 = NAT by FUNCT_2:def 1; for x be object st x in dom f1 holds f1.x = f2.x proof let x be object; assume x in dom f1; then f1.x = product <* [.a.x,b.x.] *> & f2.x = product <* [.a.x,b.x.] *> by A11,A12; hence thesis; end; hence f1 = f2 by A11,A12,A17; end; end; theorem Th16: for a,b being Real_Sequence, i being Nat holds IntervalSequence(a,b).i = product <* [.a.i,b.i.] *> proof let a,b be Real_Sequence, i be Nat; A1: for i be Nat holds IntervalSequence(a,b).i = product <* [.a.i,b.i.] *> by Def1; thus thesis by A1; end; theorem Th17: for a,b being Real_Sequence holds IntervalSequence(a,b) is SetSequence of Euclid 1 proof let a,b being Real_Sequence; REAL 1 = the carrier of TOP-REAL 1 by EUCLID:22 .= the carrier of Euclid 1 by EUCLID:67; hence thesis; end; theorem Th18: product <*REAL*> = REAL 1 proof now let x be object; assume x in product <*REAL*>; then consider g be Function such that A1: x = g and A2: dom g = dom <*REAL*> and A3: for j be object st j in dom <*REAL*> holds g.j in (<*REAL*>).j by CARD_3:def 5; A4: dom g = Seg 1 by A2,FINSEQ_1:def 8; rng g c= REAL proof let u be object; assume u in rng g; then consider t be object such that A5: t in dom g and A6: u = g.t by FUNCT_1:def 3; t in {1} by A5,FINSEQ_1:2,A2,FINSEQ_1:def 8; then A7: t = 1 & 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1; u = g.1 & 1 in dom <*REAL*> by A6,A7,FINSEQ_1:def 8; then g.1 in (<*REAL*>).1 by A3; hence thesis by A7,A6,FINSEQ_1:def 8; end; then x in Funcs(Seg 1,REAL) by A1,FUNCT_2:def 2,A4; then x in 1-tuples_on REAL by FINSEQ_2:93; hence x in REAL 1 by EUCLID:def 1; end; then A8: product <*REAL*> c= REAL 1; now let x be object; assume A9: x in REAL 1; then x in 1-tuples_on REAL by EUCLID:def 1; then A10: x in Funcs(Seg 1,REAL) by FINSEQ_2:93; reconsider g = x as Function by A9; now consider h be Function such that A11: h = g and A12: dom h = Seg 1 and A13: rng h c= REAL by A10,FUNCT_2:def 2; thus dom g = dom <*REAL*> by A11,A12,FINSEQ_1:def 8; hereby let j be object; assume A14: j in dom <*REAL*>; then A15: j in Seg 1 by FINSEQ_1:def 8; j in {1} by FINSEQ_1:2,A14,FINSEQ_1:def 8; then A16: j = 1 by TARSKI:def 1; g.j in REAL by A11,A13,A12,A15,FUNCT_1:3; hence g.j in <*REAL*>.j by A16,FINSEQ_1:def 8; end; hence for j be object st j in dom <*REAL*> holds g.j in <*REAL*>.j; end; hence x in product <*REAL*> by CARD_3:def 5; end; then REAL 1 c= product <*REAL*>; hence thesis by A8; end; theorem Th19: for a,b being Real, xa,xb being Point of Euclid 1 st xa = <*a*> & xb = <*b*> holds dist(xa,xb) = |.a - b.| proof let a,b be Real,xa,xb be Point of Euclid 1; assume that A1: xa = <*a*> and A2: xb = <*b*>; xa in Euclid 1 & xb in Euclid 1; then xa in TOP-REAL 1 & xb in TOP-REAL 1 by EUCLID:67; then reconsider ra = xa, rb = xb as Element of REAL 1 by EUCLID:22; A3: Euclid 1 = MetrStruct(#REAL 1,Pitag_dist 1#) by EUCLID:def 7; A4: ra = 1 |-> a by A1,FINSEQ_2:59; rb = 1 |-> b by A2,FINSEQ_2:59; then |.ra-rb.| = sqrt(1) * |.a-b.| by A4,TOPREALC:11 .= |.a - b.| by SQUARE_1:18; hence thesis by A3,EUCLID:def 6; end; theorem Th20: 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 proof let a,b be Real,S be Subset of Euclid 1; assume that A1: a <= b and A2: S = product <*[.a,b.]*>; set si = product <* [.a,b.] *>; reconsider si as Subset of Euclid 1 by A2; set r = b - a; for x,y be Point of Euclid 1 st x in si & y in si holds dist(x,y) <= b - a proof set r = b - a; per cases by A1,XREAL_1:48; suppose A3: r = 0; then A4: product <*[.a,b.]*> = product <* {a} *> by XXREAL_1:17 .= {<*a*>} by Th5; now set r = b - a; hereby let x,y be Point of Euclid 1; assume x in si & y in si; then A5: x = <*a*> & y = <*a*> by A4,TARSKI:def 1; Euclid 1 is Reflexive; hence dist(x,y) <= b - a by A3,A5,METRIC_1:def 2; end; end; hence for x,y be Point of Euclid 1 st x in si & y in si holds dist(x,y) <= b - a; end; suppose 0 < r; hereby let x,y be Point of Euclid 1; assume that A6: x in si and A7: y in si; consider gx be Function such that A8: x = gx and dom gx = dom <*[.a,b.]*> and A9: for j be object st j in dom <*[.a,b.]*> holds gx.j in <*[.a,b.]*>.j by A6,CARD_3:def 5; consider gy be Function such that A10: y = gy and dom gy = dom <*[.a,b.]*> and A11: for j be object st j in dom <*[.a,b.]*> holds gy.j in <*[.a,b.]*>.j by A7,CARD_3:def 5; x in Euclid 1 & y in Euclid 1; then x in TOP-REAL 1 & y in TOP-REAL 1 by EUCLID:67; then reconsider rx = x, ry = y as Element of REAL 1 by EUCLID:22; Euclid 1 = MetrStruct(#REAL 1,Pitag_dist 1#) by EUCLID:def 7; then A12: dist(x,y) = |.rx - ry.| by EUCLID:def 6; consider ux be Real such that A13: rx = <*ux*> by Th6; consider uy be Real such that A14: ry = <*uy*> by Th6; rx = 1|->ux & ry = 1|-> uy by A13,A14,FINSEQ_2:59; then A15: |.rx-ry.| = sqrt(1) * |.ux-uy.| by TOPREALC:11 .= |.ux - uy.| by SQUARE_1:18; 1 in Seg 1 by TARSKI:def 1,FINSEQ_1:2; then 1 in dom <*[.a,b.]*> by FINSEQ_1:def 8; then gx.1 in <*[.a,b.]*>.1 & gy.1 in <*[.a,b.]*>.1 by A9,A11; then gx.1 in [.a,b.] & gy.1 in [.a,b.] by FINSEQ_1:def 8; then ux in [.a,b.] & uy in [.a,b.] by A8,A10,A13,A14,FINSEQ_1:def 8; hence dist(x,y) <= r by A12,A15,UNIFORM1:12; end; end; end; hence thesis by A2; end; theorem Th21: for a,b being Real, S being Subset of Euclid 1 st a <= b & S = product<*[.a,b.]*> holds S is bounded proof let a,b be Real,S be Subset of Euclid 1; assume that A1: a <= b and A2: S = product <*[.a,b.]*>; set si = product <* [.a,b.] *>; reconsider si as Subset of Euclid 1 by A2; ex r be Real st 0 < r & for x,y be Point of Euclid 1 st x in si & y in si holds dist(x,y) <= r proof set r = b - a; per cases by A1,XREAL_1:48; suppose r = 0; then A3: product <*[.a,b.]*> = product <* {a} *> by XXREAL_1:17 .= {<*a*>} by Th5; now set r = 1; take r; thus 0 < r; hereby let x,y be Point of Euclid 1; assume x in si & y in si; then A4: x = <*a*> & y = <*a*> by A3,TARSKI:def 1; Euclid 1 is Reflexive; hence dist(x,y) <= r by A4,METRIC_1:def 2; end; end; hence ex r be Real st 0 < r & for x,y be Point of Euclid 1 st x in si & y in si holds dist(x,y) <= r; end; suppose A5: 0 < r; take r; thus 0 < r by A5; hereby let x,y be Point of Euclid 1; assume that A6: x in si and A7: y in si; consider gx be Function such that A8: x = gx and dom gx = dom <*[.a,b.]*> and A9: for j be object st j in dom <*[.a,b.]*> holds gx.j in <*[.a,b.]*>.j by A6,CARD_3:def 5; consider gy be Function such that A10: y = gy and dom gy = dom <*[.a,b.]*> and A11: for j be object st j in dom <*[.a,b.]*> holds gy.j in <*[.a,b.]*>.j by A7,CARD_3:def 5; x in Euclid 1 & y in Euclid 1; then x in TOP-REAL 1 & y in TOP-REAL 1 by EUCLID:67; then reconsider rx = x, ry = y as Element of REAL 1 by EUCLID:22; Euclid 1 = MetrStruct(#REAL 1,Pitag_dist 1#) by EUCLID:def 7; then A12: dist(x,y) = |.rx - ry.| by EUCLID:def 6; consider ux be Real such that A13: rx = <*ux*> by Th6; consider uy be Real such that A14: ry = <*uy*> by Th6; rx = 1|->ux & ry = 1|-> uy by A13,A14,FINSEQ_2:59; then A15: |.rx-ry.| = sqrt(1) * |.ux-uy.| by TOPREALC:11 .= |.ux - uy.| by SQUARE_1:18; 1 in Seg 1 by TARSKI:def 1,FINSEQ_1:2; then 1 in dom <*[.a,b.]*> by FINSEQ_1:def 8; then gx.1 in <*[.a,b.]*>.1 & gy.1 in <*[.a,b.]*>.1 by A9,A11; then gx.1 in [.a,b.] & gy.1 in [.a,b.] by FINSEQ_1:def 8; then ux in [.a,b.] & uy in [.a,b.] by A8,A10,A13,A14,FINSEQ_1:def 8; hence dist(x,y) <= r by UNIFORM1:12,A15,A12; end; end; end; hence thesis by A2; end; theorem Th22: 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 let a,b be Real_Sequence; assume A1: for i being Nat holds a.i <= b.i & a.i <= a.(i+1) & b.(i+1) <= b.i; reconsider s = IntervalSequence(a,b) as SetSequence of Euclid 1 by Th17; A2: s is non-empty proof assume not thesis; then consider i be object such that A3: i in dom s and A4: s.i = {}; product <* [.a.i,b.i.] *> = {} by A3,A4,Th16; then {} in rng <* [.a.i,b.i.] *> by CARD_3:26; then consider j be object such that A5: j in dom <* [.a.i,b.i.] *> and A6: (<* [.a.i,b.i.] *>).j = {} by FUNCT_1:def 3; j in {1} by FINSEQ_1:2,A5,FINSEQ_1:def 8; then (<* [.a.i,b.i.] *>).1 = {} by A6,TARSKI:def 1; then [.a.i,b.i.] is empty by FINSEQ_1:def 8; hence contradiction by A1,A3,XXREAL_1:30; end; A7: s is pointwise_bounded proof now let i be Nat; A8: s.i = product <* [.a.i,b.i.] *> by Th16; set si = product <* [.a.i,b.i.] *>; reconsider si as Subset of Euclid 1 by A8; ex r be Real st 0 < r & for x,y be Point of Euclid 1 st x in si & y in si holds dist(x,y) <= r proof set r = b.i - a.i; per cases by A1,XREAL_1:48; suppose r = 0; then A9: product <*[.a.i,b.i.]*> = product <* {a.i} *> by XXREAL_1:17 .= {<*a.i*>} by Th5; now set r = 1; take r; thus 0 < r; hereby let x,y be Point of Euclid 1; assume x in si & y in si; then A10: x = <*a.i*> & y = <*a.i*> by A9,TARSKI:def 1; Euclid 1 is Reflexive; hence dist(x,y) <= r by A10,METRIC_1:def 2; end; end; hence ex r be Real st 0 < r & for x,y be Point of Euclid 1 st x in si & y in si holds dist(x,y) <= r; end; suppose A11: 0 < r; take r; thus 0 < r by A11; hereby let x,y be Point of Euclid 1; assume that A12: x in si and A13: y in si; consider gx be Function such that A14: x = gx and dom gx = dom <*[.a.i,b.i.]*> and A15: for j be object st j in dom <*[.a.i,b.i.]*> holds gx.j in <*[.a.i,b.i.]*>.j by A12,CARD_3:def 5; consider gy be Function such that A16: y = gy and dom gy = dom <*[.a.i,b.i.]*> and A17: for j be object st j in dom <*[.a.i,b.i.]*> holds gy.j in <*[.a.i,b.i.]*>.j by A13,CARD_3:def 5; x in Euclid 1 & y in Euclid 1; then x in TOP-REAL 1 & y in TOP-REAL 1 by EUCLID:67; then reconsider rx = x, ry = y as Element of REAL 1 by EUCLID:22; Euclid 1 = MetrStruct(#REAL 1,Pitag_dist 1#) by EUCLID:def 7; then A18: dist(x,y) = |.rx - ry.| by EUCLID:def 6; consider ux be Real such that A19: rx = <*ux*> by Th6; consider uy be Real such that A20: ry = <*uy*> by Th6; rx = 1|->ux & ry = 1|-> uy by A19,A20,FINSEQ_2:59; then A21: |.rx-ry.| = sqrt(1) * |.ux-uy.| by TOPREALC:11 .= |.ux - uy.| by SQUARE_1:18; 1 in Seg 1 by TARSKI:def 1,FINSEQ_1:2; then 1 in dom <*[.a.i,b.i.]*> by FINSEQ_1:def 8; then gx.1 in <*[.a.i,b.i.]*>.1 & gy.1 in <*[.a.i,b.i.]*>.1 by A15,A17; then gx.1 in [.a.i,b.i.] & gy.1 in [.a.i,b.i.] by FINSEQ_1:def 8; then ux in [.a.i,b.i.] & uy in [.a.i,b.i.] by A14,A16,A19,A20,FINSEQ_1:def 8; hence dist(x,y) <= r by A21,A18,UNIFORM1:12; end; end; end; then si is bounded; hence s.i is bounded by Th16; end; hence thesis by COMPL_SP:def 1; end; s is closed proof for i be Nat holds s.i is closed proof let i be Nat; A22: s.i = product <* [.a.i,b.i.] *> by Th16; then reconsider si = product <* [.a.i,b.i.] *> as Subset of Euclid 1; A23: si`= product <* ].-infty,a.i.[ \/ ].b.i,+infty.[ *> proof si` = (the carrier of TOP-REAL 1) \si by EUCLID:67 .= REAL 1 \ product <*[.a.i,b.i.]*> by EUCLID:22 .= product <*REAL \ [.a.i,b.i.]*> by Th18,SRINGS_4:27; hence thesis by XXREAL_1:385; end; si` is open proof si` in Family_open_set Euclid 1 proof for x be Element of Euclid 1 st x in si` holds ex r be Real st r > 0 & Ball(x,r) c= si` proof let x be Element of Euclid 1; assume A24: x in si`; set A = ].-infty,a.i.[, B = ].b.i,+infty.[, f = <*A \/ B*>; consider g be Function such that A25: x = g and dom g = dom f and A26: for j be object st j in dom f holds g.j in f.j by A24,A23,CARD_3:def 5; 1 in Seg 1 by TARSKI:def 1,FINSEQ_1:2; then 1 in dom f by FINSEQ_1:def 8; then g.1 in f.1 by A26; then g.1 in A \/ B by FINSEQ_1:def 8; then per cases by XBOOLE_0:def 3; suppose A27: g.1 in A; then reconsider g1 = g.1 as ExtReal; now x is Element of TOP-REAL 1 by EUCLID:67; then x is Element of REAL 1 by EUCLID:22; then x in REAL 1; then x in 1-tuples_on REAL by EUCLID:def 1; then g in Funcs(Seg 1,REAL) by A25,FINSEQ_2:93; then consider h be Function such that A28: g = h and A29: dom h = Seg 1 and A30: rng h c= REAL by FUNCT_2:def 2; 1 in dom h by A29,TARSKI:def 1,FINSEQ_1:2; then h.1 in REAL by A30,FUNCT_1:3; then reconsider g1 as Real by A28; set r = |.g1 - a.i.|; take r; g1 - a.i <> 0 by A27,XXREAL_1:233; hence r > 0; thus Ball(x,r) c= si` proof let t be object; assume A31: t in Ball(x,r); then reconsider t1 = t as Element of Euclid 1; t1 in Euclid 1 & x in Euclid 1; then t1 in TOP-REAL 1 & x in TOP-REAL 1 by EUCLID:67; then reconsider rt1 = t1, rx = x as Element of REAL 1 by EUCLID:22; Euclid 1 = MetrStruct(#REAL 1,Pitag_dist 1#) by EUCLID:def 7; then A32: dist(x,t1) = |.rx - rt1.| by EUCLID:def 6; now take rt1; thus t = rt1; rt1 in REAL 1; then rt1 in 1-tuples_on REAL by EUCLID:def 1; then rt1 in Funcs(Seg 1,REAL) by FINSEQ_2:93; then consider h be Function such that A33: rt1 = h and A34: dom h = Seg 1 and rng h c= REAL by FUNCT_2:def 2; thus dom rt1 = dom f by A33,A34,FINSEQ_1:def 8; hereby let j be object; assume j in dom f; then A35: j in {1} by FINSEQ_1:2,FINSEQ_1:def 8; then A36: j = 1 by TARSKI:def 1; consider rt2 being Real such that A37: rt1 = <*rt2*> by Th6; A38: rt1.j = rt1.1 by A35,TARSKI:def 1 .= rt2 by A37,FINSEQ_1:def 8; consider ux be Real such that A39: rx = <*ux*> by Th6; rx = 1 |-> ux & rt1 = 1|-> rt2 by A37,A39,FINSEQ_2:59; then A40: |.rx-rt1.| = sqrt(1) * |.ux-rt2.| by TOPREALC:11 .= |.ux - rt2.| by SQUARE_1:18; rt2 in A \/ B proof A41: |.ux - rt2.| < |.g1 - a.i.| by A40,A32,A31,METRIC_1:11; g1 - a.i < 0 by A27,XXREAL_1:233,XREAL_1:49; then |.g1 - a.i.| = -(g1 - a.i) by ABSVALUE:def 1; then A42: |.g1 - rt2.| < a.i - g1 by A25,A39,FINSEQ_1:def 8,A41; per cases; suppose 0 <= g1 - rt2; then 0 + rt2 <= g1 -rt2 + rt2 by XREAL_1:7; then rt2 < a.i by A27,XXREAL_1:233,XXREAL_0:2; then rt2 in A or rt2 in B by XXREAL_1:233; hence thesis by XBOOLE_0:def 3; end; suppose g1 - rt2 < 0; then -(g1 - rt2) < a.i - g1 by A42,ABSVALUE:def 1; then rt2 - g1 + g1 < a.i - g1 + g1 by XREAL_1:8; then rt2 in A or rt2 in B by XXREAL_1:233; hence thesis by XBOOLE_0:def 3; end; end; hence rt1.j in f.j by A36,FINSEQ_1:def 8,A38; end; end; hence thesis by A23,CARD_3:def 5; end; end; hence thesis; end; suppose A43: g.1 in B; then reconsider g1 = g.1 as ExtReal; now x is Element of TOP-REAL 1 by EUCLID:67; then x is Element of REAL 1 by EUCLID:22; then x in REAL 1; then x in 1-tuples_on REAL by EUCLID:def 1; then g in Funcs(Seg 1,REAL) by A25,FINSEQ_2:93; then consider h be Function such that A44: g = h and A45: dom h = Seg 1 and A46: rng h c= REAL by FUNCT_2:def 2; 1 in Seg 1 by TARSKI:def 1,FINSEQ_1:2; then h.1 in REAL by A45,A46,FUNCT_1:3; then reconsider g1 as Real by A44; set r = |.g1 - b.i.|; take r; g1 - b.i <> 0 by A43,XXREAL_1:235; hence r > 0; thus Ball(x,r) c= si` proof let t be object; assume A46bis: t in Ball(x,r); then reconsider t1 = t as Element of Euclid 1; t1 in Euclid 1 & x in Euclid 1; then t1 in TOP-REAL 1 & x in TOP-REAL 1 by EUCLID:67; then reconsider rt1 = t1, rx = x as Element of REAL 1 by EUCLID:22; Euclid 1 = MetrStruct(#REAL 1,Pitag_dist 1#) by EUCLID:def 7; then A46ter: dist(x,t1) = |.rx - rt1.| by EUCLID:def 6; now take rt1; thus t = rt1; rt1 in REAL 1; then rt1 in 1-tuples_on REAL by EUCLID:def 1; then rt1 in Funcs(Seg 1,REAL) by FINSEQ_2:93; then consider h be Function such that A47: rt1 = h and A48: dom h = Seg 1 and rng h c= REAL by FUNCT_2:def 2; thus dom rt1 = dom f by A47,A48,FINSEQ_1:def 8; hereby let j be object; assume j in dom f; then A49: j in {1} by FINSEQ_1:2,FINSEQ_1:def 8; then A50: j = 1 by TARSKI:def 1; consider rt2 being Real such that A51: rt1 = <*rt2*> by Th6; A52: rt1.j = rt1.1 by A49,TARSKI:def 1 .= rt2 by A51,FINSEQ_1:def 8; consider ux be Real such that A53: rx = <*ux*> by Th6; rx = 1 |-> ux & rt1 = 1|-> rt2 by A51,A53,FINSEQ_2:59; then A54: |.rx-rt1.| = sqrt(1) * |.ux-rt2.| by TOPREALC:11 .= |.ux - rt2.| by SQUARE_1:18; rt2 in A \/ B proof ux = g1 by A25,A53,FINSEQ_1:def 8; then A55: |.g1 - rt2.| < |.g1 - b.i.| by A54,A46bis,A46ter,METRIC_1:11; 0 < g1 - b.i by A43,XXREAL_1:235,XREAL_1:50; then A56: |.g1 - rt2.| < g1 - b.i by A55,ABSVALUE:def 1; g1 - rt2 < g1 - b.i by A56,ABSVALUE:def 1; then g1 - rt2 - g1 < g1 - b.i - g1 by XREAL_1:14; then - rt2 < - b.i; then rt2 in A or rt2 in B by XREAL_1:24,XXREAL_1:235; hence thesis by XBOOLE_0:def 3; end; hence rt1.j in f.j by A52,A50,FINSEQ_1:def 8; end; end; hence thesis by A23,CARD_3:def 5; end; end; hence thesis; end; end; hence thesis by PCOMPS_1:def 4; end; hence thesis by COMPL_SP:def 3; end; hence thesis by A22,COMPL_SP:def 4; end; hence thesis by COMPL_SP:def 8; end; hence thesis by A2,A7; end; theorem Th23: 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 proof let a,b be Real_Sequence; assume A1: for i being Nat holds a.i <= b.i & a.i <= a.(i+1) & b.(i+1) <= b.i; now let n,m be Nat; assume A2: n <= m; product <* [.a.m,b.m.] *> c= product <*[.a.n,b.n.]*> proof let x be object; assume x in product <*[.a.m,b.m.]*>; then consider f be Function such that A3: x = f and A4: dom f = dom <* [.a.m,b.m.] *> and A5: for i be object st i in dom <* [.a.m,b.m.] *> holds f.i in (<* [.a.m,b.m.] *>).i by CARD_3:def 5; A6: dom <* [.a.m,b.m.] *> = Seg 1 by FINSEQ_1:def 8; now thus x = f by A3; thus dom f = dom <* [.a.n,b.n.] *> by A6,A4,FINSEQ_1:def 8; hereby let i be object; assume A7: i in dom <*[.a.n,b.n.]*>; then A8: i in dom <*[.a.m,b.m.]*> by A6,FINSEQ_1:def 8; i in Seg 1 by A7,FINSEQ_1:def 8; then A9: i = 1 by TARSKI:def 1,FINSEQ_1:2; then A10: (<*[.a.m,b.m.]*>).i = [.a.m,b.m.] by FINSEQ_1:def 8; A11: (<*[.a.n,b.n.]*>).i = [.a.n,b.n.] by A9,FINSEQ_1:def 8; A12: a is non-decreasing by A1; dom a = NAT by SEQ_1:1; then n in dom a & m in dom a by ORDINAL1:def 12; then A13: a.n <= a.m by A12,A2; A14: b is non-increasing by A1; dom b = NAT by SEQ_1:1;then n in dom b & m in dom b by ORDINAL1:def 12; then b.m <= b.n by A14,A2; then [.a.m,b.m.] c= [.a.n,b.n.] by A13,XXREAL_1:34; hence f.i in (<* [.a.n,b.n.] *>).i by A8,A5,A10,A11; end; end; hence thesis by CARD_3:def 5; end; then IntervalSequence(a,b).m c= product <*[.a.n,b.n.]*> by Th16; hence IntervalSequence(a,b).m c= IntervalSequence(a,b).n by Th16; end; hence thesis by PROB_1:def 4; end; theorem Th24: for a,b,x being Real st a <= x <= b holds <*x*> in product <*[.a,b.]*> proof let a,b,x be Real; assume A1: a <= x <= b; reconsider P = <*x*> as Point of Euclid 1 by Th7; set f = <*[.a,b.]*>; A2: dom f = Seg 1 by FINSEQ_1:def 8; ex g be Function st g = P & dom g = dom <*[.a,b.]*> & for y be object st y in dom <*[.a,b.]*> holds g.y in (<*[.a,b.]*>).y proof reconsider g = P as Function; now take g; thus g = P; thus dom g = dom f by A2,FINSEQ_1:def 8; hereby let y be object; assume y in dom f; then y in {1} by FINSEQ_1:def 8,FINSEQ_1:2; then A3: y = 1 by TARSKI:def 1; g.1 = x & f.1 = [.a,b.] by FINSEQ_1:def 8; hence g.y in f.y by A3,A1,XXREAL_1:1; end; end; hence thesis; end; hence thesis by CARD_3:def 5; end; theorem Th25: for a,b being Real, S being Subset of Euclid 1 st a <= b & S = product <*[.a,b.]*> holds diameter S = b - a proof let a,b be Real, S be Subset of Euclid 1; assume that A1: a <= b and A2: S = product <*[.a,b.]*>; set f = <*[.a,b.]*>; A3: S is bounded by A1,A2,Th21; A4: S is non empty by A1,A2,Th24; ((for x, y being Point of Euclid 1 st x in S & y in S holds dist (x,y) <= b - a) & (for s being Real st (for x, y being Point of Euclid 1 st x in S & y in S holds dist (x,y) <= s) holds b - a <= s)) proof thus for x, y being Point of Euclid 1 st x in S & y in S holds dist (x,y) <= b - a by A1,A2,Th20; thus for s being Real st ( for x, y being Point of Euclid 1 st x in S & y in S holds dist (x,y) <= s ) holds b - a <= s proof let s be Real; assume A5: for x, y being Point of Euclid 1 st x in S & y in S holds dist (x,y) <= s; assume A6: s < b - a; A7: <*a*> in S & <*b*> in S by A2,A1,Th24; reconsider sa = <*a*>, sb = <*b*> as Point of Euclid 1 by Th7; A8: dist(sa,sb) <= s by A5,A7; a - a <= b - a by A1,XREAL_1:9; then |.b-a.|= b - a by ABSVALUE:def 1; hence contradiction by A6,A8,Th19; end; end; hence thesis by A3,A4,TBSP_1:def 8; end; theorem Th26: 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 let a,b being Real_Sequence; assume that A1: for i be Nat holds a.i <= b.i and A2: a is non-decreasing and A3: b is non-increasing; now take r = b.0 + 1; hereby let n be Nat; reconsider n0 = n as ExtReal; 0 in NAT; then A4: 0 in dom b by SEQ_1:1; n in NAT by ORDINAL1:def 12; then n0 in dom b by SEQ_1:1; then A5: b.n0 <= b.0 by A4,A3; a.n <= b.n by A1; then a.n <= b.0 by A5,XXREAL_0:2; then a.n + 0 < b.0 +1 by XREAL_1:8; hence a.n < r; end; end; then A6: a is bounded_above by SEQ_2:def 3; now take r = a.0 - 1; hereby let n be Nat; reconsider n0 = n as ExtReal; 0 in NAT; then A7: 0 in dom a by SEQ_1:1; n in NAT by ORDINAL1:def 12; then n0 in dom a by SEQ_1:1; then A8: a.0 <= a.n0 by A7,A2; a.n <= b.n by A1; then a.0 <= b.n by A8,XXREAL_0:2; then a.0 - 1 < b.n - 0 by XREAL_1:15; hence r < b.n; end; end; then b is bounded_below by SEQ_2:def 4; hence thesis by A2,A3,A6; end; theorem Th27: 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 let a,b being Real_Sequence; assume that A1: a.0 <= b.0 and A2: for i be 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)); defpred P[object] means ex i be Nat st \$1 = i & a.i <= b.i; A3: P by A1; A4: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; then consider i be Nat such that k = i and A5: a.k <= b.k; ((a.(k+1) = a.k & b.(k+1) = (a.k+b.k)/2 ) or (a.(k+1) = (a.k + b.k)/2 & b.(k+1) = b.k)) by A2; hence thesis by A5,Th8; end; A6: for k be Nat holds P[k] from NAT_1:sch 2(A3,A4); hereby let k be Nat; ex i be Nat st i = k & a.i <= b.i by A6; hence a.k <= b.k; end; end; theorem Th28: 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 proof let a,b being Real_Sequence, S being SetSequence of (Euclid 1); assume that A1: a.0 <= b.0 and A2: S = IntervalSequence(a,b) and A3: 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); A4: for i being Nat holds a.i <= b.i & a.i <= a.(i+1) & b.(i+1) <= b.i proof let i be Nat; thus A6: a.i <= b.i by Th27,A1,A3; thus a.i <= a.(i+1) proof a.(i+1) = a.i or a.(i+1) = (a.i+b.i)/2 by A3; hence thesis by A6,Th8; end; thus b.(i+1) <= b.i proof b.(i+1) = b.i or b.(i+1) = (a.i+b.i)/2 by A3; hence thesis by A6,Th8; end; end; now let i be Nat; A7: IntervalSequence(a,b) is SetSequence of Euclid 1 by Th17; reconsider IntervalSequence1 = IntervalSequence(a,b).i as Subset of Euclid 1 by ORDINAL1:def 12,A7,FUNCT_2:5; S.i = product <* [.a.i,b.i.] *> by A2,Th16; then reconsider IntervalSequence2 = product <* [.a.i,b.i.] *> as Subset of Euclid 1; diameter(S.i) = diameter IntervalSequence2 by A2,Th16 .= b.i - a.i by A4,Th25; hence (diameter S).i = b.i - a.i by COMPL_SP:def 2; end; hence thesis by A4; end; theorem Th29: 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 proof let a,b being Real_Sequence, S being SetSequence of (Euclid 1); assume that A1: a.0 = b.0 and A2: S = IntervalSequence(a,b) and A3: 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); defpred P[Nat] means a.\$1 = a.0 & b.\$1 = b.0; A4: P; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A6: P[k]; (a.(k+1) = a.k & b.(k+1) = (a.k+b.k)/2) or (a.(k+1)=(a.k+b.k)/2 & b.(k+1) = b.k) by A3; hence thesis by A1,A6; end; A7: for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); now let i be Nat; thus A8: a.i = a.0 by A7; thus A9: b.i = b.0 by A7; (diameter S).i= b.i - a.i by A1,A2,A3,Th28; hence (diameter S).i = 0 by A1,A8,A9; end; hence thesis; end; theorem Th30: 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) proof let a,b be Real_Sequence; assume that A1: 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); defpred P[object] means ex i be Nat, r be Real st \$1 = i & r = 2|^i & r <> 0 & b.i - a.i <= (b.0 - a.0) / r; A2: P proof reconsider i0 = 0 as Nat; reconsider r0 = 2|^0 as Real; take i0; take r0; 2|^0 = 1 by NEWTON:4; hence thesis; end; A3: for k be Nat holds P[k] implies P[k+1] proof let k be Nat; assume P[k]; then consider i1 be Nat, r1 be Real such that A4: k = i1 and A5: r1 = 2|^i1 and r1 <> 0 and A6: b.i1 - a.i1 <= (b.0 - a.0) / r1; reconsider i0 = k+1 as Nat; reconsider r0 = 2|^(k+1) as Real; A7: r0 <> 0 by NEWTON:87; b.i0 - a.i0 <= (b.0 - a.0) /r0 proof A8: (a.(k+1) = a.k & b.(k+1) = (a.k+b.k)/2 ) or (a.(k+1) = (a.k + b.k)/2 & b.(k+1) = b.k) by A1; A9: (b.i1-a.i1)/2 <= ((b.0-a.0)/r1)/2 by A6,XREAL_1:72; r1 * 2 = r0 by A4,A5,NEWTON:6; hence thesis by A8,A4,XCMPLX_1:78,A9; end; hence thesis by A7; end; A10: for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); let i be Nat, r be Real; assume that A11: r = 2 |^i and r <> 0; consider i0 be Nat, r0 be Real such that A12: i = i0 and A13: r0 = 2|^i0 & r0 <> 0 & b.i0 - a.i0 <= (b.0 - a.0) / r0 by A10; thus b.i - a.i <= (b.0 - a.0) / r by A11,A12,A13; end; theorem Th31: 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 proof let a,b being Real_Sequence, S being SetSequence of (Euclid 1); assume that A1: a.0 <= b.0 and A2: S = IntervalSequence(a,b) and A3: (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))); per cases by A1,XXREAL_0:1; suppose A4: a.0 = b.0; for x,y be object st x in dom (diameter S) & y in dom (diameter S) holds (diameter S).x = (diameter S).y proof let x,y be object; assume that A5: x in dom (diameter S) and A6: y in dom (diameter S); (diameter S).x = 0 & (diameter S).y = 0 by A5,A6,A4,A2,A3,Th29; hence thesis; end; then A7: diameter S is constant; hence diameter S is convergent; lim diameter S = (diameter S).0 by A7,SEQ_4:26; hence lim diameter S = 0 by A4,A2,A3,Th29; end; suppose a.0 < b.0; then A8: a.0 - a.0 < b.0 - a.0 by XREAL_1:14; A9: diameter S = b + (- a) proof now let i be Nat; (-a). i = - (a.i) by SEQ_1:10; then b.i - a.i = b.i + (-a).i; hence (diameter S).i = b.i + (-a).i by A1,A2,A3,Th28; end; hence thesis by SEQ_1:7; end; reconsider S2 = diameter S as Real_Sequence; A10: (for i be Nat holds a.i <= b.i) by A1,A3,Th27; A11: a is non-decreasing by A1,A2,A3,Th28; b is non-increasing by A1,A2,A3,Th28; then A12: a is convergent & b is convergent by A10,A11,Th26; lim diameter S = 0 proof for p be Real st 0

0 by NEWTON:83; then A28: |.S2.m - 0.| <= (b.0-a.0)/r by A27,Th30,A3; (b.0-a.0)/(2 to_power m) < p by A24,A25; hence |.S2.m - 0.| < p by A28,XXREAL_0:2; end; end; hence thesis; end; hence thesis by A12,A9,SEQ_2:def 7; end; hence thesis by A12,A9; end; end; theorem Th32: 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 proof let a,b be Real_Sequence; assume that A1: a.0 <= b.0 and A2: 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)); IntervalSequence(a,b) is SetSequence of Euclid 1 by Th17; then A3: for i being Nat holds a.i <= b.i & a.i <= a.(i+1) & b.(i+1) <= b.i by A1,A2,Th28; reconsider S = IntervalSequence(a,b) as non-empty pointwise_bounded closed SetSequence of (Euclid 1) by A3,Th22; A4: S is non-ascending by A3,Th23; lim diameter S = 0 by A1,A2,Th31; then meet S is non empty by A4,COMPL_SP:10; hence thesis; end; theorem 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 proof let r be Real, a,b be Real_Sequence; assume that A1: 0 < r and A2: a.0 <= b.0 and A3: 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)); meet IntervalSequence(a,b) is non empty by A2,A3,Th32; then consider y be object such that A4: y in meet IntervalSequence(a,b); A5: y in meet rng IntervalSequence(a,b) by A4,FUNCT_6:def 4; A6: dom IntervalSequence(a,b) = NAT by FUNCT_2:def 1; A7: for i be Nat holds IntervalSequence(a,b).i = product <* [.a.i,b.i.] *> by Def1; IntervalSequence(a,b).0 in rng IntervalSequence(a,b) by A6,FUNCT_1:3; then y in IntervalSequence(a,b).0 by A5,SETFAM_1:def 1; then A8: y in product <* [.a.0,b.0.] *> by Th16; then A9: y in IntervalSequence(a,b).0 by A7; consider g be Function such that A10: y = g and dom g = dom <*[.a.0,b.0.]*> and for t be object st t in dom <*[.a.0,b.0.]*> holds g.t in (<* [.a.0,b.0.] *>).t by A8,CARD_3:def 5; y is Element of TOP-REAL 1 by A9,EUCLID:22; then consider c be Real such that A11: y = <*c*> by JORDAN2B:20; take c; A12: now let i be Nat; IntervalSequence(a,b).i in rng IntervalSequence(a,b) by A6,ORDINAL1:def 12,FUNCT_1:3; then y in IntervalSequence(a,b).i by A5,SETFAM_1:def 1; then y in product <* [.a.i,b.i.] *> by Th16; then consider h be Function such that A13: y = h and dom h = dom <*[.a.i,b.i.]*> and A14: for t be object st t in dom <*[.a.i,b.i.]*> holds h.t in (<* [.a.i,b.i.] *>).t by CARD_3:def 5; A15: dom <*[.a.i,b.i.]*> = Seg 1 by FINSEQ_1:def 8; 1 in Seg 1 by TARSKI:def 1,FINSEQ_1:2; then h.1 in (<* [.a.i,b.i.] *>).1 by A14,A15; then g.1 in [.a.i,b.i.] by A10,A13,FINSEQ_1:def 8; then c in [.a.i,b.i.] by A10,A11,FINSEQ_1:def 8; hence a.i <= c <= b.i by XXREAL_1:1; end; hence for j be Nat holds a.j <= c <= b.j; thus ex k be Nat st c - r < a.k & b.k < c + r proof A16: IntervalSequence(a,b) is SetSequence of Euclid 1 by Th17; then A17: for i being Nat holds a.i <= b.i & a.i <= a.(i+1) & b.(i+1) <= b.i by A2,A3,Th28; reconsider S = IntervalSequence(a,b) as non-empty pointwise_bounded closed SetSequence of (Euclid 1) by A17,Th22; A18: diameter S is convergent & lim diameter S = 0 by A2,A3,Th31; consider m0 be Nat such that A19: for l be Nat st m0 <= l holds |.(diameter S).l - 0.| < r by A1,A18,SEQ_2:def 7; a.m0 <= b.m0 by A16,A2,A3,Th28; then a.m0 - a.m0 <= b.m0 - a.m0 by XREAL_1:9; then |.b.m0 - a.m0.| = b.m0 - a.m0 by ABSVALUE:def 1; then |.(diameter S).m0 - 0.| = b.m0 - a.m0 by A2,A3,Th28; then A20: b.m0 - a.m0 < r by A19; c - a.m0 <= b.m0 - a.m0 by A12,XREAL_1:9; then A21: c - a.m0 < r by A20,XXREAL_0:2; take m0; c - a.m0 + a.m0 < r + a.m0 by A21,XREAL_1:8; then c - r < a.m0 + r - r by XREAL_1:9; hence c - r < a.m0; b.m0 - c <= b.m0 - a.m0 by A12,XREAL_1:10; then b.m0 -c < r by A20,XXREAL_0:2; then b.m0 - c + c < r + c by XREAL_1:8; hence b.m0 < c +r; end; end; begin :: Tagged division theorem Th33: for I being non empty closed_interval Subset of REAL ex a,b being Real st a <= b & I = [.a,b.] proof let I be non empty closed_interval Subset of REAL; ex a,b be Real st I = [.a,b.] by MEASURE5:def 3; hence thesis by XXREAL_1:29; end; theorem 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.] proof let I1, I2 being non empty closed_interval Subset of REAL; assume A1: upper_bound I1 = lower_bound I2; consider a1,b1 be Real such that A2: a1 <= b1 and A3: I1 = [.a1,b1.] by Th33; consider a2,b2 be Real such that A4: a2 <= b2 and A5: I2 = [.a2,b2.] by Th33; A6: upper_bound I1 = b1 by A2,A3,JORDAN5A:19; lower_bound I2 = a2 by A4,A5,JORDAN5A:19; hence thesis by A1,A2,A4,A3,A5,A6; end; definition let A being non empty closed_interval Subset of REAL, D being Division of A; func set_of_tagged_Division(D) -> Subset of REAL* means :Def2: 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 proof defpred P[object] means ex s be non empty non-decreasing FinSequence of REAL st \$1 = s & dom s = dom D & for i be Nat st i in dom s holds s.i in divset(D,i); consider S be set such that A1: for x being object holds x in S iff x in REAL* & P[x] from XBOOLE_0:sch 1; take S; thus S is Subset of REAL* proof S c= REAL* by A1; hence thesis; end; for x be object holds x in S iff ex s be non empty non-decreasing FinSequence of REAL st x = s & dom s = dom D & for i be Nat st i in dom s holds s.i in divset(D,i) proof let x be object; thus x in S implies ex s be non empty non-decreasing FinSequence of REAL st x = s & dom s = dom D & for i be Nat st i in dom s holds s.i in divset(D,i) by A1; given s be non empty non-decreasing FinSequence of REAL such that A2: x = s and A3: dom s = dom D and A4: for i be Nat st i in dom s holds s.i in divset(D,i); x in REAL* by A2,FINSEQ_1:def 11; hence x in S by A2,A3,A4,A1; end; hence thesis; end; uniqueness proof let TD1,TD2 be Subset of REAL* such that A1: for x be object holds x in TD1 iff ex s be non empty non-decreasing FinSequence of REAL st x = s & dom s = dom D & for i be Nat st i in dom s holds s.i in divset(D,i) and A2: for x be object holds x in TD2 iff ex s be non empty non-decreasing FinSequence of REAL st x = s & dom s = dom D & for i be Nat st i in dom s holds s.i in divset(D,i); for x be object st x in TD1 holds x in TD2 proof let x be object; assume x in TD1; then ex s be non empty non-decreasing FinSequence of REAL st x = s & dom s = dom D & for i be Nat st i in dom s holds s.i in divset(D,i) by A1; hence thesis by A2; end; then A3: TD1 c= TD2; for x be object st x in TD2 holds x in TD1 proof let x be object; assume x in TD2; then ex s be non empty non-decreasing FinSequence of REAL st x = s & dom s = dom D & for i be Nat st i in dom s holds s.i in divset(D,i) by A2; hence thesis by A1; end; then TD2 c= TD1; hence thesis by A3; end; end; theorem Th34: for A being non empty closed_interval Subset of REAL, D being Division of A holds D in set_of_tagged_Division(D) proof let A being non empty closed_interval Subset of REAL, D being Division of A; for i be Nat st i in dom D holds D.i in divset(D,i) proof let i be Nat; assume A1: i in dom D; consider a,b be Real such that A2: divset(D,i) = [.a,b.] by MEASURE5:def 3; a <= b by A2,XXREAL_1:29; then A3: upper_bound divset(D,i) = b & b in [.a,b.] by A2,JORDAN5A:19,XXREAL_1:1; per cases by A1,Th3; suppose i = 1; hence thesis by A3,A2,A1,INTEGRA1:def 4; end; suppose 1 < i; hence thesis by A3,A2,A1,INTEGRA1:def 4; end; end; hence thesis by Def2; end; theorem Th35: for a,b being Real, Iab being non empty closed_interval Subset of REAL st Iab = [.a,b.] holds <*b*> is Division of Iab proof let a,b being Real, Iab being non empty closed_interval Subset of REAL; assume A1: Iab = [.a,b.]; A2: a <= b by A1,XXREAL_1:29; thus <*b*> is Division of Iab proof set D = <*b*>; A3: rng D c= Iab proof let x be object; assume x in rng D; then x in {b} by FINSEQ_1:39; then x = b by TARSKI:def 1; hence thesis by A1,A2,XXREAL_1:1; end; D.(len D) = upper_bound Iab proof dom D = Seg 1 by FINSEQ_1:def 8; then D.(len D) = <*b*>.1 by FINSEQ_1:def 3 .= b by FINSEQ_1:def 8; hence thesis by A1,A2,JORDAN5A:19; end; hence thesis by A3,INTEGRA1:def 2; end; end; definition let I being non empty closed_interval Subset of REAL, jauge being positive-yielding Function of I,REAL; mode tagged_division of I,jauge means :Def3: ex D being Division of I, T being Element of set_of_tagged_Division(D) st it = [D,T]; existence proof consider a,b be Real such that A1: I = [.a,b.] by MEASURE5:def 3; A2: a <= b by A1,XXREAL_1:29; reconsider B = <*b*> as Division of I by A1,Th35; now thus dom <*b*> = dom B; hereby let i be Nat; assume A3: i in dom B; then A4: i in {1} by FINSEQ_1:2,FINSEQ_1:def 8; then A5: i = 1 by TARSKI:def 1; consider c,d be Real such that A6: divset(B,1) = [.c,d.] by MEASURE5:def 3; A7: c <= d by A6,XXREAL_1:29; 1 in dom B by A3,A4,TARSKI:def 1; then lower_bound divset(B,1) = lower_bound [.a,b.] & upper_bound divset(B,1) = B.1 by A1,INTEGRA1:def 4; then c = lower_bound [.a,b.] & d = B.1 by A7,A6,JORDAN5A:19; then A8: c = a & d = b by FINSEQ_1:def 8,A2,JORDAN5A:19; b in [.a,b.] by A2,XXREAL_1:1; hence <*b*>.i in divset(B,i) by A8,A6,A5,FINSEQ_1:def 8; end; end; then reconsider T = <*b*> as Element of set_of_tagged_Division(B) by Def2; take [B,T]; thus thesis; end; end; definition let I being non empty closed_interval Subset of REAL, jauge being positive-yielding Function of I,REAL, TD being tagged_division of I,jauge; attr TD is delta-fine means 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 Th36: for r being Real holds upper_bound {r} = r & lower_bound {r} = r proof let r be Real; thus upper_bound {r} = upper_bound [.r,r.] by XXREAL_1:17 .= r by JORDAN5A:19; thus lower_bound {r} = lower_bound [.r,r.] by XXREAL_1:17 .= r by JORDAN5A:19; end; theorem for r being Real holds vol {r} = 0 proof let r be Real; vol {r} = upper_bound {r} - lower_bound {r} by INTEGRA1:def 5 .= r - lower_bound {r} by Th36 .= r - r by Th36; hence thesis; end; theorem 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 by FUNCT_2:32; theorem 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.] proof let I be non empty closed_interval Subset of REAL, c be Real; assume A1: c in I; consider a,b be Real such that A2: a <= b and A3: I = [.a,b.] by Th33; A4: lower_bound(I) = a & upper_bound(I) = b by A2,A3,JORDAN5A:19; A5: a <= c <= b by A1,A3,XXREAL_1:1; hence [.lower_bound(I),c.] is non empty closed_interval Subset of REAL & [.c,upper_bound(I).] is non empty closed_interval Subset of REAL by A4,XXREAL_1:30,MEASURE5:def 3; upper_bound [.lower_bound(I),c.] = c by A4,A5,JORDAN5A:19; hence upper_bound [.lower_bound(I),c.] = lower_bound [.c,upper_bound(I).] by A4,A5,JORDAN5A:19; end; definition let Iac,Icb being non empty closed_interval Subset of REAL, Dac being Division of Iac, Dcb being Division of Icb; assume A1: upper_bound(Iac) <= lower_bound(Icb); func Dac (#) Dcb -> non empty increasing FinSequence of REAL equals :Def4: Dac ^ Dcb if Dcb.1 <> upper_bound(Iac) otherwise Dac ^ (Dcb/^1); correctness proof Z1: now assume A2: Dcb.1 <> upper_bound(Iac); A3: Dac.len(Dac) = upper_bound Iac by INTEGRA1:def 2; A4: Dac.len(Dac) <= lower_bound(Icb) by A1,INTEGRA1:def 2; A5: rng Dcb c= Icb by INTEGRA1:def 2; rng Dcb <> {}; then 1 in dom Dcb by FINSEQ_3:32; then A6: Dcb.1 in Icb by A5,FUNCT_1:3; consider c,b be Real such that A7: Icb = [.c,b.] by MEASURE5:def 3; c <= b by A7,XXREAL_1:29; then lower_bound(Icb) = c by A7,JORDAN5A:19; then lower_bound(Icb) <= Dcb.1 by A6,A7,XXREAL_1:1; then Dac.len(Dac) <= Dcb.1 by A4,XXREAL_0:2; then Dac.len(Dac) < Dcb.1 by A3,A2,XXREAL_0:1; hence Dac ^ Dcb is non empty increasing FinSequence of REAL by Th1; end; now assume A8: Dcb.1 = upper_bound(Iac); now assume A9: not Dcb/^1 is empty; then A10: rng (Dcb/^1) <> {}; rng Dcb <> {}; then A11: 1 in dom Dcb by FINSEQ_3:32; then 1 in Seg len Dcb by FINSEQ_1:def 3; then A12: 1 <= len Dcb by FINSEQ_1:1; then reconsider D2 = Dcb/^1 as non empty increasing FinSequence of REAL by A9,INTEGRA1:34; A13: Dac.len(Dac) = upper_bound Iac by INTEGRA1:def 2; 1 in dom (Dcb/^1) by A10,FINSEQ_3:32; then A14: (Dcb/^1).1 = Dcb.(1+1) by A12,RFINSEQ:def 1; 1 in dom (Dcb/^1) by A10,FINSEQ_3:32; then (1+1) in dom Dcb by FINSEQ_5:26; then upper_bound Iac < D2.1 by A8,A14,A11,VALUED_0:def 13; hence Dac ^ (Dcb/^1) is non empty increasing FinSequence of REAL by A13,Th1; end; hence Dac ^ (Dcb/^1) is non empty increasing FinSequence of REAL by FINSEQ_1:34; end; hence thesis by Z1; end; end; theorem 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 proof let Iac,Icb being non empty closed_interval Subset of REAL, Dac being Division of Iac, Dcb being Division of Icb; assume that A1: upper_bound(Iac) = lower_bound(Icb) and A2: len Dcb = 1 and A3: Dcb.1 = lower_bound(Icb); len (Dcb/^1) = len Dcb - 1 by A2,RFINSEQ:def 1; then Dcb/^1 = {} by A2; then Dac ^ (Dcb/^1) = Dac by FINSEQ_1:34; hence thesis by A1,A3,Def4; end; theorem Th37: 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 let I1,I2,I being non empty closed_interval Subset of REAL such that A1: upper_bound(I1) <= lower_bound(I2) and A2: lower_bound(I) <= lower_bound(I1) and A3: upper_bound(I2) <= upper_bound(I); consider a1,b1 be Real such that A4: I1 = [.a1,b1.] by MEASURE5:def 3; A5: a1 <= b1 by A4,XXREAL_1:29; then A6: lower_bound I1 = a1 & upper_bound I1 = b1 by A4,JORDAN5A:19; consider a2,b2 be Real such that A7: I2 = [.a2,b2.] by MEASURE5:def 3; A8: a2 <= b2 by A7,XXREAL_1:29; A9: lower_bound(I) <= a1 & b2 <= upper_bound(I) by A2,A3,A5,A4,JORDAN5A:19,A8,A7; A10: b1 <= a2 by A6,A1,A8,A7,JORDAN5A:19; consider a3,b3 be Real such that A11: I = [.a3,b3.] by MEASURE5:def 3; a3 <= b3 by A11,XXREAL_1:29; then A12: lower_bound I = a3 & upper_bound I = b3 by A11,JORDAN5A:19; now let x be object; assume A13: x in I1 \/ I2; then reconsider x1 = x as Real; per cases by A13,XBOOLE_0:def 3; suppose x in I1; then a1 <= x1 <= b1 by A4,XXREAL_1:1; then a1 <= x1 <= a2 by A10,XXREAL_0:2; then a1 <= x1 <= b2 by A8,XXREAL_0:2; then lower_bound I <= x1 <= upper_bound I by A9,XXREAL_0:2; hence x in I by A12,A11,XXREAL_1:1; end; suppose x in I2; then a2 <= x1 <= b2 by A7,XXREAL_1:1; then b1 <= x1 <= b2 by A10,XXREAL_0:2; then a1 <= x1 <= b2 by A5,XXREAL_0:2; then lower_bound I <= x1 <= upper_bound I by A9,XXREAL_0:2; hence x in I by A12,A11,XXREAL_1:1; end; end; hence thesis; end; theorem 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 proof let Iac,Icb,I being non empty closed_interval Subset of REAL, Dac being Division of Iac, Dcb being Division of Icb; assume that A1: upper_bound Iac <= lower_bound Icb and A2: I = [.lower_bound Iac,upper_bound Icb .]; lower_bound Iac <= upper_bound Iac by BORSUK_4:28; then A3: lower_bound Iac <= lower_bound Icb by A1,XXREAL_0:2; lower_bound Icb <= upper_bound Icb by BORSUK_4:28; then A4: lower_bound Iac <= upper_bound Icb by A3,XXREAL_0:2; then lower_bound I = lower_bound Iac & upper_bound I = upper_bound Icb by A2,JORDAN5A:19; then A5: Iac \/ Icb c= I by A1,Th37; A6: rng Dac c= Iac by INTEGRA1:def 2; A7: rng Dcb c= Icb by INTEGRA1:def 2; rng Dcb <> {}; then 1 in dom Dcb by FINSEQ_3:32; then A8: 1 in Seg len Dcb by FINSEQ_1:def 3; then 1 <= len Dcb by FINSEQ_1:1; then A9: len Dac + 1 <= len Dac + len Dcb by XREAL_1:7; set Dacb = Dac (#) Dcb; per cases; suppose Dcb.1 <> upper_bound(Iac); then A10: Dacb = Dac ^ Dcb by A1,Def4; rng Dacb = rng Dac \/ rng Dcb by A10,FINSEQ_1:31; then rng Dacb c= Iac \/ Icb by A6,A7,XBOOLE_1:13; then A11: rng Dacb c= I by A5; len (Dacb) = len Dac + len Dcb by A10,FINSEQ_1:22; then Dacb.len(Dacb) = Dcb.(len Dac + len Dcb - len Dac) by A9,A10,FINSEQ_1:23 .= upper_bound Icb by INTEGRA1:def 2 .= upper_bound I by A4,A2,JORDAN5A:19; hence thesis by A11,INTEGRA1:def 2; end; suppose A12: Dcb.1 = upper_bound(Iac); then A13: Dacb = Dac ^ (Dcb/^1) by A1,Def4; then A14: rng Dacb c= rng Dac \/ rng (Dcb/^1) by FINSEQ_1:31; rng (Dcb/^1) c= rng Dcb by FINSEQ_5:33; then A15: rng Dac \/ rng (Dcb/^1) c= rng Dac \/ rng Dcb by XBOOLE_1:13; rng Dac \/ rng Dcb c= Iac \/ Icb by A6,A7,XBOOLE_1:13; then rng Dacb c= Iac \/ Icb by A14,A15; then A16: rng Dacb c= I by A5; A17: len (Dacb) = len Dac + len (Dcb/^1) by A13,FINSEQ_1:22; A18: 1 <= len Dcb by A8,FINSEQ_1:1; then A18bis: len (Dcb/^1) = len Dcb - 1 by RFINSEQ:def 1; per cases; suppose A19: len Dcb = 1; then Dcb/^1 is empty by FINSEQ_5:32; then Dacb = Dac by A13,FINSEQ_1:34; then Dacb.(len Dacb) = Dcb.len Dcb by A12,A19,INTEGRA1:def 2 .= upper_bound Icb by INTEGRA1:def 2 .= upper_bound I by A4,A2,JORDAN5A:19; hence thesis by A16,INTEGRA1:def 2; end; suppose len Dcb <> 1; then A20: 2 - 1 <= len Dcb - 1 by NAT_1:23,XREAL_1:9; A21: Seg len(Dcb/^1) = dom (Dcb/^1) by FINSEQ_1:def 3; A22: len (Dcb/^1) = len Dcb - 1 by A18,RFINSEQ:def 1; 1 <= len (Dcb/^1) by A18,RFINSEQ:def 1,A20; then A23: len(Dcb/^1) in dom (Dcb/^1) by A21,FINSEQ_1:1; Dcb/^1 <> {} by A22,A20; then rng (Dcb/^1) <> {}; then 1 in dom (Dcb/^1) by FINSEQ_3:32; then 1 in Seg len (Dcb/^1) by FINSEQ_1:def 3; then 1 <= len (Dcb/^1) by FINSEQ_1:1; then len Dac + 1 <= len Dac +len (Dcb/^1) <= len Dac + len (Dcb/^1) by XREAL_1:7; then Dacb.len(Dacb) = (Dcb/^1).(len Dac + len (Dcb/^1) - len Dac) by A17,A13,FINSEQ_1:23 .= Dcb.(len(Dcb/^1) + 1) by A18,RFINSEQ:def 1,A23 .= upper_bound Icb by A18bis,INTEGRA1:def 2 .= upper_bound I by A4,A2,JORDAN5A:19; hence thesis by A16,INTEGRA1:def 2; end; end; end; theorem for I being non empty closed_interval Subset of REAL, D being Division of I holds set_of_tagged_Division(D) is non empty by Th34; theorem Th38: 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 proof let s being non empty increasing FinSequence of REAL, r be Real; assume s.len s < r; then s.len s < <*r*>.1 by FINSEQ_1:def 8; hence thesis by Th1; end; theorem 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 proof let s1,s2 being non empty increasing FinSequence of REAL, r being Real; assume A1: s1.len s1 < r < s2.1; then reconsider s = s1 ^ <*r*> as non empty increasing FinSequence of REAL by Th38; s.len s = s.(len s1 + 1) by FINSEQ_2:16 .= r by FINSEQ_1:42; hence thesis by A1,Th1; end; theorem 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 let I1,I2,I being non empty closed_interval Subset of REAL; assume that A1: upper_bound I1 = lower_bound I2 and A2: I = I1 \/ I2; A3: I1 = [.lower_bound I1,upper_bound I1.] by INTEGRA1:4; then A4: lower_bound I1 <= upper_bound I1 by XXREAL_1:29; A5: I2 = [.lower_bound I2,upper_bound I2.] by INTEGRA1:4; then A6: lower_bound I2 <= upper_bound I2 by XXREAL_1:29; A7: I = [.lower_bound I1,upper_bound I2.] by A2,A3,A5,A1,A4,A6,XXREAL_1:165; A8: I = [.lower_bound I,upper_bound I.] by INTEGRA1:4; then lower_bound I <= upper_bound I by XXREAL_1:29; hence thesis by A7,A8,XXREAL_1:66; end; theorem 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.] proof let I be non empty closed_interval Subset of REAL, D be Division of I; rng D <> {}; then 1 in dom D by FINSEQ_3:32; then lower_bound divset(D,1) = lower_bound I & upper_bound divset(D,1) = D.1 by INTEGRA1:def 4; hence divset(D,1) = [.lower_bound I,D.1.] by INTEGRA1:4; thus for j be Nat st j in dom D & j <> 1 holds divset(D,j)=[.D.(j-1),D.j.] proof let j be Nat; assume that A1: j in dom D and A2: j <> 1; lower_bound divset(D,j) = D.(j-1) & upper_bound divset(D,j) = D.j by A1,A2,INTEGRA1:def 4; hence thesis by INTEGRA1:4; end; end; theorem for r being Real, p,q being FinSequence of REAL holds len (p ^ <*r*> ^ q) = len p + len q + 1 proof let r be Real, p,q be FinSequence of REAL; A1: len (p ^ <*r*> ^ q) = len( p ^ <*r*>) + len q by FINSEQ_1:22 .= len p + len <*r*> + len q by FINSEQ_1:22; len <*r*> = 1 by FINSEQ_1:40; hence thesis by A1; end; theorem for I being non empty closed_interval Subset of REAL, D being Division of I, T be Element of set_of_tagged_Division(D) holds T is non empty proof let I be non empty closed_interval Subset of REAL, D be Division of I, T being Element of set_of_tagged_Division(D); set_of_tagged_Division(D) is non empty by Th34; then consider s being non empty non-decreasing FinSequence of REAL such that A1: T = s and dom s = dom D and for i be Nat st i in dom s holds s.i in divset(D,i) by Def2; thus thesis by A1; end; theorem 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 proof let I being non empty closed_interval Subset of REAL, D being Division of I, T being Element of set_of_tagged_Division(D); set_of_tagged_Division(D) is non empty by Th34; then ex s be non empty non-decreasing FinSequence of REAL st T = s & dom s = dom D & for i be Nat st i in dom s holds s.i in divset(D,i) by Def2; hence thesis by FINSEQ_1:def 4; end; definition let I being non empty closed_interval Subset of REAL, jauge being positive-yielding Function of I,REAL, TD being tagged_division of I,jauge; func division_of(TD) -> Division of I means ex D being Division of I, T being Element of set_of_tagged_Division(D) st it = D & TD = [D,T]; existence proof consider D be Division of I, T be Element of set_of_tagged_Division(D) such that A1: TD = [D,T] by Def3; take D; thus thesis by A1; end; uniqueness by XTUPLE_0:1; end; begin :: Examples of Division reserve r,s for Real; theorem 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) proof let jauge be Function of [.r,s.],].0,+infty.[; assume A1: r <= s; set A = the set of all ]. x - jauge.x, x + jauge.x .[ /\ [.r,s.] where x is Element of [.r,s.]; A c= bool [.r,s.] proof let t be object; assume t in A; then consider x0 be Element of [.r,s.] such that A2: t = ]. x0 - jauge.x0,x0 + jauge.x0 .[ /\ [.r,s.]; reconsider t as set by TARSKI:1; t c= [.r,s.] by A2,XBOOLE_1:17; hence thesis; end; hence thesis by A1,TOPMETR:18; end; theorem Th39: 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) proof let jauge be Function of [.r,s.],].0,+infty.[, S be Subset-Family of Closed-Interval-TSpace(r,s); assume that A1: r <= s and A2: S = the set of all ].x-jauge.x,x+jauge.x.[ /\ [.r,s.] where x is Element of [.r,s.]; [.r,s.] c= union S proof let x be object; assume A3: x in [.r,s.]; then reconsider x0 = x as Element of [.r,s.]; x0 in dom jauge by A3,PARTFUN1:def 2; then jauge.x0 in rng jauge by FUNCT_1:3; then 0 < jauge.x0 by XXREAL_1:4; then x0 - jauge.x0 < x0 - 0 & x0 + 0 < x0 + jauge.x0 by XREAL_1:15,XREAL_1:8; then x0 in ].x0-jauge.x0,x0+jauge.x0.[ by XXREAL_1:4; then A5: x0 in ].x0-jauge.x0,x0+jauge.x0.[ /\ [.r,s.] by A3,XBOOLE_0:def 4; ].x0-jauge.x0,x0+jauge.x0.[ /\ [.r,s.] in S by A2; hence thesis by A5,TARSKI:def 4; end; then S is Cover of [.r,s.] by SETFAM_1:def 11; hence thesis by A1,TOPMETR:18; end; theorem Th40: 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 proof let jauge be Function of [.r,s.],].0,+infty.[, S be Subset-Family of Closed-Interval-TSpace(r,s); assume that A1: r <= s and A2: S = the set of all ].x-jauge.x,x+jauge.x.[ /\ [.r,s.] where x is Element of [.r,s.]; for P be Subset of Closed-Interval-TSpace(r,s) st P in S holds P is open proof let P be Subset of Closed-Interval-TSpace(r,s); assume P in S; then consider x0 be Element of [.r,s.] such that A4: P = ].x0-jauge.x0,x0+jauge.x0.[ /\[.r,s.] by A2; set CIT = Closed-Interval-TSpace(r,s), CIM = Closed-Interval-MSpace(r,s); A5: CIT = TopSpaceMetr(CIM) by TOPMETR:def 7; A6: TopSpaceMetr(CIM) = TopStruct(# the carrier of CIM,Family_open_set CIM#) by PCOMPS_1:def 5; reconsider I = [.r,s.] as non empty Subset of RealSpace by A1,XXREAL_1:30; reconsider P1 = P as Subset of CIM by TOPMETR:def 7,A6; for t be Element of CIM st t in P1 holds ex r be Real st r > 0 & Ball(t,r) c= P1 proof let t be Element of CIM; assume A7: t in P1; the carrier of CIM c= the carrier of RealSpace by TOPMETR:def 1; then reconsider tr = t as Point of RealSpace; reconsider XJ = ].x0-jauge.x0,x0+jauge.x0.[ as Subset of RealSpace; reconsider XK = XJ as Subset of R^1 by TOPMETR:17; [.r,s.] is non empty by A1,XXREAL_1:30; then x0 in [.r,s.]; then reconsider p = x0 as Point of RealSpace; tr in XK by A7,A4,XBOOLE_0:def 4; then consider r0 be Real such that A8: r0 > 0 and A9: Ball(tr,r0) c= XK by JORDAN6:35,TOPMETR:15,TOPMETR:def 6; take r0; Ball(t,r0) = Ball(tr,r0) /\ the carrier of CIM by TOPMETR:9; then Ball(t,r0) = Ball(tr,r0) /\ [.r,s.] by A1,TOPMETR:10; hence thesis by A4,A8,A9,XBOOLE_1:27; end; then P in Family_open_set CIM by PCOMPS_1:def 4; hence thesis by A5,A6,PRE_TOPC:def 2; end; hence thesis by TOPS_2:def 1; end; theorem Th41: 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 proof let jauge be Function of [.r,s.],].0,+infty.[, S be Subset-Family of Closed-Interval-TSpace(r,s); assume A1: S = the set of all ].x-jauge.x,x+jauge.x.[ /\ [.r,s.] where x is Element of [.r,s.]; for X being Subset of Closed-Interval-TSpace(r,s) st X in S holds X is connected proof let X be Subset of Closed-Interval-TSpace(r,s); assume X in S; then consider x0 be Element of [.r,s.] such that A2: X = ].x0-jauge.x0,x0+jauge.x0.[ /\ [.r,s.] by A1; thus thesis by A2,RCOMP_3:43; end; hence thesis by RCOMP_3:def 1; end; theorem 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.[ ) proof let jauge be Function of [.r,s.],].0,+infty.[, S be Subset-Family of Closed-Interval-TSpace(r,s); assume that A1: r <= s and A2: S = the set of all ].x-jauge.x,x+jauge.x.[ /\ [.r,s.] where x is Element of [.r,s.]; let IC be IntervalCover of S; S is Subset-Family of Closed-Interval-TSpace(r,s) & S is Cover of Closed-Interval-TSpace(r,s) & S is open connected & r <= s by A1,A2,Th39,Th40,Th41; hence thesis by RCOMP_3:def 2; end; theorem Th42: 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 let r,s,t,x be Real; hereby assume that A1: r <= x - t and A2: x + t <= s; ].x-t,x+t.[ c= [.r,s.] proof let u be object; assume A3: u in ].x-t,x+t.[; then reconsider u1 = u as Real; x-t proof let a,b be Real, Iab be non empty closed_interval Subset of REAL; assume that A1: a <= b and A2: Iab = [.a,b.]; let Dab be Division of Iab; assume A3: len Dab = 1; then consider d be Real such that A4: Dab = <*Dab.1*> by FINSEQ_1:40; Dab.1 = upper_bound Iab by A3,INTEGRA1:def 2 .= b by A1,A2,JORDAN5A:19; hence thesis by A4; end; theorem 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 proof let a,b being Real,Iab being non empty compact Subset of REAL, Dab being Division of Iab; assume A1: 2 <= len Dab; set D = (Dab/^1); A2: 1 <= len Dab by A1,XXREAL_0:2; then A3: len D = len Dab - 1 by RFINSEQ:def 1; A4: D is non empty increasing FinSequence of REAL proof A5: D is non empty proof 2 - 1 <= len Dab - 1 by A1,XREAL_1:13; hence thesis by A3; end; D is increasing proof now let e1,e2 being ExtReal; assume that A6: e1 in dom D and A7: e2 in dom D and A8: e1 < e2; reconsider ne1 = e1, ne2 = e2 as Nat by A6,A7; A9: D.e1 = Dab.(ne1 + 1) by A2,A6,RFINSEQ:def 1; ne1 in Seg len D by A6,FINSEQ_1:def 3; then ne1 + 1 in Seg (len D + 1) by FINSEQ_1:60; then A10: ne1 + 1 in dom Dab by A3,FINSEQ_1:def 3; ne2 in Seg len D & ne2 in Seg len D by A7,FINSEQ_1:def 3; then ne2 + 1 in Seg (len D + 1) by FINSEQ_1:60; then A11: ne2 + 1 in dom Dab by A3,FINSEQ_1:def 3; A12: D.e2 = Dab.(ne2 + 1) by A2,A7,RFINSEQ:def 1; ne1 + 1 < ne2 + 1 by A8,XREAL_1:8; hence D.e1 < D.e2 by A9,A12,A10,A11,VALUED_0:def 13; end; hence thesis; end; hence thesis by A5; end; A13: rng D c= Iab proof A14: rng D c= rng Dab by FINSEQ_5:33; rng Dab c= Iab by INTEGRA1:def 2; hence thesis by A14; end; D.(len D) = upper_bound Iab proof 2 - 1 <= len Dab - 1 by A1,XREAL_1:13; then Seg len D = dom D & len D in Seg len D by A3,FINSEQ_1:def 3,FINSEQ_1:3; then D.(len D) = Dab.(len D + 1) by A2,RFINSEQ:def 1 .= Dab.len Dab by A3; hence thesis by INTEGRA1:def 2; end; hence thesis by A4,A13,INTEGRA1:def 2; end; theorem Th45: for a,b being Real st a < b holds <*a,b*> is non empty increasing FinSequence of REAL proof let a,b be Real; assume A1: a < b; set s = <*a,b*>; A2: rng s c= REAL; s is increasing proof now let e1,e2 be ExtReal; assume that A3: e1 in dom s and A4: e2 in dom s and A5: e1 < e2; dom s = Seg len s by FINSEQ_1:def 3 .= Seg 2 by FINSEQ_1:44; then (e1 = 1 or e1 = 2) & (e2 = 1 or e2 = 2) by TARSKI:def 2,A3,A4,FINSEQ_1:2; then s.e1 = a & s.e2 = b by A5,FINSEQ_1:44; hence s.e1 < s.e2 by A1; end; hence thesis; end; hence thesis by A2,FINSEQ_1:def 4; end; theorem 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 proof let a,b be Real, Iab be non empty closed_interval Subset of REAL; assume that A1: a < b and A2: Iab = [.a,b.]; thus <*a,b*> is Division of Iab proof set D = <*a,b*>; A3: D is non empty increasing FinSequence of REAL by A1,Th45; A4: rng D c= Iab proof let x be object; assume x in rng D; then x in {a,b} by FINSEQ_2:127; then x = a or x = b by TARSKI:def 2; hence thesis by A1,A2,XXREAL_1:1; end; D.(len D) = upper_bound Iab proof A5: len D = 2 by FINSEQ_1:44; upper_bound Iab = b by A1,A2,JORDAN5A:19; hence thesis by A5,FINSEQ_1:44; end; hence thesis by A3,A4,INTEGRA1:def 2; end; end; begin :: Cousin's Lemma theorem Th46: 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)) proof let a,b being Real, jauge being positive-yielding Function of [.a,b.],REAL; assume A1: a <= b; defpred P[object] means ex x be non empty increasing FinSequence of REAL, t be non empty FinSequence of REAL st x.1 = a & x.(len x) = \$1 & t.1 = a & dom x = dom t & (for i be Nat st i-1 in dom t & i in dom t holds t.i - jauge.(t.i) <= x.(i-1) <= t.i) & (for i be Nat st i in dom t holds t.i <= x.i <= t.i + jauge.(t.i)); consider C be set such that A2: for x be object holds x in C iff x in [.a,b.] & P[x] from XBOOLE_0:sch 1; for x be object st x in C holds x is real proof let x be object; assume x in C; then x in [.a,b.] by A2; hence thesis; end; then reconsider C as real-membered set by MEMBERED:def 3; A3: now thus a in [.a,b.] by A1,XXREAL_1:1; now set x = <*a*>; set t = <*a*>; take x,t; len x = 1 & len t = 1 by FINSEQ_1:39; hence x.1 = a & x.(len x) = a & t.1 = a by FINSEQ_1:def 8; thus dom x = dom t; thus for i be Nat st i-1 in dom t & i in dom t holds t.i - jauge.(t.i) <= x.(i-1) <= t.i proof let i be Nat; assume i - 1 in dom t & i in dom t; then i - 1 in {1} & i in {1} by FINSEQ_1:2,FINSEQ_1:def 8; then i - 1 = 1 & i = 1 by TARSKI:def 1; hence thesis; end; thus for i be Nat st i in dom t holds t.i <= x.i <= t.i + jauge.(t.i) proof let i be Nat; assume i in dom t; then i in {1} by FINSEQ_1:2,FINSEQ_1:def 8; then A4: i = 1 by TARSKI:def 1; thus t.i <= x.i; t.i = a by A4,FINSEQ_1:def 8; then t.i in [.a,b.] by A1,XXREAL_1:1; then t.i in dom jauge by FUNCT_2:def 1; then jauge.(t.i) in rng jauge by FUNCT_1:3; then x.i + 0 < t.i + jauge.(t.i) by XREAL_1:8,PARTFUN3:def 1; hence x.i <= t.i + jauge.(t.i); end; end; hence P[a]; end; A5: b is UpperBound of [.a,b.] by XXREAL_2:21; C c= [.a,b.] by A2; then A6: b is UpperBound of C by A5,XXREAL_2:6; then C is non empty bounded_above real-membered by A3,A2,XXREAL_2:def 10; then reconsider c = sup C as Real; A7: c in [.a,b.] proof assume not c in [.a,b.]; then per cases by XXREAL_1:1; suppose c < a; hence thesis by A3,A2,XXREAL_2:4; end; suppose b < c; hence thesis by A6,XXREAL_2:def 3; end; end; then c in dom jauge by FUNCT_2:def 1; then A8: jauge.c in rng jauge by FUNCT_1:3; then A9: c - jauge.c < c by XREAL_1:44,PARTFUN3:def 1; C c= REAL by MEMBERED:3; then C c= ExtREAL by NUMBERS:31; then C is non empty Subset of ExtREAL by A3,A2; then consider d be Element of ExtREAL such that A10: d in C and A11: c - jauge.c < d by A9,XXREAL_2:94; consider D0 be non empty increasing FinSequence of REAL, T0 be non empty FinSequence of REAL such that A12: D0.1 = a and A13: D0.(len D0) = d and A13bis: T0.1 = a and A14: dom D0 = dom T0 and A15: (for i be Nat st i-1 in dom T0 & i in dom T0 holds T0.i - jauge.(T0.i) <= D0.(i-1) <= T0.i) and A16: (for i be Nat st i in dom T0 holds T0.i <= D0.i <= T0.i + jauge.(T0.i)) by A10,A2; set D1 = D0 ^ <*c*>, T1 = T0 ^ <*c*>; A17: c in C & P[c] proof per cases; suppose d = c; hence thesis by A10,A12,A13,A13bis,A14,A15,A16; end; suppose A18: d <> c; A19: d <= sup C by A10,XXREAL_2:4; then D0.len D0 < c by A13,A18,XXREAL_0:1; then A20: D0.len(D0) < <*c*>.1 by FINSEQ_1:def 8; now thus c in [.a,b.] by A7; now reconsider D2 = D1 as non empty increasing FinSequence of REAL by A20,Th1; reconsider T2 = T1 as non empty FinSequence of REAL; take D2,T2; rng D0 <> {}; then 1 in dom D0 by FINSEQ_3:32; hence D2.1 = a by A12,FINSEQ_1:def 7; A21: len D2 = len D0 + len (<*c*>) by FINSEQ_1:22 .= len D0 + 1 by FINSEQ_1:39; 1 in Seg 1 by FINSEQ_1:1; then 1 in dom <*c*> by FINSEQ_1:def 8; then D2.len D2 = (<*c*>).1 by A21,FINSEQ_1:def 7 .= c by FINSEQ_1:def 8; hence D2.len D2 = c; rng T0 <> {}; then 1 in dom T0 by FINSEQ_3:32; hence T2.1 = a by A13bis,FINSEQ_1:def 7; A22: Seg len D0 = dom T0 by A14,FINSEQ_1:def 3 .= Seg len T0 by FINSEQ_1:def 3; A23: dom D2 = Seg (len D0 + len <*c*>) by FINSEQ_1:def 7 .= Seg (len T0 + len <*c*>) by A22,FINSEQ_1:6 .= dom (T0^<*c*>) by FINSEQ_1:def 7; hence dom D2 = dom T2; A24: Seg len D2 = dom T2 by A23,FINSEQ_1:def 3; hereby let i be Nat; assume that A25: i - 1 in dom T2 and A26: i in dom T2; A27: i - 1 in dom T0 or ex n1 be Nat st n1 in dom (<*c*>) & i - 1 = len T0 + n1 by A25,FINSEQ_1:25; A28: (ex n1 be Nat st n1 in dom (<*c*>) & i - 1 = len T0 + n1) implies i = len T0 + 2 proof assume (ex n1 be Nat st n1 in dom (<*c*>) & i - 1 = len T0 + n1); then consider n1 be Nat such that A29: n1 in dom (<*c*>) and A30: i - 1 = len T0 + n1; n1 in Seg 1 by A29,FINSEQ_1:def 8; then n1 = 1 by TARSKI:def 1,FINSEQ_1:2; hence thesis by A30; end; per cases by A26,FINSEQ_1:25; suppose A40: i in dom T0; then A41: T2.i = T0.i by FINSEQ_1:def 7; per cases by A25,FINSEQ_1:25,A28; suppose A42: i - 1 in dom T0; then T0.i - jauge.(T0.i) <= D0.(i-1) <= T0.i by A40,A15; hence T2.i - jauge.(T2.i) <= D2.(i-1) <= T2.i by A41,A42,A14,FINSEQ_1:def 7; end; suppose i = len T0 + 2; then len T0 + 2 <= len T2 by A26,FINSEQ_3:25; then len T0 + 2 <= len D2 by A24,FINSEQ_1:def 3; then len T0 + 2 <= len T0 + 1 by A21,A22,FINSEQ_1:6; then len T0 + 2 - len T0 <= len T0 + 1 - len T0 by XREAL_1:13; hence T2.i - jauge.(T2.i) <= D2.(i-1) <= T2.i; end; end; suppose ex n0 be Nat st n0 in dom (<*c*>) & i = len T0 + n0; then consider n0 be Nat such that A43: n0 in dom (<*c*>) and A44: i = len T0 + n0; A45: n0 in Seg 1 by A43,FINSEQ_1:def 8; then A46: n0 = 1 by TARSKI:def 1,FINSEQ_1:2; 1 in Seg 1 by FINSEQ_1:1; then 1 in dom <*c*> by FINSEQ_1:def 8; then T2.i = <*c*>.1 by A46,A44,FINSEQ_1:def 7; then A47: T2.i = c by FINSEQ_1:def 8; D0.(i-1) = d by A13,A46,A44,A22,FINSEQ_1:6; hence T2.i - jauge.(T2.i) <= D2.(i-1) <= T2.i by A11,A19,A47,A45,A44,A27,A28,A14,FINSEQ_1:def 7, TARSKI:def 1,FINSEQ_1:2; end; end; hereby let i be Nat; assume i in dom T2; then per cases by FINSEQ_1:25; suppose A48: i in dom T0; then A49: T2.i = T0.i by FINSEQ_1:def 7; D2.i = D0.i by A48,A14,FINSEQ_1:def 7; hence T2.i <= D2.i <= T2.i + jauge.(T2.i) by A16,A49,A48; end; suppose ex n0 be Nat st n0 in dom (<*c*>) & i = len T0 + n0; then consider n0 be Nat such that A50: n0 in dom (<*c*>) and A51: i = len T0 + n0; A52: 1 in Seg 1 by FINSEQ_1:1; then A53: 1 in dom <*c*> by FINSEQ_1:def 8; A54: n0 in Seg 1 by A50,FINSEQ_1:def 8; then n0 = 1 by FINSEQ_1:2,TARSKI:def 1; then A55: T2.i = <*c*>.1 by A53,A51,FINSEQ_1:def 7; len T0 = len D0 by A22,FINSEQ_1:6; then A56: i = len D0 + 1 by A54,FINSEQ_1:2,TARSKI:def 1,A51; 1 in dom <*c*> by A52,FINSEQ_1:def 8; then A57: D2.i = <*c*>.1 by A56,FINSEQ_1:def 7 .= c by FINSEQ_1:def 8; dom jauge = [.a,b.] by FUNCT_2:def 1; then T2.i in dom jauge by A7,A55,FINSEQ_1:def 8; then jauge.(T2.i) in rng jauge by FUNCT_1:3; then T2.i + 0 < T2.i + jauge.(T2.i) by PARTFUN3:def 1,XREAL_1:8; hence T2.i <= D2.i <= T2.i + jauge.(T2.i) by A55,FINSEQ_1:def 8,A57; end; end; end; hence P[c]; end; hence thesis by A2; end; end; c = b proof assume A58: not c = b; A59: a <= c <= b by A7,XXREAL_1:1; set c2 = min(c + jauge.(c)/2,b); A60: c2 in C & P[c2] proof set D1 = D0 ^ <*c2*>, T1 = T0 ^ <*c*>; per cases; suppose d = c2; hence thesis by A10,A2; end; suppose A61: d <> c2; A62: 0 < jauge.c by A8,PARTFUN3:def 1; reconsider d as Real by A10; A63: d + 0 < c + jauge.(c)/2 by A10,XXREAL_2:4,A62,XREAL_1:8; A64: d < b proof assume A65: b <= d; d in [.a,b.] by A10,A2; then a <= d <= b by XXREAL_1:1; then c2 = min (d,c+jauge.(c)/2) by A65,XXREAL_0:1; hence thesis by A63,XXREAL_0:def 9,A61; end; d + 0 < c + jauge.(c)/2 by A10,XXREAL_2:4,A62,XREAL_1:8; then D0.len D0 < c2 by A13,A64,XXREAL_0:21; then A66: D0.len(D0) < <*c2*>.1 by FINSEQ_1:def 8; now thus A67: c2 in [.a,b.] proof A68: c2 <= b by XXREAL_0:17; c in [.a,b.] by A17,A2; then A69: a <= c <= b by XXREAL_1:1; 0 < jauge.c by A8,PARTFUN3:def 1; then a + 0 < c + jauge.(c)/2 by A69,XREAL_1:8; then a <= c2 by A1,XXREAL_0:20; hence thesis by A68,XXREAL_1:1; end; now reconsider D2 = D1 as non empty increasing FinSequence of REAL by A66,Th1; reconsider T2 = T1 as non empty FinSequence of REAL; take D2,T2; rng D0 <> {}; then 1 in dom D0 by FINSEQ_3:32; hence D2.1 = a by A12,FINSEQ_1:def 7; A70: len D2 = len D0 + len (<*c2*>) by FINSEQ_1:22 .= len D0 + 1 by FINSEQ_1:39; 1 in Seg 1 by FINSEQ_1:1; then 1 in dom <*c2*> by FINSEQ_1:def 8; then D2.len D2 = (<*c2*>).1 by A70,FINSEQ_1:def 7 .= c2 by FINSEQ_1:def 8; hence D2.len D2 = c2; rng T0 <> {}; then 1 in dom T0 by FINSEQ_3:32; hence T2.1 = a by A13bis,FINSEQ_1:def 7; A71: Seg len D0 = dom T0 by A14,FINSEQ_1:def 3 .= Seg len T0 by FINSEQ_1:def 3; A72: dom D2 = Seg len (D0^<*c2*>) by FINSEQ_1:def 3 .= Seg (len D0 + 1) by FINSEQ_2:16 .= Seg (len T0 + 1) by A71,FINSEQ_1:6 .= Seg len (T0 ^ <*c*>) by FINSEQ_2:16 .= dom (T0^<*c*>) by FINSEQ_1:def 3; hence dom D2 = dom T2; A73: Seg len D2 = dom T2 by A72,FINSEQ_1:def 3; hereby let i be Nat; assume that A74: i - 1 in dom T2 and A75: i in dom T2; A76: (ex n1 be Nat st n1 in dom (<*c*>) & i - 1 = len T0 + n1) implies i = len T0 + 2 proof assume (ex n1 be Nat st n1 in dom (<*c*>) & i - 1 = len T0 + n1); then consider n1 be Nat such that A77: n1 in dom (<*c*>) and A78: i - 1 = len T0 + n1; n1 in Seg 1 by A77,FINSEQ_1:def 8; then i - 1 = len T0 + 1 by A78,TARSKI:def 1,FINSEQ_1:2; hence thesis; end; per cases by A75,FINSEQ_1:25; suppose A79: i in dom T0; then A80: T2.i = T0.i by FINSEQ_1:def 7; per cases by A74,FINSEQ_1:25,A76; suppose A81: i - 1 in dom T0; then T0.i - jauge.(T0.i) <= D0.(i-1) <= T0.i by A79,A15; hence T2.i - jauge.(T2.i) <= D2.(i-1) <= T2.i by A80,A81,A14,FINSEQ_1:def 7; end; suppose A82: i = len T0 + 2; i <= len T2 by A75,FINSEQ_3:25; then len T0 + 2 <= len D2 by A82,A73,FINSEQ_1:def 3; then len T0 + 2 <= len T0 + 1 by A70,A71,FINSEQ_1:6; then len T0 + 2 - len T0 <= len T0 + 1 - len T0 by XREAL_1:13; hence T2.i - jauge.(T2.i) <= D2.(i-1) <= T2.i; end; end; suppose ex n0 be Nat st n0 in dom (<*c*>) & i = len T0 + n0; then consider n0 be Nat such that A83: n0 in dom (<*c*>) and A84: i = len T0 + n0; A85: n0 in Seg 1 by A83,FINSEQ_1:def 8; then A86: n0 = 1 by TARSKI:def 1,FINSEQ_1:2; A87: i - 1 in dom T0 by A74,A76,FINSEQ_1:25,A84,A85,TARSKI:def 1,FINSEQ_1:2; 1 in Seg 1 by FINSEQ_1:1; then 1 in dom <*c*> by FINSEQ_1:def 8; then T2.i = <*c*>.1 by A86,A84,FINSEQ_1:def 7; then A88: T2.i = c by FINSEQ_1:def 8; D0.(i-1) = d by A13,A86,A84,A71,FINSEQ_1:6; then c - jauge.c <= D0.(i-1) <= c by A10,XXREAL_2:4,A11; hence T2.i - jauge.(T2.i) <= D2.(i-1) <= T2.i by A88,A87,A14,FINSEQ_1:def 7; end; end; hereby let i be Nat; assume i in dom T2; then per cases by FINSEQ_1:25; suppose A89: i in dom T0; then A90: T2.i = T0.i by FINSEQ_1:def 7; D2.i = D0.i by A89,A14,FINSEQ_1:def 7; hence T2.i <= D2.i <= T2.i + jauge.(T2.i) by A16,A90,A89; end; suppose ex n0 be Nat st n0 in dom (<*c*>) & i = len T0 + n0; then consider n0 be Nat such that A91: n0 in dom (<*c*>) and A92: i = len T0 + n0; 1 in Seg 1 by FINSEQ_1:1; then A93: 1 in dom <*c*> by FINSEQ_1:def 8; A94: n0 in Seg 1 by A91,FINSEQ_1:def 8; then n0 = 1 by FINSEQ_1:2,TARSKI:def 1; then T2.i = <*c*>.1 by A93,A92,FINSEQ_1:def 7; then A95: T2.i = c by FINSEQ_1:def 8; len T0 = len D0 by A71,FINSEQ_1:6; then A96: i = len D0 + 1 by A94,A92,FINSEQ_1:2,TARSKI:def 1; 1 in Seg 1 by FINSEQ_1:1; then 1 in dom <*c2*> by FINSEQ_1:def 8; then A97: D2.i = <*c2*>.1 by A96,FINSEQ_1:def 7 .= c2 by FINSEQ_1:def 8; A98: c <= b by A7,XXREAL_1:1; A99: 0 < jauge.c by A8,PARTFUN3:def 1; then A100: c + 0 <= c + jauge.(c)/2 by XREAL_1:8; A101: (c + jauge.(c)/2) + 0 < (c + jauge.(c)/2) + jauge.(c)/2 by A99,XREAL_1:8; c2 <= c + jauge.(c)/2 by XXREAL_0:17; hence T2.i <= D2.i <= T2.i + jauge.(T2.i) by A101,XXREAL_0:2,A95,A97,A100,A98,XXREAL_0:20; end; end; end; hence c2 in [.a,b.] & P[c2] by A67; end; hence c2 in C & P[c2] by A2; end; end; 0 < jauge.c by A8,PARTFUN3:def 1; then A102: c + 0 < c + jauge.(c)/2 by XREAL_1:8; c < b by A59,A58,XXREAL_0:1; then c < c2 by A102,XXREAL_0:def 9; hence thesis by A60,XXREAL_2:4; end; hence thesis by A17; end; ::\$N Cousin's Lemma theorem 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,jauge st TD is delta-fine proof let I being non empty closed_interval Subset of REAL, jauge being positive-yielding Function of I,REAL; consider a,b be Real such that A1: a <= b and A2: I = [.a,b.] by Th33; A3: lower_bound I = a & upper_bound I = b by A1,A2,JORDAN5A:19; reconsider r = 1/2 as positive Real; reconsider jauge2 = r (#) jauge as positive-yielding Function of I,REAL; consider x be non empty increasing FinSequence of REAL, t be non empty FinSequence of REAL such that A4: x.1 = a and A5: x.(len x) = b and A6: t.1 = a and A7: dom x = dom t and A8: (for i be Nat st i-1 in dom t & i in dom t holds t.i - jauge2.(t.i) <= x.(i-1) <= t.i) and A9: (for i be Nat st i in dom t holds t.i <= x.i <= t.i + jauge2.(t.i)) by A1,A2,Th46; now thus rng x c= I proof let u be object; assume A10: u in rng x; then consider v be object such that A11: v in dom x and A12: x.v = u by FUNCT_1:def 3; rng x c= REAL; then reconsider u1 = u as Element of REAL by A11,A12,FUNCT_1:3; reconsider v1 = v as Nat by A11; A13: 1 in dom x by A10,FINSEQ_3:31; per cases by Th3,A11; suppose v1 = 1; hence thesis by A1,A2,A4,A12,XXREAL_1:1; end; suppose A14: 1 < v1; per cases by A11,Th4; suppose A15: v1 < len x; len x in dom x by FINSEQ_5:6; then a <= u1 <= b by A5,A15,A14,A13,A4,A12,A11,VALUED_0:def 13; hence thesis by A2,XXREAL_1:1; end; suppose v1 = len x; hence thesis by A1,A2,A5,A12,XXREAL_1:1; end; end; end; thus x.(len x) = upper_bound I by A5,A1,A2,JORDAN5A:19; end; then reconsider D = x as Division of I by INTEGRA1:def 2; now t is non-decreasing proof assume not t is non-decreasing; then consider e1,e2 be ExtReal such that A16: e1 in dom t and A17: e2 in dom t and A18: e1 <= e2 and A19: t.e2 < t.e1; per cases by A16,Th3; suppose A20: e1 = 1; per cases by A17,Th3; suppose e2 = 1; hence thesis by A19,A20; end; suppose A21: 1 < e2; reconsider f2 = e2 as Nat by A17; f2 - 1 in dom t by A17,A21,CGAMES_1:20; then A22: x.(f2-1) <= t.f2 by A8,A17; rng x <> {}; then A23: 1 in dom x by FINSEQ_3:32; f2 - 1 in dom x by A17,A21,CGAMES_1:20,A7; then x.1 <= x.(f2-1) by A23,FINSEQ_3:25,VALUED_0:def 15; hence thesis by A4,A22,XXREAL_0:2,A19,A6,A20; end; end; suppose A24: 1 < e1; per cases by A18,XXREAL_0:1; suppose e1 = e2; hence thesis by A19; end; suppose A25: e1 < e2; A26: t.e1 <= x.e1 by A16,A9; reconsider f2 = e2 as Nat by A17; 1 < e2 by A24,A25,XXREAL_0:2; then A27: f2 - 1 in dom t by A17,CGAMES_1:20; then A28: x.(f2-1) <= t.e2 by A17,A8; per cases; suppose e1 = f2 - 1; then x.e1 <= t.e2 by A27,A17,A8; hence thesis by A26,XXREAL_0:2,A19; end; suppose A29: e1 <> f2 - 1; reconsider f1 = e1 as Nat by A16; f1 < f2 - 1 proof assume f2 - 1 <= f1; then f2 - 1 + 1<= f1 + 1 by XREAL_1:6; then f1 = f2 or f2 = f1 + 1 by A18,NAT_1:9; hence thesis by A25,A29; end; then x.e1 < x.(f2-1) by A27,A7,A16,VALUED_0:def 13; then x.e1 <= t.e2 by A28,XXREAL_0:2; hence thesis by A19,A26,XXREAL_0:2; end; end; end; end; then reconsider s = t as non empty non-decreasing FinSequence of REAL; take s; thus t = s; thus dom s = dom D by A7; thus for i be Nat st i in dom s holds s.i in divset(D,i) proof let i be Nat; assume A30: i in dom s; consider d1,d2 be Real such that A31: divset(D,i) = [.d1,d2.] by MEASURE5:def 3; A32: d1 <= d2 by A31,XXREAL_1:29; per cases by A30,Th3; suppose A33: i = 1; then lower_bound divset(D,i) = lower_bound I & upper_bound divset(D,i) = D.1 by A7,A30,INTEGRA1:def 4; then d1 = a & d2 = D.1 by A32,A31,JORDAN5A:19,A3; hence thesis by A6,A4,A31,A33,XXREAL_1:1; end; suppose A34: 1 < i; then lower_bound divset(D,i) = D.(i-1) & upper_bound divset(D,i) = D.i by A7,A30,INTEGRA1:def 4; then A35: d1 = D.(i-1) & d2 = D.i by A32,A31,JORDAN5A:19; i - 1 in dom t by A30,CGAMES_1:20,A34; then D.(i-1) <= s.i <= D.i by A30,A8,A9; hence thesis by A31,A35,XXREAL_1:1; end; end; end; then reconsider T = t as Element of set_of_tagged_Division(D) by Def2; reconsider TD = [D,T] as tagged_division of I,jauge by Def3; take TD; thus TD is delta-fine proof now take D; thus D is Division of I; take T; thus T is Element of set_of_tagged_Division(D); thus TD = [D,T]; thus for i be Nat st i in dom D holds vol divset(D,i) <= jauge.(T.i) proof let i be Nat; assume A36: i in dom D; consider u,v be Real such that A37: divset(D,i) = [.u,v.] by MEASURE5:def 3; u <= v by A37,XXREAL_1:29; then A38: lower_bound divset(D,i) = u & upper_bound divset(D,i) = v by A37,JORDAN5A:19; per cases by A36,Th3; suppose A39: i = 1; then A40: u = lower_bound I & v = D.1 by A36,A38,INTEGRA1:def 4; A41: vol divset(D,i) = v - u by A38,INTEGRA1:def 5 .= D.1 - a by A40,A1,A2,JORDAN5A:19 .= 0 by A4; T.i in [.a,b.] by A39,A6,A1,XXREAL_1:1; then T.i in dom jauge by A2,FUNCT_2:def 1; then jauge.(T.i) in rng jauge by FUNCT_1:3; hence thesis by A41,PARTFUN3:def 1; end; suppose A42: 1 < i; then A43: u = D.(i-1) & v = D.i by A36,A38,INTEGRA1:def 4; i - 1 in dom t by A36,A7,A42,CGAMES_1:20; then A44: t.i - jauge2.(t.i) <= x.(i-1) by A36,A7,A8; A45: set_of_tagged_Division(D) is non empty by Th34; consider s be non empty non-decreasing FinSequence of REAL such that A46: T = s and A47: dom s = dom D and A48: for i be Nat st i in dom s holds s.i in divset(D,i) by A45,Def2; divset(D,i) c= I by A36,INTEGRA1:8; then t.i in I by A46,A47,A48,A36; then A49: t.i in dom jauge2 by FUNCT_2:def 1; x.i <= t.i + jauge2.(t.i) by A36,A7,A9; then x.i - x.(i-1) <= (t.i + jauge2.(t.i)) - (t.i - jauge2.(t.i)) by A44,XREAL_1:13; then x.i - x.(i-1) <= 2 * jauge2.(t.i); then x.i - x.(i-1) <= 2 * ((1/2) * jauge.(t.i)) by A49,VALUED_1:def 5; hence thesis by A38,INTEGRA1:def 5,A43; end; end; end; hence thesis; end; end;