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,FINSEQ_1:def 8;
then c in [.a.i,b.i.] by A10,A11,FINSEQ_1:def 8;
hence a.i <= c <= b.i by XXREAL_1:1;
end;
hence for j be Nat holds a.j <= c <= b.j;
thus ex k be Nat st c - r < a.k & b.k < c + r
proof
A16: IntervalSequence(a,b) is SetSequence of Euclid 1 by Th17; then
A17: for i being Nat holds
a.i <= b.i & a.i <= a.(i+1) & b.(i+1) <= b.i by A2,A3,Th28;
reconsider S = IntervalSequence(a,b) as
non-empty pointwise_bounded closed
SetSequence of (Euclid 1) by A17,Th22;
A18: diameter S is convergent & lim diameter S = 0 by A2,A3,Th31;
consider m0 be Nat such that
A19: for l be Nat st m0 <= l holds |.(diameter S).l - 0.| < r
by A1,A18,SEQ_2:def 7;
a.m0 <= b.m0 by A16,A2,A3,Th28;
then a.m0 - a.m0 <= b.m0 - a.m0 by XREAL_1:9;
then |.b.m0 - a.m0.| = b.m0 - a.m0 by ABSVALUE:def 1;
then |.(diameter S).m0 - 0.| = b.m0 - a.m0 by A2,A3,Th28; then
A20: b.m0 - a.m0 < r by A19;
c - a.m0 <= b.m0 - a.m0 by A12,XREAL_1:9; then
A21: c - a.m0 < r by A20,XXREAL_0:2;
take m0;
c - a.m0 + a.m0 < r + a.m0 by A21,XREAL_1:8;
then c - r < a.m0 + r - r by XREAL_1:9;
hence c - r < a.m0;
b.m0 - c <= b.m0 - a.m0 by A12,XREAL_1:10;
then b.m0 -c < r by A20,XXREAL_0:2;
then b.m0 - c + c < r + c by XREAL_1:8;
hence b.m0 < c +r;
end;
end;
begin :: Tagged division
theorem Th33:
for I being non empty closed_interval Subset of REAL
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 by FINSEQ_1:def 8;
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 FINSEQ_1:def 8,A2,JORDAN5A:19;
b in [.a,b.] by A2,XXREAL_1:1;
hence <*b*>.i in divset(B,i) by A8,A6,A5,FINSEQ_1:def 8;
end;
end;
then reconsider T = <*b*> as Element of set_of_tagged_Division(B)
by Def2;
take [B,T];
thus thesis;
end;
end;
definition
let I 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 by FINSEQ_1:def 8;
hence thesis by Th1;
end;
theorem
for s1,s2 being non empty increasing FinSequence of REAL,
r being Real st s1.len s1 < r < s2.1
holds s1 ^ <*r*> ^ s2 is non empty increasing FinSequence of REAL
proof
let s1,s2 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