:: Cousin's Lemma
:: by Roland Coghetto
::
:: Received December 31, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XREAL_0, VALUED_1, INT_1, NEWTON, MEMBERED, PARTFUN1, RCOMP_3,
TOPMETR, SEQ_4, INTEGRA1, MEASURE7, COUSIN, NORMSP_2, SETFAM_1, RELAT_1,
COMPL_SP, PROB_1, FUNCT_2, NUMBERS, SUBSET_1, NAT_1, FUNCT_1, ARYTM_3,
FINSEQ_2, ZFMISC_1, COMPLEX1, STRUCT_0, XBOOLE_0, NORMSP_1, EUCLID,
PRE_TOPC, REAL_1, CARD_1, XXREAL_0, ARYTM_1, FINSEQ_1, CARD_3, ORDINAL4,
TARSKI, SQUARE_1, SEQ_2, ORDINAL2, SEQ_1, RSSPACE3, REWRITE1, METRIC_1,
BHSP_3, REAL_NS1, NORMSP_0, XXREAL_2, XXREAL_1, MEASURE5, RCOMP_1,
PCOMPS_1, POWER, RFINSEQ, RELAT_2, PARTFUN3, VALUED_0;
notations ORDINAL1,
INT_1, NEWTON, VALUED_1, MEMBERED, PARTFUN1, CONNSP_1, SETFAM_1,
TOPS_2, TOPMETR, XXREAL_2, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, XCMPLX_0,
XXREAL_0, FINSEQ_1, RFINSEQ, METRIC_1, ZFMISC_1, SUBSET_1, BINOP_1,
PRE_TOPC, NAT_1, FINSEQ_2, FUNCT_2, STRUCT_0, NUMBERS, XREAL_0, SQUARE_1,
COMPLEX1, RLVECT_1, SEQ_1, SEQ_2, RVSUM_1, NORMSP_0, NORMSP_1, RSSPACE3,
REAL_NS1, TBSP_1, EUCLID, PROB_1, KURATO_0, RELSET_1, PCOMPS_1, CARD_3,
KURATO_2, NORMSP_2, COMPL_SP, RCOMP_1, MEASURE5, SEQ_4, INTEGRA1, SEQM_3,
PARTFUN3, RCOMP_3, MATRPROB, POWER;
constructors NEWTON, CONNSP_1, TOPS_2, RCOMP_3, SQUARE_1, RSSPACE3, LOPBAN_1,
RVSUM_1, COMSEQ_2, REAL_NS1, TBSP_1, KURATO_0, COMPL_SP, FRECHET,
NORMSP_2, SEQ_4, INTEGRA1, MEASURE6, RFINSEQ, REAL_1, PARTFUN3, MATRPROB,
POWER;
registrations SEQ_2, LOPBAN_5, VALUED_1, XXREAL_2, METRIC_1, MATRTOP1,
BORSUK_5, JORDAN5A, COMPLEX1, SUBSET_1, FUNCT_1, RELSET_1, XXREAL_0,
XREAL_0, MEMBERED, STRUCT_0, VALUED_0, FUNCT_2, EUCLID, FINSEQ_1, CARD_1,
NAT_1, REAL_NS1, COMPL_SP, MEASURE5, INTEGRA1, SEQM_3, RELAT_1, ORDINAL1,
XCMPLX_0, NUMBERS, INT_1, RVSUM_1, SEQ_4, PARTFUN3, POWER;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
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 <= len p by FINSEQ_3:25; 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 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 be Element of Euclid n, g,h be 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:
the carrier of REAL-NS n = the carrier of Euclid n
proof
thus the carrier of Euclid n = the carrier of TOP-REAL n by EUCLID:67
.= REAL n by EUCLID:22
.= the carrier of REAL-NS n by REAL_NS1:def 4;
end;
theorem Th11:
s1 = s2 implies (s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm)
proof
assume
A1: s1 = s2;
thus s1 is Cauchy implies s2 is Cauchy_sequence_by_Norm
proof
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;
assume
A9: s2 is Cauchy_sequence_by_Norm;
now
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;
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;
registration
let n be Nat;
cluster Euclid n -> complete;
coherence
proof
MetricSpaceNorm REAL-NS n = Euclid n by Th15;
hence thesis;
end;
end;
begin :: The Nested Intervals Theorem (1-dimensional Euclidean space)
definition
let a,b be Real_Sequence;
func IntervalSequence(a,b) -> SetSequence of REAL 1 means :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;
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 be 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.] *>;
consider g1 be Function of NAT,bool REAL 1 such that
A13: g1 = f1 and
A14: for i be Nat holds g1.i = product <* [. a.i,b.i .] *> by A11;
consider g2 be Function of NAT,bool REAL 1 such that
A15: g2 = f2 and
A16: for i be Nat holds g2.i = product <* [. a.i,b.i .] *> by A12;
A17: dom g1 = NAT & dom g2 = NAT by FUNCT_2:def 1;
for x be object st x in dom g1 holds g1.x = g2.x
proof
let x be object;
assume x in dom g1;
then g1.x = product <* [.a.x,b.x.] *> &
g2.x = product <* [.a.x,b.x.] *> by A14,A16;
hence thesis;
end;
hence f1 = f2 by A13,A15,A17;
end;
end;
theorem Th17:
for a,b being Real_Sequence holds
IntervalSequence(a,b) is SetSequence of Euclid 1
proof
let a,b be 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
A8: product <*REAL*> c= REAL 1
proof
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;
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;
REAL 1 c= product <*REAL*>
proof
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;
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;
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.];
then ux in [.a,b.] & uy in [.a,b.]
by A8,A10,A13,A14;
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.];
then ux in [.a,b.] & uy in [.a,b.]
by A8,A10,A13,A14;
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,Def1;
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;
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 Def1;
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
take r = 1;
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.];
then ux in [.a.i,b.i.] & uy in [.a.i,b.i.]
by A14,A16,A19,A20;
hence dist(x,y) <= r by A21,A18,UNIFORM1:12;
end;
end;
end;
then si is bounded;
hence s.i is bounded by Def1;
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 Def1;
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;
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;
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,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,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;
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; 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;
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.];
A11: (<*[.a.n,b.n.]*>).i = [.a.n,b.n.] by A9;
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 Def1;
hence IntervalSequence(a,b).m c= IntervalSequence(a,b).n by Def1;
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;
thus 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 be 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 be 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[0] 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);
let k be Nat;
ex i be Nat st i = k & a.i <= b.i by A6;
hence a.k <= b.k;
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 be Real_Sequence, S be 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,Def1;
then reconsider IntervalSequence2 = product <* [.a.i,b.i.] *> as
Subset of Euclid 1;
diameter(S.i) = diameter IntervalSequence2 by A2,Def1
.= 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 be Real_Sequence, S be 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[0];
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);
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;
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[0]
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 be Real_Sequence, S be 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;
set S2 = diameter S;
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<p ex n be Nat st
for m be Nat st n<=m holds |.(S2.m) - 0.| < p
proof
let p be Real;
assume
A13: 0 < p;
A14: now
0 + 1 < (b.0-a.0) / p + 1 by A13,A8,XREAL_1:8; then
A15: 0 <= log(2,(b.0-a.0)/p + 1) by Th2;
reconsider i0 = [/ log(2,(b.0-a.0)/p + 1) \] as Integer;
A16: log(2,(b.0-a.0)/p + 1) <= i0 by INT_1:def 7;
A17: i0 in NAT by A15,INT_1:3;
A18: log(2,(b.0-a.0)/p + 1) + 0 < i0 + 1 by A16,XREAL_1:8;
reconsider n0 = i0 + 1 as Nat by A17;
take n0;
let m be Nat;
assume
A19: n0 <= m;
A20: 0 < 2 to_power n0 by POWER:34;
2 to_power log(2,(b.0-a.0) / p + 1) < 2 to_power n0
by A18,POWER:39; then
A21: (b.0 - a.0) / p + 1 < 2 to_power n0 by A13,A8,POWER:def 3;
(b.0 - a.0) / p < (b.0 - a.0) / p + 1 by XREAL_1:29;
then (b.0 - a.0) / p < 2 to_power n0 by A21,XXREAL_0:2;
then (b.0 - a.0) / p * p < (2 to_power n0) * p by A13,XREAL_1:68;
then b.0 - a.0 < p * 2 to_power n0 by A13,XCMPLX_1:87;
then (b.0 - a.0) / (2 to_power n0) <
p * (2 to_power n0) / (2 to_power n0) by A20,XREAL_1:74; then
A22: (b.0 - a.0) / (2 to_power n0) < p by A20,XCMPLX_1:89;
A23: 2 to_power n0 <= 2 to_power m by A19,NAT_6:1;
0 < 2 to_power n0 by POWER:34;
then (b.0 - a.0)/(2 to_power m) <= (b.0 - a.0)/(2 to_power n0)
by A23,A8,XREAL_1:118;
hence (b.0 - a.0) / (2 to_power m) < p by A22,XXREAL_0:2;
end;
now
consider n0 be Nat such that
A24: for m be Nat st n0 <= m holds (b.0-a.0)/(2 to_power m) < p by A14;
take n0;
hereby
let m be Nat;
assume
A25: n0 <= m;
a.m <= b.m by A1,A2,A3,Th28; then
A26: a.m - a.m <= b.m - a.m by XREAL_1:9;
(b-a).m = (b+ (-a)).m by SEQ_1:11
.= b.m +(-a).m by SEQ_1:7
.= b.m + (- a.m) by SEQ_1:10
.= b.m - a.m; then
A27: |.S2.m - 0.| = |.b.m - a.m.| by A9,SEQ_1:11
.= b.m - a.m by A26,ABSVALUE:def 1;
reconsider m0 = m as Element of NAT by ORDINAL1:def 12;
2|^m0 is Element of NAT;
then reconsider r = 2|^m as Real;
r <> 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;
set f = IntervalSequence(a,b);
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 Def1;
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 EUCLID:22,A4;
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 Def1;
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;
then c in [.a.i,b.i.] by A10,A11;
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
holds 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 be 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 be non empty closed_interval Subset of REAL,
D be 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;
S c= REAL* by A1;
hence S is Subset of REAL*;
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;
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);
A3: TD1 c= 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;
TD2 c= 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;
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 be non empty closed_interval Subset of REAL,
D be 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;
1 <= i by A1,FINSEQ_3:25; then
per cases by XXREAL_0:1;
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 be Real, Iab be non empty closed_interval Subset of REAL;
assume
A1: Iab = [.a,b.];
A2: a <= b by A1,XXREAL_1:29;
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;
hence thesis by A1,A2,JORDAN5A:19;
end;
hence thesis by A3,INTEGRA1:def 2;
end;
definition
let I be non empty closed_interval Subset of REAL;
mode tagged_division of I 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 A2,JORDAN5A:19;
b in [.a,b.] by A2,XXREAL_1:1;
hence <*b*>.i in divset(B,i) by A8,A6,A5;
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 be non empty closed_interval Subset of REAL,
jauge be positive-yielding Function of I,REAL,
TD be tagged_division of I;
attr TD is jauge-fine means
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
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 SEQ_4:9
.= r - r by SEQ_4:9;
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 be non empty closed_interval Subset of REAL,
Dac be Division of Iac,
Dcb be 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
A12: 1 <= len Dcb by FINSEQ_3:25;
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 be non empty closed_interval Subset of REAL,
Dac be Division of Iac, Dcb be 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 be 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;
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;
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 be non empty closed_interval Subset of REAL,
Dac be Division of Iac, Dcb be 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 <= len (Dcb/^1) by FINSEQ_3:25; 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;
registration
let I be non empty closed_interval Subset of REAL,
D be Division of I;
cluster set_of_tagged_Division(D) -> non empty;
coherence by Th34;
end;
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 be non empty increasing FinSequence of REAL,
r be Real;
assume s.len s < r;
then s.len s < <*r*>.1;
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 be non empty increasing FinSequence of REAL,
r be 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;
registration
let I be non empty closed_interval Subset of REAL,
D be Division of I;
cluster -> non empty for Element of set_of_tagged_Division(D);
coherence
proof
let T be Element of set_of_tagged_Division(D);
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;
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 be non empty closed_interval Subset of REAL,
D be Division of I, T be Element of set_of_tagged_Division(D);
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 be non empty closed_interval Subset of REAL,
TD be tagged_division of I;
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<u1<x+t by A3,XXREAL_1:4;
then r<=u1<=s by A1,A2,XXREAL_0:2;
hence thesis by XXREAL_1:1;
end;
hence ].x-t,x+t.[ /\ [.r,s.] = ].x-t,x+t.[ by XBOOLE_1:17,XBOOLE_1:19;
end;
hereby
assume that
A4: r <= x - t and
A5: s < x + t;
A6: ].x-t,x+t.[ /\ [.r,s.] c= ].x-t,s.]
proof
let u be object;
assume
A7: u in ].x-t,x+t.[ /\ [.r,s.]; then
A8: u in ].x-t,x+t.[ & u in [.r,s.] by XBOOLE_0:def 4;
reconsider u1 = u as Real by A7;
x-t < u1 <= s by A8,XXREAL_1:1,XXREAL_1:4;
hence thesis by XXREAL_1:2;
end;
].x-t,s.] c= ].x-t,x+t.[ /\ [.r,s.]
proof
let u be object;
assume
A9: u in ].x-t,s.];
then reconsider u1 = u as Real;
x-t<u1<=s by A9,XXREAL_1:2;
then x-t<u1<x+t & r<=u1<=s by A4,A5,XXREAL_0:2;
then u in ].x-t,x+t.[ & u in [.r,s.] by XXREAL_1:1,XXREAL_1:4;
hence thesis by XBOOLE_0:def 4;
end;
hence ].x-t,x+t.[ /\ [.r,s.] = ].x-t,s.] by A6;
end;
hereby
assume that
A10: x-t < r and
A11: x+t<=s;
A12: ].x-t,x+t.[ /\ [.r,s.] c= [.r,x+t.[
proof
let u be object;
assume
A13: u in ].x-t,x+t.[ /\ [.r,s.]; then
A14: u in ].x-t,x+t.[ & u in [.r,s.] by XBOOLE_0:def 4;
reconsider u1 = u as Real by A13;
r <= u1 < x+t by A14,XXREAL_1:4,XXREAL_1:1;
hence thesis by XXREAL_1:3;
end;
[.r,x+t.[ c= ].x-t,x+t.[ /\ [.r,s.]
proof
let u be object;
assume
A15: u in [.r,x+t.[;
then reconsider u1 = u as Real;
r<=u1<x+t by A15,XXREAL_1:3;
then x-t<u1<x+t & r<=u1<=s by A10,A11,XXREAL_0:2;
then u in ].x-t,x+t.[ & u in [.r,s.] by XXREAL_1:1,XXREAL_1:4;
hence thesis by XBOOLE_0:def 4;
end;
hence ].x-t,x+t.[ /\ [.r,s.] = [.r,x+t.[ by A12;
end;
hereby
assume that
A16: x-t < r and
A17: s <x+t;
[.r,s.] c= ].x-t,x+t.[
proof
let u be object;
assume
A18: u in [.r,s.];
then reconsider u1 = u as Real;
r<= u1<=s by A18,XXREAL_1:1;
then x-t<u1<x+t by A16,A17,XXREAL_0:2;
hence thesis by XXREAL_1:4;
end;
hence ].x-t,x+t.[ /\ [.r,s.] = [.r,s.] by XBOOLE_1:17,XBOOLE_1:19;
end;
end;
theorem
for r,s,t,x being Real,XT being Subset of REAL st
0 < t & r <= x <= s & XT = ].x-t,x+t.[ /\ [.r,s.] holds
(r <= x - t & x + t <= s implies
lower_bound XT = x-t & upper_bound XT = x+t) &
(r <= x - t & s < x + t implies
lower_bound XT = x-t & upper_bound XT = s) &
(x-t < r & x+t <= s implies
lower_bound XT = r & upper_bound XT = x+t) &
(x-t < r & s < x+t implies
lower_bound XT = r & upper_bound XT = s)
proof
let r,s,t,x be Real,XT be Subset of REAL;
assume that
A1: 0 < t and
A2: r <= x <= s and
A3: XT = ].x-t,x+t.[ /\ [.r,s.];
hereby
assume that
A4: r <= x-t and
A5: x+t <= s;
x - t < x - 0 & x + 0 < x + t by A1,XREAL_1:15,XREAL_1:8; then
A6: x - t < x + t by XXREAL_0:2;
XT = ].x-t,x+t.[ by A3,A4,A5,Th42;
hence lower_bound XT = x-t & upper_bound XT = x+t by A6,TOPREAL6:17;
end;
hereby
assume that
A7: r <= x-t and
A8: s < x+t;
A9: x - t < s - 0 by A2,A1,XREAL_1:15;
XT = ].x-t,s.] by A3,A7,A8,Th42;
hence lower_bound XT = x-t & upper_bound XT = s
by A9,RCOMP_3:6,RCOMP_3:7;
end;
hereby
assume that
A10: x-t < r and
A11: x+t <= s;
A12: r + 0 < x + t by A2,A1,XREAL_1:8;
XT = [.r,x+t.[ by A10,A11,A3,Th42;
hence lower_bound XT = r & upper_bound XT = x+t
by A12,RCOMP_3:4,RCOMP_3:5;
end;
assume that
A13: x-t < r and
A14: s < x+t;
A15: r <= s by A2,XXREAL_0:2;
XT = [.r,s.] by A3,A13,A14,Th42;
hence lower_bound XT = r & upper_bound XT = s by A15,JORDAN5A:19;
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;
hence s.e1 < s.e2 by A1;
end;
hence thesis;
end;
hence thesis by A2,FINSEQ_1:def 4;
end;
theorem Th43:
for a,b,c being Real,Iac,Icb being non empty compact Subset of REAL st
a <= c <= b & Iac=[.a,c.] & Icb=[.c,b.] holds
for Dac being Division of Iac, Dcb being Division of Icb,
i,j being Nat st i in dom Dac & j in dom Dcb holds
(i < len Dac implies Dac.i < Dcb.j) & ((i = len Dac & c < Dcb.1) implies
Dac.i < Dcb.j) & (Dcb.1 = c implies Dac.len Dac = Dcb.1)
proof
let a,b,c be Real,Iac,Icb be non empty compact Subset of REAL;
assume that
A1: a <= c <= b and
A2: Iac=[.a,c.] and
A3: Icb=[.c,b.];
let Dac be Division of Iac, Dcb be Division of Icb, i,j be Nat;
assume that
A4: i in dom Dac and
A5: j in dom Dcb;
A6: Dac.(len Dac) = upper_bound Iac by INTEGRA1:def 2
.= c by A1,A2,JORDAN5A:19;
rng Dcb c= [.c,b.] by A3,INTEGRA1:def 2;
then Dcb.j in [.c,b.] by A5,FUNCT_1:3; then
A7: c <= Dcb.j by XXREAL_1:1;
thus i < len Dac implies Dac.i < Dcb.j
proof
assume
A8: i < len Dac;
Seg len Dac = dom Dac by FINSEQ_1:def 3; then
len Dac in dom Dac by FINSEQ_1:3;
then Dac.i < c by A6,A8,A4,VALUED_0:def 13;
hence Dac.i < Dcb.j by A7,XXREAL_0:2;
end;
thus i = len Dac & c < Dcb.1 implies Dac.i < Dcb.j
proof
assume
A9: i = len Dac & c < Dcb.1;
A10: 1 in dom Dcb by FINSEQ_5:6;
j in Seg len Dcb by A5,FINSEQ_1:def 3;
then j = 1 or ... or j = len Dcb by FINSEQ_1:91;
then per cases by XXREAL_0:1;
suppose j = 1;
hence thesis by A9,A6;
end;
suppose 1 < j;
then Dcb.1 < Dcb.j by A10,A5, VALUED_0:def 13;
hence thesis by A9,A6,XXREAL_0:2;
end;
end;
thus Dcb.1 = c implies Dac.len Dac = Dcb.1 by A6;
end;
theorem Th44:
for a,b,c being Real,Iac,Icb being non empty compact Subset of REAL st
a <= c <= b & Iac=[.a,c.] & Icb=[.c,b.] holds
for Dac being Division of Iac, Dcb being Division of Icb,
i,j being Nat st i in dom Dac & j in dom Dcb holds
c < Dcb.1 implies Dac.i < Dcb.j
proof
let a,b,c be Real,Iac,Icb be non empty compact Subset of REAL;
assume that
A1: a <= c <= b and
A2: Iac=[.a,c.] and
A3: Icb=[.c,b.];
let Dac being Division of Iac, Dcb being Division of Icb, i,j being Nat;
assume that
A4: i in dom Dac and
A5: j in dom Dcb;
assume
A6: c < Dcb.1;
i <= len Dac by A4,FINSEQ_3:25;
then i < len Dac or i = len Dac by XXREAL_0:1;
hence thesis by A6,A1,A2,A3,A4,A5,Th43;
end;
theorem
for a,b,c being Real,Iab,Iac,Icb being non empty compact Subset of REAL st
a <= c <= b & Iab = [.a,b.] & Iac=[.a,c.] & Icb=[.c,b.] holds
for Dac being Division of Iac, Dcb being Division of Icb st c < Dcb.1 holds
Dac ^ Dcb is Division of Iab
proof
let a,b,c be Real,
Iab,Iac,Icb be non empty compact Subset of REAL;
assume that
A1: a <= c <= b and
A2: Iab = [.a,b.] and
A3: Iac = [.a,c.] and
A4: Icb = [.c,b.];
let Dac be Division of Iac,
Dcb be Division of Icb;
assume
A5: c < Dcb.1;
set Dacb = Dac ^ Dcb;
for e1,e2 being ExtReal st e1 in dom Dacb & e2 in dom Dacb & e1 < e2 holds
Dacb.e1 < Dacb.e2
proof
let e1,e2 be ExtReal;
assume that
A6: e1 in dom Dacb and
A7: e2 in dom Dacb and
A8: e1 < e2;
per cases by A6,A7,FINSEQ_1:25;
suppose
A9: e1 in dom Dac & e2 in dom Dac; then
A10: Dacb.e1 = Dac.e1 & Dacb.e2 = Dac.e2 by FINSEQ_1:def 7;
e1 < e2 & Dac is increasing by A8;
hence thesis by A9,A10;
end;
suppose
A11: e1 in dom Dac & ex n be Nat st n in dom Dcb &
e2 = len Dac + n;
then consider n0 be Nat such that
A12: n0 in dom Dcb and
A13: e2 = len Dac + n0;
Dacb.e1 = Dac.e1 & Dacb.e2 = Dcb.n0 by A11,A13,FINSEQ_1:def 7;
hence thesis by A11,A12,A3,A4,A5,Th44,A1;
end;
suppose
A14: (ex n be Nat st n in dom Dcb & e1 = len Dac + n) &
e2 in dom Dac;
then consider n0 be Nat such that
n0 in dom Dcb and
A15: e1 = len Dac + n0;
A16: len Dac <= e1 by A15,NAT_1:11;
e2 in Seg len Dac by FINSEQ_1:def 3,A14;
then e2 <= len Dac by FINSEQ_1:1;
hence thesis by A8,A16,XXREAL_0:2;
end;
suppose
A17: (ex n be Nat st n in dom Dcb & e1 = len Dac + n) &
(ex n be Nat st n in dom Dcb & e2 = len Dac + n);
then consider n1 be Nat such that
A18: n1 in dom Dcb and
A19: e1 = len Dac + n1;
consider n2 be Nat such that
A20: n2 in dom Dcb and
A21: e2 = len Dac + n2 by A17;
A22: len Dac + n1 - len Dac < len Dac + n2 - len Dac
by A8,A19,A21,XREAL_1:14;
Dcb.n1 = Dacb.e1 & Dcb.n2 = Dacb.e2
by A17,A19,A21,FINSEQ_1:def 7;
hence thesis by A22,A18,A20,VALUED_0:def 13;
end;
end; then
A23: Dacb is increasing;
A24: rng Dacb c= Iab
proof
let x be object;
assume
A25: x in rng Dacb;
A26: rng Dac c= [.a,c.] by A3,INTEGRA1:def 2;
rng Dcb c= [.c,b.] by A4,INTEGRA1:def 2;
then (rng Dac) \/ (rng Dcb) c= [.a,c.] \/ [.c,b.] by XBOOLE_1:13,A26;
then rng Dacb c= [.a,c.] \/ [.c,b.] by FINSEQ_1:31;
then rng Dacb c= [.a,b.] by A1,XXREAL_1:165;
hence thesis by A25,A2;
end;
Dacb.(len Dacb) = upper_bound Iab
proof
A27: a <= b by A1,XXREAL_0:2;
A28: len Dcb in Seg len Dcb by FINSEQ_1:3;
A29: Seg len Dcb = dom Dcb by FINSEQ_1:def 3;
len Dacb = len Dac + len Dcb by FINSEQ_1:22;
then Dacb.(len Dacb) = Dcb.(len Dcb) by A29,A28,FINSEQ_1:def 7
.= upper_bound Icb by INTEGRA1:def 2
.= b by JORDAN5A:19,A1,A4
.= upper_bound [.a,b.] by A27,JORDAN5A:19;
hence thesis by A2;
end;
hence thesis by A23,A24,INTEGRA1:def 2;
end;
theorem
for a,b being Real,Iab being non empty closed_interval Subset of REAL st
a <= b & Iab = [.a,b.] holds
for Dab being Division of Iab st len Dab = 1 holds Dab = <*b*>
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 be Real, Iab be non empty compact Subset of REAL,
Dab be 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;
A5: D is non empty
proof
2 - 1 <= len Dab - 1 by A1,XREAL_1:13;
hence thesis by A3;
end;
A4: D is non empty increasing
proof
D is increasing
proof
now
let e1,e2 be 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
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.];
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;
end;
hence thesis by A3,A4,INTEGRA1:def 2;
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 be Real, jauge be 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*>, 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;
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;
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;
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;
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
given 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;
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;
dom jauge = [.a,b.] by FUNCT_2:def 1;
then T2.i in dom jauge by A7,A55;
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,A57;
end;
end;
end;
hence P[c];
end;
hence thesis by A2;
end;
end;
c = b
proof
assume
A58: 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;
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;
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
given 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;
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;
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;
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 Th47:
for I being non empty closed_interval Subset of REAL,
jauge being positive-yielding Function of I,REAL holds
ex TD being tagged_division of I st TD is jauge-fine
proof
let I be non empty closed_interval Subset of REAL,
jauge be 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;
1 <= v1 by A11,FINSEQ_3:25; then
per cases by XXREAL_0:1;
suppose v1 = 1;
hence thesis by A1,A2,A4,A12,XXREAL_1:1;
end;
suppose
A14: 1 < v1;
v1 <= len x by A11,FINSEQ_3:25; then
per cases by XXREAL_0:1;
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;
1 <= e1 by FINSEQ_3:25,A16; then
per cases by XXREAL_0:1;
suppose
A20: e1 = 1;
1 <= e2 by FINSEQ_3:25,A17; then
per cases by XXREAL_0:1;
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;
1 <= i by FINSEQ_3:25,A30; then
per cases by XXREAL_0:1;
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 by Def3;
take TD;
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;
1 <= i by FINSEQ_3:25,A36; then
per cases by XXREAL_0:1;
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;
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 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;
registration
let I be non empty closed_interval Subset of REAL,
jauge be positive-yielding Function of I,REAL;
cluster jauge-fine for tagged_division of I;
existence by Th47;
end;