:: Basic Properties of Extended Real Numbers
:: by Andrzej Trybulec, Yatsuka Nakamura, Artur Korni{\l}owicz and
:: Adam Grabowski
::
:: Received January 22, 2007
:: Copyright (c) 2007-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XXREAL_0, SUBSET_1, NUMBERS, MEMBERED, XBOOLE_0, ARYTM_3, TARSKI,
REAL_1, XXREAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0,
XREAL_0;
constructors NUMBERS, XXREAL_0, XREAL_0, MEMBERED;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, MEMBERED;
expansions XBOOLE_0, MEMBERED;
theorems XBOOLE_0, XXREAL_0, XBOOLE_1, TARSKI, AXIOMS, XREAL_0, XREAL_1,
MEMBERED, ZFMISC_1;
begin
reserve x for set,
p,q,r,s,t,u for ExtReal,
g for Real,
a for Element of ExtREAL;
scheme Conti { P,Q[object] }:
ex s st (for r st P[r] holds r <= s) & for r st Q[r] holds s <= r
provided
A1: for r,s st P[r] & Q[s] holds r <= s
proof
set A = { a : P[a]}, B = { a : Q[a]};
reconsider X = A /\ REAL, Y = B /\ REAL as Subset of REAL by XBOOLE_1:17;
per cases;
suppose
A2: X = {};
per cases;
suppose
A3: +infty in A;
take +infty;
thus for r st P[r] holds r <= +infty by XXREAL_0:3;
ex a st a = +infty & P[a] by A3;
hence thesis by A1;
end;
suppose
A4: not +infty in A;
take -infty;
thus for r st P[r] holds r <= -infty
proof
let r such that
A5: P[r];
r in ExtREAL by XXREAL_0:def 1;
then
A6: r in A by A5;
per cases by A4,A6,XXREAL_0:14;
suppose r = -infty;
hence thesis;
end;
suppose r in REAL;
hence thesis by A2,A6,XBOOLE_0:def 4;
end;
end;
thus thesis by XXREAL_0:5;
end;
end;
suppose
A7: Y = {};
per cases;
suppose
A8: -infty in B;
take -infty;
ex a st a = -infty & Q[a] by A8;
hence for r st P[r] holds r <= -infty by A1;
thus thesis by XXREAL_0:5;
end;
suppose
A9: not -infty in B;
take +infty;
thus for r st P[r] holds r <= +infty by XXREAL_0:3;
let r such that
A10: Q[r];
r in ExtREAL by XXREAL_0:def 1;
then
A11: r in B by A10;
per cases by A9,A11,XXREAL_0:14;
suppose r = +infty;
hence thesis;
end;
suppose r in REAL;
hence thesis by A7,A11,XBOOLE_0:def 4;
end;
end;
end;
suppose that
A12: X <> {} and
A13: Y <> {};
for x,y being Real st x in X & y in Y holds x <= y
proof
let x,y be Real;
assume x in X;
then x in A by XBOOLE_0:def 4;
then
A14: ex a st ( a = x)&( P[a]);
assume y in Y;
then y in B by XBOOLE_0:def 4;
then ex a st a = y & Q[a];
hence thesis by A1,A14;
end;
then consider s being Real such that
A15: for x,y being Real st x in X & y in Y holds x <= s & s <= y
by AXIOMS:1;
reconsider s as ExtReal;
take s;
thus for r st P[r] holds r <= s
proof
let r;
consider x being Element of REAL such that
A16: x in Y by A13;
x in B by A16,XBOOLE_0:def 4;
then
A17: ex a st x = a & Q[a];
assume
A18: P[r];
per cases by A1,A17,A18,XXREAL_0:13;
suppose
A19: r in REAL;
then reconsider r as Real;
r is Element of ExtREAL by XXREAL_0:def 1;
then r in A by A18;
then r in X by A19,XBOOLE_0:def 4;
hence thesis by A15,A16;
end;
suppose r = -infty;
hence thesis by XXREAL_0:5;
end;
end;
let r;
consider x being Element of REAL such that
A20: x in X by A12;
x in A by A20,XBOOLE_0:def 4;
then
A21: ex a st x = a & P[a];
assume
A22: Q[r];
per cases by A1,A21,A22,XXREAL_0:10;
suppose
A23: r in REAL;
then reconsider r as Real;
r is Element of ExtREAL by XXREAL_0:def 1;
then r in B by A22;
then r in Y by A23,XBOOLE_0:def 4;
hence thesis by A15,A20;
end;
suppose r = +infty;
hence thesis by XXREAL_0:3;
end;
end;
end;
begin :: Intervals
definition
let r,s be ExtReal;
func [.r,s.] -> set equals
{ a : r <= a & a <= s };
correctness;
func [.r,s.[ -> set equals
{ a : r <= a & a < s };
correctness;
func ].r,s.] -> set equals
{ a : r < a & a <= s };
correctness;
func ].r,s.[ -> set equals
{ a : r < a & a < s };
correctness;
end;
theorem Th1:
t in [.r,s.] iff r <= t & t <= s
proof
hereby
assume t in [.r,s.];
then ex a st a = t & r <= a & a <= s;
hence r <= t & t <= s;
end;
t is Element of ExtREAL by XXREAL_0:def 1;
hence thesis;
end;
theorem Th2:
t in ].r,s.] iff r < t & t <= s
proof
hereby
assume t in ].r,s.];
then ex a st a = t & r < a & a <= s;
hence r < t & t <= s;
end;
t is Element of ExtREAL by XXREAL_0:def 1;
hence thesis;
end;
theorem Th3:
t in [.r,s.[ iff r <= t & t < s
proof
hereby
assume t in [.r,s.[;
then ex a st a = t & r <= a & a < s;
hence r <= t & t < s;
end;
t is Element of ExtREAL by XXREAL_0:def 1;
hence thesis;
end;
theorem Th4:
t in ].r,s.[ iff r < t & t < s
proof
hereby
assume t in ].r,s.[;
then ex a st a = t & r < a & a < s;
hence r < t & t < s;
end;
t is Element of ExtREAL by XXREAL_0:def 1;
hence thesis;
end;
registration
let r,s; :: MEASURE5:11
cluster [.r,s.] -> ext-real-membered;
coherence
proof
let x be object;
assume x in [.r,s.];
then ex a st x = a & r <= a & a <= s;
hence thesis;
end;
cluster [.r,s.[ -> ext-real-membered;
coherence
proof
let x be object;
assume x in [.r,s.[;
then ex a st x = a & r <= a & a < s;
hence thesis;
end;
cluster ].r,s.] -> ext-real-membered;
coherence
proof
let x be object;
assume x in ].r,s.];
then ex a st x = a & r < a & a <= s;
hence thesis;
end;
cluster ].r,s.[ -> ext-real-membered;
coherence
proof
let x be object;
assume x in ].r,s.[;
then ex a st x = a & r < a & a < s;
hence thesis;
end;
end;
theorem Th5:
x in [.p,q.] implies x in ].p,q.[ or x = p or x = q
proof
assume
A1: x in [. p, q .];
then reconsider s = x as ExtReal;
A2: p <= s by A1,Th1;
A3: s <= q by A1,Th1;
A4: p = s or p < s by A2,XXREAL_0:1;
s = q or s < q by A3,XXREAL_0:1;
hence thesis by A4,Th4;
end;
theorem Th6:
x in [.p,q.] implies x in ].p,q.] or x = p
proof
assume
A1: x in [.p,q.];
then reconsider s = x as ExtReal;
A2: p <= s by A1,Th1;
A3: s <= q by A1,Th1;
p = s or p < s by A2,XXREAL_0:1;
hence thesis by A3,Th2;
end;
theorem Th7:
x in [.p,q.] implies x in [.p,q.[ or x = q
proof
assume
A1: x in [.p,q.];
then reconsider s = x as ExtReal;
A2: p <= s by A1,Th1;
s <= q by A1,Th1;
then q = s or s < q by XXREAL_0:1;
hence thesis by A2,Th3;
end;
theorem Th8:
x in [.p,q.[ implies x in ].p,q.[ or x = p
proof
assume
A1: x in [.p,q.[;
then reconsider s = x as ExtReal;
A2: p <= s by A1,Th3;
A3: s < q by A1,Th3;
p = s or p < s by A2,XXREAL_0:1;
hence thesis by A3,Th4;
end;
theorem Th9:
x in ].p,q.] implies x in ].p,q.[ or x = q
proof
assume
A1: x in ].p,q.];
then reconsider s = x as ExtReal;
A2: p < s by A1,Th2;
s <= q by A1,Th2;
then q = s or s < q by XXREAL_0:1;
hence thesis by A2,Th4;
end;
theorem
x in [.p,q.[ implies x in ].p,q.] & x <> q or x = p
proof
assume
A1: x in [.p,q.[;
then reconsider s = x as ExtReal;
A2: p <= s by A1,Th3;
A3: s < q by A1,Th3;
p = s or p < s by A2,XXREAL_0:1;
hence thesis by A3,Th2;
end;
theorem
x in ].p,q.] implies x in [.p,q.[ & x <> p or x = q
proof
assume
A1: x in ].p,q.];
then reconsider s = x as ExtReal;
A2: p < s by A1,Th2;
s <= q by A1,Th2;
then q = s or s < q by XXREAL_0:1;
hence thesis by A2,Th3;
end;
theorem Th12:
x in ].p,q.] implies x in [.p,q.] & x <> p
proof
assume
A1: x in ].p,q.];
then reconsider s = x as ExtReal;
A2: p < s by A1,Th2;
s <= q by A1,Th2;
hence thesis by A2,Th1;
end;
theorem Th13:
x in [.p,q.[ implies x in [.p,q.] & x <> q
proof
assume
A1: x in [.p,q.[;
then reconsider s = x as ExtReal;
A2: p <= s by A1,Th3;
s < q by A1,Th3;
hence thesis by A2,Th1;
end;
theorem Th14:
x in ].p,q.[ implies x in [.p,q.[ & x <> p
proof
assume
A1: x in ].p,q.[;
then reconsider s = x as ExtReal;
A2: p < s by A1,Th4;
s < q by A1,Th4;
hence thesis by A2,Th3;
end;
theorem Th15:
x in ].p,q.[ implies x in ].p,q.] & x <> q
proof
assume
A1: x in ].p,q.[;
then reconsider s = x as ExtReal;
A2: p < s by A1,Th4;
s < q by A1,Th4;
hence thesis by A2,Th2;
end;
theorem Th16:
x in ].p,q.[ implies x in [.p,q.] & x <> p & x <> q
proof
assume
A1: x in ].p,q.[;
then x in ].p,q.] by Th15;
hence thesis by A1,Th12,Th15;
end;
theorem Th17: :: MEASURE5:14
[.r,r.] = {r}
proof
let s;
thus s in [.r,r.] implies s in {r}
proof
assume s in [.r,r.];
then ex a st s = a & r <= a & a <= r;
then s = r by XXREAL_0:1;
hence thesis by TARSKI:def 1;
end;
assume s in {r};
then
A1: s = r by TARSKI:def 1;
reconsider s as Element of ExtREAL by XXREAL_0:def 1;
s <= s;
hence thesis by A1;
end;
theorem Th18: :: MEASURE5:13
[.r,r.[ = {}
proof
let p;
not ex p st p in [.r,r.[
proof
given p such that
A1: p in [.r,r.[;
ex a st p = a & r <= a & a < r by A1;
hence thesis;
end;
hence thesis;
end;
theorem Th19: :: MEASURE5:13
].r,r.] = {}
proof
let p;
thus p in ].r,r.] implies p in {}
proof
assume p in ].r,r.];
then ex a st p = a & r < a & a <= r;
hence thesis;
end;
thus thesis;
end;
theorem Th20: :: MEASURE5:13
].r,r.[ = {}
proof
let p;
thus p in ].r,r.[ implies p in {}
proof
assume p in ].r,r.[;
then ex a st p = a & r < a & a < r;
hence thesis;
end;
thus thesis;
end;
registration
let r;
cluster [.r,r.] -> non empty;
coherence
proof
[.r,r.] = {r} by Th17;
hence thesis;
end;
cluster [.r,r.[ -> empty;
coherence by Th18;
cluster ].r,r.] -> empty;
coherence by Th19;
cluster ].r,r.[ -> empty;
coherence by Th20;
end;
theorem Th21:
].p,q.[ c= ].p,q.]
proof
let s;
assume
A1: s in ].p,q.[;
then
A2: p < s by Th4;
s < q by A1,Th4;
hence thesis by A2,Th2;
end;
theorem Th22:
].p,q.[ c= [.p,q.[
proof
let s;
assume
A1: s in ].p,q.[;
then
A2: p < s by Th4;
s < q by A1,Th4;
hence thesis by A2,Th3;
end;
theorem Th23:
].p,q.] c= [.p,q.]
proof
let s;
assume
A1: s in ].p,q.];
then
A2: p < s by Th2;
s <= q by A1,Th2;
hence thesis by A2,Th1;
end;
theorem Th24:
[.p,q.[ c= [.p,q.]
proof
let s;
assume
A1: s in [.p,q.[;
then
A2: p <= s by Th3;
s < q by A1,Th3;
hence thesis by A2,Th1;
end;
theorem Th25:
].p,q.[ c= [.p,q.]
proof
A1: ].p,q.[ c= [.p,q.[ by Th22;
[.p,q.[ c= [.p,q.] by Th24;
hence thesis by A1;
end;
theorem :: MEASURE5:12,15
p <= q implies ].q,p.] = {}
proof
assume
A1: p <= q;
assume ].q,p.] <> {};
then consider r such that
A2: r in ].q,p.];
A3: q < r by A2,Th2;
r <= p by A2,Th2;
hence contradiction by A1,A3,XXREAL_0:2;
end;
theorem Th27: :: MEASURE5:12,15
p <= q implies [.q,p.[ = {}
proof
assume
A1: p <= q;
assume [.q,p.[ <> {};
then consider r such that
A2: r in [.q,p.[;
A3: q <= r by A2,Th3;
r < p by A2,Th3;
hence contradiction by A1,A3,XXREAL_0:2;
end;
theorem Th28: :: MEASURE5:12,15
p <= q implies ].q,p.[ = {}
proof
assume p <= q;
then [.q,p.[ = {} by Th27;
hence thesis by Th22,XBOOLE_1:3;
end;
theorem Th29: :: MEASURE5:12
p < q implies [.q,p.] = {}
proof
assume
A1: p < q;
assume [.q,p.] <> {};
then consider r such that
A2: r in [.q,p.];
A3: q <= r by A2,Th1;
r <= p by A2,Th1;
hence contradiction by A1,A3,XXREAL_0:2;
end;
theorem
r <= s implies [.r,s.] is non empty by Th1;
theorem
p < q implies [.p,q.[ is non empty by Th3;
theorem
p < q implies ].p,q.] is non empty by Th2;
theorem
p < q implies ].p,q.[ is non empty
proof
assume p < q;
then ex s st p < s & s < q by XREAL_1:227;
hence thesis by Th4;
end;
theorem Th34:
p <= r & s <= q implies [.r,s.] c= [.p,q.]
proof
assume that
A1: p <= r and
A2: s <= q;
let t;
assume
A3: t in [.r,s.];
then
A4: r <= t by Th1;
A5: t <= s by A3,Th1;
A6: p <= t by A1,A4,XXREAL_0:2;
t <= q by A2,A5,XXREAL_0:2;
hence thesis by A6,Th1;
end;
theorem Th35:
p <= r & s <= q implies [.r,s.[ c= [.p,q.]
proof
A1: [.r,s.[ c= [.r,s.] by Th24;
assume that
A2: p <= r and
A3: s <= q;
[.r,s.] c= [.p,q.] by A2,A3,Th34;
hence thesis by A1;
end;
theorem Th36:
p <= r & s <= q implies ].r,s.] c= [.p,q.]
proof
A1: ].r,s.] c= [.r,s.] by Th23;
assume that
A2: p <= r and
A3: s <= q;
[.r,s.] c= [.p,q.] by A2,A3,Th34;
hence thesis by A1;
end;
theorem Th37:
p <= r & s <= q implies ].r,s.[ c= [.p,q.]
proof
A1: ].r,s.[ c= [.r,s.] by Th25;
assume that
A2: p <= r and
A3: s <= q;
[.r,s.] c= [.p,q.] by A2,A3,Th34;
hence thesis by A1;
end;
theorem Th38:
p <= r & s <= q implies [.r,s.[ c= [.p,q.[
proof
assume that
A1: p <= r and
A2: s <= q;
let t;
assume
A3: t in [.r,s.[;
then
A4: r <= t by Th3;
A5: t < s by A3,Th3;
A6: p <= t by A1,A4,XXREAL_0:2;
t < q by A2,A5,XXREAL_0:2;
hence thesis by A6,Th3;
end;
theorem Th39:
p < r & s <= q implies [.r,s.] c= ].p,q.]
proof
assume that
A1: p < r and
A2: s <= q;
let t;
assume
A3: t in [.r,s.];
then
A4: r <= t by Th1;
A5: t <= s by A3,Th1;
A6: p ].p,q.]
proof
assume that
A1: r <= s and
A2: [.r,s.] = ].p,q.];
now
assume r in ].p,q.];
then
A3: p < r by Th2;
s <= q by A1,A2,Th58;
then r <= q by A1,XXREAL_0:2;
then p < q by A3,XXREAL_0:2;
hence contradiction by A2,A3,Th53;
end;
hence contradiction by A1,A2,Th1;
end;
theorem
r <= s implies [.r,s.] <> [.p,q.[
proof
assume that
A1: r <= s and
A2: [.r,s.] = [.p,q.[;
now
assume s in [.p,q.[;
then
A3: s < q by Th3;
p <= r by A1,A2,Th54;
then p <= s by A1,XXREAL_0:2;
then p < q by A3,XXREAL_0:2;
hence contradiction by A2,A3,Th52;
end;
hence contradiction by A1,A2,Th1;
end;
theorem
r <= s implies [.r,s.] <> ].p,q.[
proof
assume that
A1: r <= s and
A2: [.r,s.] = ].p,q.[;
now
assume s in ].p,q.[;
then
A3: s < q by Th4;
p <= r by A1,A2,Th62;
then p <= s by A1,XXREAL_0:2;
then p < q by A3,XXREAL_0:2;
hence contradiction by A2,A3,Th51;
end;
hence contradiction by A1,A2,Th1;
end;
theorem
r < s implies [.r,s.[ <> [.p,q.]
proof
assume that
A1: r < s and
A2: [.r,s.[ = [.p,q.];
A3: not s in [.r,s.[ by Th3;
p <= r by A1,A2,Th52;
then
A4: p <= s by A1,XXREAL_0:2;
s <= q by A1,A2,Th52;
hence contradiction by A2,A3,A4,Th1;
end;
theorem
r < s implies [.r,s.[ <> ].p,q.]
proof
assume that
A1: r < s and
A2: [.r,s.[ = ].p,q.];
A3: not s in [.r,s.[ by Th3;
p <= r by A1,A2,Th60;
then
A4: p < s by A1,XXREAL_0:2;
s <= q by A1,A2,Th60;
hence contradiction by A2,A3,A4,Th2;
end;
theorem
r < s implies [.r,s.[ <> ].p,q.[
proof
assume that
A1: r < s and
A2: [.r,s.[ = ].p,q.[;
now
assume r in ].p,q.[;
then
A3: p < r by Th4;
s <= q by A1,A2,Th64;
then r < q by A1,XXREAL_0:2;
then p < q by A3,XXREAL_0:2;
hence contradiction by A2,A3,Th56;
end;
hence contradiction by A1,A2,Th3;
end;
theorem
r < s implies ].r,s.] <> [.p,q.]
proof
assume that
A1: r < s and
A2: ].r,s.] = [.p,q.];
A3: not r in ].r,s.] by Th2;
A4: p <= r by A1,A2,Th53;
s <= q by A1,A2,Th53;
then r <= q by A1,XXREAL_0:2;
hence contradiction by A2,A3,A4,Th1;
end;
theorem
r < s implies ].r,s.] <> [.p,q.[
proof
assume that
A1: r < s and
A2: ].r,s.] = [.p,q.[;
A3: not r in ].r,s.] by Th2;
A4: p <= r by A1,A2,Th57;
s <= q by A1,A2,Th57;
then r < q by A1,XXREAL_0:2;
hence contradiction by A2,A3,A4,Th3;
end;
theorem
r < s implies ].r,s.] <> ].p,q.[
proof
assume that
A1: r < s and
A2: ].r,s.] = ].p,q.[;
now
assume s in ].p,q.[;
then
A3: s < q by Th4;
p <= r by A1,A2,Th65;
then p <= s by A1,XXREAL_0:2;
then p < q by A3,XXREAL_0:2;
hence contradiction by A2,A3,Th59;
end;
hence contradiction by A1,A2,Th2;
end;
theorem
r < s implies ].r,s.[ <> [.p,q.]
proof
assume that
A1: r < s and
A2: ].r,s.[ = [.p,q.];
A3: not r in ].r,s.[ by Th4;
A4: p <= r by A1,A2,Th51;
s <= q by A1,A2,Th51;
then r <= q by A1,XXREAL_0:2;
hence contradiction by A2,A3,A4,Th1;
end;
theorem
r < s implies ].r,s.[ <> ].p,q.]
proof
assume that
A1: r < s and
A2: ].r,s.[ = ].p,q.];
A3: not s in ].r,s.[ by Th4;
p <= r by A1,A2,Th59;
then
A4: p < s by A1,XXREAL_0:2;
s <= q by A1,A2,Th59;
hence contradiction by A2,A3,A4,Th2;
end;
theorem
r < s implies ].r,s.[ <> [.p,q.[
proof
assume that
A1: r < s and
A2: ].r,s.[ = [.p,q.[;
A3: not r in ].r,s.[ by Th4;
A4: p <= r by A1,A2,Th56;
s <= q by A1,A2,Th56;
then r < q by A1,XXREAL_0:2;
hence contradiction by A2,A3,A4,Th3;
end;
theorem
r <= s & [.r,s.] c< [.p,q.] implies p < r or s < q
proof
assume
A1: r <= s;
assume
A2: [.r,s.] c< [.p,q.];
then
A3: [.r,s.] c= [.p,q.];
then
A4: p <= r by A1,Th50;
A5: s <= q by A1,A3,Th50;
p <> r or s <> q by A2;
hence thesis by A4,A5,XXREAL_0:1;
end;
theorem
r < s & ].r,s.[ c= [.p,q.] implies [.r,s.] c= [.p,q.]
proof
assume that
A1: r < s and
A2: ].r,s.[ c= [.p,q.];
let t;
assume
A3: t in [.r,s.];
per cases by A3,Th5;
suppose t in ].r,s.[;
hence thesis by A2;
end;
suppose
A4: t = r;
then
A5: p <= t by A1,A2,Th51;
s <= q by A1,A2,Th51;
then t <= q by A1,A4,XXREAL_0:2;
hence thesis by A5,Th1;
end;
suppose
A6: t = s;
A7: s <= q by A1,A2,Th51;
p <= r by A1,A2,Th51;
then p <= t by A1,A6,XXREAL_0:2;
hence thesis by A6,A7,Th1;
end;
end;
theorem
r < s implies [.s,p.[ c= ].r,p.[
proof
assume
A1: r < s;
let t;
assume
A2: t in [.s,p.[;
then s <= t by Th3;
then
A3: r < t by A1,XXREAL_0:2;
t < p by A2,Th3;
hence thesis by A3,Th4;
end;
theorem Th85: :: MEASURE5:15
s <= r implies [.r,s.] c= {r} & [.r,s.] c= {s}
proof
assume
A1: s <= r;
thus [.r,s.] c= {r}
proof
let t;
assume
A2: t in [.r,s.];
then
A3: t <= s by Th1;
A4: r <= t by A2,Th1;
t <= r by A1,A3,XXREAL_0:2;
then r = t by A4,XXREAL_0:1;
hence thesis by TARSKI:def 1;
end;
let t;
assume
A5: t in [.r,s.];
then r <= t by Th1;
then
A6: s <= t by A1,XXREAL_0:2;
t <= s by A5,Th1;
then s = t by A6,XXREAL_0:1;
hence thesis by TARSKI:def 1;
end;
theorem
].r,s.[ misses {r,s}
proof
let t;
assume
A1: t in ].r,s.[;
then
A2: r < t by Th4;
t < s by A1,Th4;
hence thesis by A2,TARSKI:def 2;
end;
theorem
[.r,s.[ misses {s}
proof
let t;
assume t in [.r,s.[;
then t < s by Th3;
hence thesis by TARSKI:def 1;
end;
theorem
].r,s.] misses {r}
proof
let t;
assume t in ].r,s.];
then r < t by Th2;
hence thesis by TARSKI:def 1;
end;
theorem
s <= p implies [.r,s.] misses ].p,q.[
proof
assume
A1: s <= p;
let t;
assume t in [.r,s.];
then t <= s by Th1;
then t <= p by A1,XXREAL_0:2;
hence thesis by Th4;
end;
theorem
s <= p implies [.r,s.] misses ].p,q.]
proof
assume
A1: s <= p;
let t;
assume t in [.r,s.];
then t <= s by Th1;
then t <= p by A1,XXREAL_0:2;
hence thesis by Th2;
end;
theorem
s <= p implies ].r,s.] misses ].p,q.[
proof
assume
A1: s <= p;
let t;
assume t in ].r,s.];
then t <= s by Th2;
then t <= p by A1,XXREAL_0:2;
hence thesis by Th4;
end;
theorem
s <= p implies ].r,s.] misses ].p,q.]
proof
assume
A1: s <= p;
let t;
assume t in ].r,s.];
then t <= s by Th2;
then t <= p by A1,XXREAL_0:2;
hence thesis by Th2;
end;
theorem
s <= p implies ].r,s.[ misses [.p,q.]
proof
assume
A1: s <= p;
let t;
assume t in ].r,s.[;
then t < s by Th4;
then t < p by A1,XXREAL_0:2;
hence thesis by Th1;
end;
theorem
s <= p implies ].r,s.[ misses [.p,q.[
proof
assume
A1: s <= p;
let t;
assume t in ].r,s.[;
then t < s by Th4;
then t < p by A1,XXREAL_0:2;
hence thesis by Th3;
end;
theorem
s <= p implies [.r,s.[ misses [.p,q.]
proof
assume
A1: s <= p;
let t;
assume t in [.r,s.[;
then t < s by Th3;
then t < p by A1,XXREAL_0:2;
hence thesis by Th1;
end;
theorem
s <= p implies [.r,s.[ misses [.p,q.[
proof
assume
A1: s <= p;
let t;
assume t in [.r,s.[;
then t < s by Th3;
then t < p by A1,XXREAL_0:2;
hence thesis by Th3;
end;
theorem :: MEASURE5:24
r < p & r < s implies not ].r,s.[ c= [.p,q.]
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.[ by A4,A5,Th4;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th1;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t < s by A6,A8,XXREAL_0:2;
hence t in ].r,s.[ by A7,Th4;
thus thesis by A8,Th1;
end;
end;
theorem :: MEASURE5:38
r < p & r < s implies not [.r,s.[ c= [.p,q.]
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in [.r,s.[ by A4,A5,Th3;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th1;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t < s by A6,A8,XXREAL_0:2;
hence t in [.r,s.[ by A7,Th3;
thus thesis by A8,Th1;
end;
end;
theorem :: MEASURE5:42
r < p & r < s implies not ].r,s.] c= [.p,q.]
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.] by A4,A5,Th2;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th1;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t < s by A6,A8,XXREAL_0:2;
hence t in ].r,s.] by A7,Th2;
thus thesis by A8,Th1;
end;
end;
theorem :: MEASURE5:34
r < p & r <= s implies not [.r,s.] c= [.p,q.]
proof
assume that
A1: r < p and
A2: r <= s;
take t=r;
thus t in [.r,s.] by A2,Th1;
thus thesis by A1,Th1;
end;
theorem :: MEASURE5:26
r < p & r < s implies not ].r,s.[ c= [.p,q.[
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.[ by A4,A5,Th4;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th3;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t < s by A6,A8,XXREAL_0:2;
hence t in ].r,s.[ by A7,Th4;
thus thesis by A8,Th3;
end;
end;
theorem :: MEASURE5:48
r < p & r < s implies not ].r,s.] c= [.p,q.[
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.] by A4,A5,Th2;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th3;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t < s by A6,A8,XXREAL_0:2;
hence t in ].r,s.] by A7,Th2;
thus thesis by A8,Th3;
end;
end;
theorem
r < p & r < s implies not [.r,s.[ c= [.p,q.[
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in [.r,s.[ by A4,A5,Th3;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th3;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t < s by A6,A8,XXREAL_0:2;
hence t in [.r,s.[ by A7,Th3;
thus thesis by A8,Th3;
end;
end;
theorem :: MEASURE5:44
r < p & r <= s implies not [.r,s.] c= [.p,q.[
proof
assume that
A1: r < p and
A2: r <= s;
take t=r;
thus t in [.r,s.] by A2,Th1;
thus thesis by A1,Th3;
end;
theorem :: MEASURE5:30
r < p & r < s implies not ].r,s.[ c= ].p,q.]
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.[ by A4,A5,Th4;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th2;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t < s by A6,A8,XXREAL_0:2;
hence t in ].r,s.[ by A7,Th4;
thus thesis by A8,Th2;
end;
end;
theorem :: MEASURE5:46
r <= p & r < s implies not [.r,s.[ c= ].p,q.]
proof
assume that
A1: r <= p and
A2: r < s;
take t=r;
thus t in [.r,s.[ by A2,Th3;
thus thesis by A1,Th2;
end;
theorem :: MEASURE5:50
r < p & r < s implies not ].r,s.] c= ].p,q.]
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.] by A4,A5,Th2;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th2;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t <= s by A6,A8,XXREAL_0:2;
hence t in ].r,s.] by A7,Th2;
thus thesis by A8,Th2;
end;
end;
theorem :: MEASURE5:40
r <= p & r <= s implies not [.r,s.] c= ].p,q.]
proof
assume that
A1: r <= p and
A2: r <= s;
take r;
thus r in [.r,s.] by A2,Th1;
thus thesis by A1,Th2;
end;
theorem :: MEASURE5:22 :: MEASURE5:36
r <= p & r <= s implies not [.r,s.] c= ].p,q.[
proof
assume that
A1: r <= p and
A2: r <= s;
take r;
thus r in [.r,s.] by A2,Th1;
thus thesis by A1,Th4;
end;
theorem :: MEASURE5:28
r <= p & r < s implies not [.r,s.[ c= ].p,q.[
proof
assume that
A1: r <= p and
A2: r < s;
take r;
thus r in [.r,s.[ by A2,Th3;
thus thesis by A1,Th4;
end;
theorem :: MEASURE5:32
r < p & r < s implies not ].r,s.] c= ].p,q.[
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.] by A4,A5,Th2;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th4;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t <= s by A6,A8,XXREAL_0:2;
hence t in ].r,s.] by A7,Th2;
thus thesis by A8,Th4;
end;
end;
theorem :: MEASURE5:20
r < p & r < s implies not ].r,s.[ c= ].p,q.[
proof
assume that
A1: r < p and
A2: r < s;
per cases;
suppose
A3: s <= p;
consider t such that
A4: r < t and
A5: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.[ by A4,A5,Th4;
t < p by A3,A5,XXREAL_0:2;
hence thesis by Th4;
end;
suppose
A6: p <= s;
consider t such that
A7: r < t and
A8: t < p by A1,XREAL_1:227;
take t;
t < s by A6,A8,XXREAL_0:2;
hence t in ].r,s.[ by A7,Th4;
thus thesis by A8,Th4;
end;
end;
theorem :: MEASURE5:21
q < s & r < s implies not ].r,s.[ c= [.p,q.]
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in ].r,s.[ by A5,Th4;
thus thesis by A4,Th1;
end;
suppose
A6: q <= r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.[ by A7,A8,Th4;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th1;
end;
end;
theorem
q < s & r < s implies not [.r,s.[ c= [.p,q.]
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in [.r,s.[ by A5,Th3;
thus thesis by A4,Th1;
end;
suppose
A6: q <= r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in [.r,s.[ by A7,A8,Th3;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th1;
end;
end;
theorem
q < s & r < s implies not ].r,s.] c= [.p,q.]
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in ].r,s.] by A5,Th2;
thus thesis by A4,Th1;
end;
suppose
A6: q <= r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.] by A7,A8,Th2;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th1;
end;
end;
theorem
q < s & r <= s implies not [.r,s.] c= [.p,q.]
proof
assume that
A1: q < s and
A2: r <= s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in [.r,s.] by A5,Th1;
thus thesis by A4,Th1;
end;
suppose
A6: q < r;
take t=r;
thus t in [.r,s.] by A2,Th1;
thus thesis by A6,Th1;
end;
end;
theorem
q < s & r < s implies not ].r,s.[ c= [.p,q.[
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in ].r,s.[ by A5,Th4;
thus thesis by A4,Th3;
end;
suppose
A6: q < r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.[ by A7,A8,Th4;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th3;
end;
end;
theorem
q <= s & r < s implies not ].r,s.] c= [.p,q.[
proof
assume that
A1: q <= s and
A2: r < s;
take t=s;
thus t in ].r,s.] by A2,Th2;
thus thesis by A1,Th3;
end;
theorem
q < s & r < s implies not [.r,s.[ c= [.p,q.[
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in [.r,s.[ by A5,Th3;
thus thesis by A4,Th3;
end;
suppose
A6: q < r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in [.r,s.[ by A7,A8,Th3;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th3;
end;
end;
theorem
q < s & r < s implies not ].r,s.[ c= ].p,q.]
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in ].r,s.[ by A5,Th4;
thus thesis by A4,Th2;
end;
suppose
A6: q < r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.[ by A7,A8,Th4;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th2;
end;
end;
theorem
q < s & r <= s implies not [.r,s.] c= ].p,q.]
proof
assume that
A1: q < s and
A2: r <= s;
take t=s;
thus t in [.r,s.] by A2,Th1;
thus thesis by A1,Th2;
end;
theorem
q < s & r < s implies not [.r,s.[ c= ].p,q.]
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in [.r,s.[ by A5,Th3;
thus thesis by A4,Th2;
end;
suppose
A6: q < r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in [.r,s.[ by A7,A8,Th3;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th2;
end;
end;
theorem
q < s & r < s implies not ].r,s.] c= ].p,q.]
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in ].r,s.] by A5,Th2;
thus thesis by A4,Th2;
end;
suppose
A6: q < r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.] by A7,A8,Th2;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th2;
end;
end;
theorem
q <= s & r <= s implies not [.r,s.] c= ].p,q.[
proof
assume that
A1: q <= s and
A2: r <= s;
take t=s;
thus t in [.r,s.] by A2,Th1;
thus thesis by A1,Th4;
end;
theorem
q < s & r < s implies not [.r,s.[ c= ].p,q.[
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in [.r,s.[ by A5,Th3;
thus thesis by A4,Th4;
end;
suppose
A6: q < r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in [.r,s.[ by A7,A8,Th3;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th4;
end;
end;
theorem
q <= s & r < s implies not ].r,s.] c= ].p,q.[
proof
assume that
A1: q <= s and
A2: r < s;
take t=s;
thus t in ].r,s.] by A2,Th2;
thus thesis by A1,Th4;
end;
theorem
q < s & r < s implies not ].r,s.[ c= ].p,q.[
proof
assume that
A1: q < s and
A2: r < s;
per cases;
suppose
A3: r <= q;
consider t such that
A4: q < t and
A5: t < s by A1,XREAL_1:227;
take t;
r < t by A3,A4,XXREAL_0:2;
hence t in ].r,s.[ by A5,Th4;
thus thesis by A4,Th4;
end;
suppose
A6: q < r;
consider t such that
A7: r < t and
A8: t < s by A2,XREAL_1:227;
take t;
thus t in ].r,s.[ by A7,A8,Th4;
q < t by A6,A7,XXREAL_0:2;
hence thesis by Th4;
end;
end;
begin :: Boolean operations
theorem Th128:
r <= s implies [.r,s.] = ].r,s.[ \/ {r,s}
proof
assume
A1: r <= s;
let t;
thus t in [.r,s.] implies t in ].r,s.[ \/ {r,s}
proof
assume t in [.r,s.];
then t in ].r,s.[ or t = r or t = s by Th5;
then t in ].r,s.[ or t in {r,s} by TARSKI:def 2;
hence thesis by XBOOLE_0:def 3;
end;
assume t in ].r,s.[ \/ {r,s};
then t in ].r,s.[ or t in {r,s} by XBOOLE_0:def 3;
then t in ].r,s.[ or t = r or t = s by TARSKI:def 2;
hence thesis by A1,Th1,Th16;
end;
theorem Th129:
r <= s implies [.r,s.] = [.r,s.[ \/ {s}
proof
assume
A1: r <= s;
let t;
thus t in [.r,s.] implies t in [.r,s.[ \/ {s}
proof
assume t in [.r,s.];
then t in [.r,s.[ or t = s by Th7;
then t in [.r,s.[ or t in {s} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
assume t in [.r,s.[ \/ {s};
then t in [.r,s.[ or t in {s} by XBOOLE_0:def 3;
then t in [.r,s.[ or t = s by TARSKI:def 1;
hence thesis by A1,Th1,Th13;
end;
theorem Th130:
r <= s implies [.r,s.] = {r} \/ ].r,s.]
proof
assume
A1: r <= s;
let t;
thus t in [.r,s.] implies t in {r} \/ ].r,s.]
proof
assume t in [.r,s.];
then t in ].r,s.] or t = r by Th6;
then t in ].r,s.] or t in {r} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
assume t in {r} \/].r,s.];
then t in ].r,s.] or t in {r} by XBOOLE_0:def 3;
then t in ].r,s.] or t = r by TARSKI:def 1;
hence thesis by A1,Th1,Th12;
end;
theorem Th131:
r < s implies [.r,s.[ = {r} \/ ].r,s.[
proof
assume
A1: r < s;
let t;
thus t in [.r,s.[ implies t in {r} \/ ].r,s.[
proof
assume t in [.r,s.[;
then t in ].r,s.[ or t = r by Th8;
then t in ].r,s.[ or t in {r} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
assume t in {r} \/].r,s.[;
then t in ].r,s.[ or t in {r} by XBOOLE_0:def 3;
then t in ].r,s.[ or t = r by TARSKI:def 1;
hence thesis by A1,Th3,Th14;
end;
theorem Th132:
r < s implies ].r,s.] = ].r,s.[ \/ {s}
proof
assume
A1: r < s;
let t;
thus t in ].r,s.] implies t in ].r,s.[ \/ {s}
proof
assume t in ].r,s.];
then t in ].r,s.[ or t = s by Th9;
then t in ].r,s.[ or t in {s} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
assume t in ].r,s.[ \/ {s};
then t in ].r,s.[ or t in {s} by XBOOLE_0:def 3;
then t in ].r,s.[ or t = s by TARSKI:def 1;
hence thesis by A1,Th2,Th15;
end;
theorem
r <= s implies [.r,s.] \ {r,s} = ].r,s.[
proof
assume r <= s;
then
A1: [.r,s.] = ].r,s.[ \/ {r,s} by Th128;
A2: not r in ].r,s.[ by Th4;
not s in ].r,s.[ by Th4;
hence thesis by A1,A2,ZFMISC_1:121;
end;
theorem
r <= s implies [.r,s.] \ {r} = ].r,s.]
proof
assume r <= s;
then
A1: [.r,s.] = {r} \/ ].r,s.] by Th130;
not r in ].r,s.] by Th2;
hence thesis by A1,ZFMISC_1:117;
end;
theorem
r <= s implies [.r,s.] \ {s} = [.r,s.[
proof
assume r <= s;
then
A1: [.r,s.] = [.r,s.[ \/ {s} by Th129;
not s in [.r,s.[ by Th3;
hence thesis by A1,ZFMISC_1:117;
end;
theorem
r < s implies [.r,s.[ \ {r} = ].r,s.[
proof
assume r < s;
then
A1: [.r,s.[= {r} \/ ].r,s.[ by Th131;
not r in ].r,s.[ by Th4;
hence thesis by A1,ZFMISC_1:117;
end;
theorem
r < s implies ].r,s.] \ {s} = ].r,s.[
proof
assume r < s;
then
A1: ].r,s.] = ].r,s.[ \/ {s} by Th132;
not s in ].r,s.[ by Th4;
hence thesis by A1,ZFMISC_1:117;
end;
theorem
r < s & s < t implies ].r,s.] /\ [.s,t.[ = {s}
proof
assume that
A1: r < s and
A2: s < t;
now
let x be object;
hereby
assume
A3: x in ].r,s.] /\ [.s,t.[;
then reconsider p = x as ExtReal;
A4: p in ].r,s.] by A3,XBOOLE_0:def 4;
p in [.s,t.[ by A3,XBOOLE_0:def 4;
then
A5: s <= p by Th3;
p <= s by A4,Th2;
hence x = s by A5,XXREAL_0:1;
end;
assume
A6: x = s;
A7: s in ].r,s.] by A1,Th2;
s in [.s,t.[ by A2,Th3;
hence x in ].r,s.] /\ [.s,t.[ by A6,A7,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
[.r,s.[ /\ [.p,q.[ = [.max(r,p),min(s,q).[
proof
let t;
thus t in [.r,s.[ /\ [.p,q.[ implies t in [.max(r,p),min(s,q).[
proof
assume
A1: t in [.r,s.[ /\ [.p,q.[;
then
A2: t in [.r,s.[ by XBOOLE_0:def 4;
A3: t in [.p,q.[ by A1,XBOOLE_0:def 4;
A4: r <= t by A2,Th3;
A5: t < s by A2,Th3;
A6: p <= t by A3,Th3;
A7: t < q by A3,Th3;
A8: max(r,p) <= t by A4,A6,XXREAL_0:28;
t < min(s,q) by A5,A7,XXREAL_0:21;
hence thesis by A8,Th3;
end;
assume
A9: t in [.max(r,p),min(s,q).[;
then
A10: max(r,p) <= t by Th3;
A11: t < min(s,q) by A9,Th3;
A12: r <= t by A10,XXREAL_0:30;
A13: p <= t by A10,XXREAL_0:30;
A14: t < s by A11,XXREAL_0:23;
A15: t < q by A11,XXREAL_0:23;
A16: t in [.r,s.[ by A12,A14,Th3;
t in [.p,q.[ by A13,A15,Th3;
hence thesis by A16,XBOOLE_0:def 4;
end;
theorem
[.r,s.] /\ [.p,q.] = [.max(r,p),min(s,q).]
proof
let t;
thus t in [.r,s.] /\ [.p,q.] implies t in [.max(r,p),min(s,q).]
proof
assume
A1: t in [.r,s.] /\ [.p,q.];
then
A2: t in [.r,s.] by XBOOLE_0:def 4;
A3: t in [.p,q.] by A1,XBOOLE_0:def 4;
A4: r <= t by A2,Th1;
A5: t <= s by A2,Th1;
A6: p <= t by A3,Th1;
A7: t <= q by A3,Th1;
A8: max(r,p) <= t by A4,A6,XXREAL_0:28;
t <= min(s,q) by A5,A7,XXREAL_0:20;
hence thesis by A8,Th1;
end;
assume
A9: t in [.max(r,p),min(s,q).];
then
A10: max(r,p) <= t by Th1;
A11: t <= min(s,q) by A9,Th1;
A12: r <= t by A10,XXREAL_0:30;
A13: p <= t by A10,XXREAL_0:30;
A14: t <= s by A11,XXREAL_0:22;
A15: t <= q by A11,XXREAL_0:22;
A16: t in [.r,s.] by A12,A14,Th1;
t in [.p,q.] by A13,A15,Th1;
hence thesis by A16,XBOOLE_0:def 4;
end;
theorem
].r,s.] /\ ].p,q.] = ].max(r,p),min(s,q).]
proof
let t;
thus t in ].r,s.] /\ ].p,q.] implies t in ].max(r,p),min(s,q).]
proof
assume
A1: t in ].r,s.] /\ ].p,q.];
then
A2: t in ].r,s.] by XBOOLE_0:def 4;
A3: t in ].p,q.] by A1,XBOOLE_0:def 4;
A4: r < t by A2,Th2;
A5: t <= s by A2,Th2;
A6: p < t by A3,Th2;
A7: t <= q by A3,Th2;
A8: max(r,p) < t by A4,A6,XXREAL_0:29;
t <= min(s,q) by A5,A7,XXREAL_0:20;
hence thesis by A8,Th2;
end;
assume
A9: t in ].max(r,p),min(s,q).];
then
A10: max(r,p) < t by Th2;
A11: t <= min(s,q) by A9,Th2;
A12: r < t by A10,XXREAL_0:31;
A13: p < t by A10,XXREAL_0:31;
A14: t <= s by A11,XXREAL_0:22;
A15: t <= q by A11,XXREAL_0:22;
A16: t in ].r,s.] by A12,A14,Th2;
t in ].p,q.] by A13,A15,Th2;
hence thesis by A16,XBOOLE_0:def 4;
end;
theorem
].r,s.[ /\ ].p,q.[ = ].max(r,p),min(s,q).[
proof
let t;
thus t in ].r,s.[ /\ ].p,q.[ implies t in ].max(r,p),min(s,q).[
proof
assume
A1: t in ].r,s.[ /\ ].p,q.[;
then
A2: t in ].r,s.[ by XBOOLE_0:def 4;
A3: t in ].p,q.[ by A1,XBOOLE_0:def 4;
A4: r < t by A2,Th4;
A5: t < s by A2,Th4;
A6: p < t by A3,Th4;
A7: t < q by A3,Th4;
A8: max(r,p) < t by A4,A6,XXREAL_0:29;
t < min(s,q) by A5,A7,XXREAL_0:21;
hence thesis by A8,Th4;
end;
assume
A9: t in ].max(r,p),min(s,q).[;
then
A10: max(r,p) < t by Th4;
A11: t < min(s,q) by A9,Th4;
A12: r < t by A10,XXREAL_0:31;
A13: p < t by A10,XXREAL_0:31;
A14: t < s by A11,XXREAL_0:23;
A15: t < q by A11,XXREAL_0:23;
A16: t in ].r,s.[ by A12,A14,Th4;
t in ].p,q.[ by A13,A15,Th4;
hence thesis by A16,XBOOLE_0:def 4;
end;
theorem
r <= p & s <= q implies [.r,s.] /\ [.p,q.] = [.p,s.]
proof
assume that
A1: r <= p and
A2: s <= q;
let t;
thus t in [.r,s.] /\ [.p,q.] implies t in [.p,s.]
proof
assume
A3: t in [.r,s.] /\ [.p,q.];
then
A4: t in [.r,s.] by XBOOLE_0:def 4;
A5: t in [.p,q.] by A3,XBOOLE_0:def 4;
A6: t <= s by A4,Th1;
p <= t by A5,Th1;
hence thesis by A6,Th1;
end;
assume
A7: t in [.p,s.];
then
A8: p <= t by Th1;
A9: t <= s by A7,Th1;
A10: r <= t by A1,A8,XXREAL_0:2;
A11: t <= q by A2,A9,XXREAL_0:2;
A12: t in [.r,s.] by A9,A10,Th1;
t in [.p,q.] by A8,A11,Th1;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r <= p & s <= q implies [.r,s.[ /\ [.p,q.] = [.p,s.[
proof
assume that
A1: r <= p and
A2: s <= q;
let t;
thus t in [.r,s.[ /\ [.p,q.] implies t in [.p,s.[
proof
assume
A3: t in [.r,s.[ /\ [.p,q.];
then
A4: t in [.r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.] by A3,XBOOLE_0:def 4;
A6: t < s by A4,Th3;
p <= t by A5,Th1;
hence thesis by A6,Th3;
end;
assume
A7: t in [.p,s.[;
then
A8: p <= t by Th3;
A9: t < s by A7,Th3;
A10: r <= t by A1,A8,XXREAL_0:2;
A11: t <= q by A2,A9,XXREAL_0:2;
A12: t in [.r,s.[ by A9,A10,Th3;
t in [.p,q.] by A8,A11,Th1;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r >= p & s > q implies [.r,s.[ /\ [.p,q.] = [.r,q.]
proof
assume that
A1: r >= p and
A2: s > q;
let t;
thus t in [.r,s.[ /\ [.p,q.] implies t in [.r,q.]
proof
assume
A3: t in [.r,s.[ /\ [.p,q.];
then
A4: t in [.r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.] by A3,XBOOLE_0:def 4;
A6: r <= t by A4,Th3;
t <= q by A5,Th1;
hence thesis by A6,Th1;
end;
assume
A7: t in [.r,q.];
then
A8: r <= t by Th1;
A9: t <= q by A7,Th1;
then
A10: t < s by A2,XXREAL_0:2;
A11: p <= t by A1,A8,XXREAL_0:2;
A12: t in [.r,s.[ by A8,A10,Th3;
t in [.p,q.] by A9,A11,Th1;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r < p & s <= q implies ].r,s.] /\ [.p,q.] = [.p,s.]
proof
assume that
A1: r < p and
A2: s <= q;
let t;
thus t in ].r,s.] /\ [.p,q.] implies t in [.p,s.]
proof
assume
A3: t in ].r,s.] /\ [.p,q.];
then
A4: t in ].r,s.] by XBOOLE_0:def 4;
A5: t in [.p,q.] by A3,XBOOLE_0:def 4;
A6: t <= s by A4,Th2;
p <= t by A5,Th1;
hence thesis by A6,Th1;
end;
assume
A7: t in [.p,s.];
then
A8: p <= t by Th1;
A9: t <= s by A7,Th1;
A10: r < t by A1,A8,XXREAL_0:2;
A11: t <= q by A2,A9,XXREAL_0:2;
A12: t in ].r,s.] by A9,A10,Th2;
t in [.p,q.] by A8,A11,Th1;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r >= p & s >= q implies ].r,s.] /\ [.p,q.] = ].r,q.]
proof
assume that
A1: r >= p and
A2: s >= q;
let t;
thus t in ].r,s.] /\ [.p,q.] implies t in ].r,q.]
proof
assume
A3: t in ].r,s.] /\ [.p,q.];
then
A4: t in ].r,s.] by XBOOLE_0:def 4;
A5: t in [.p,q.] by A3,XBOOLE_0:def 4;
A6: r < t by A4,Th2;
t <= q by A5,Th1;
hence thesis by A6,Th2;
end;
assume
A7: t in ].r,q.];
then
A8: r < t by Th2;
A9: t <= q by A7,Th2;
then
A10: t <= s by A2,XXREAL_0:2;
A11: p <= t by A1,A8,XXREAL_0:2;
A12: t in ].r,s.] by A8,A10,Th2;
t in [.p,q.] by A9,A11,Th1;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r < p & s <= q implies ].r,s.[ /\ [.p,q.] = [.p,s.[
proof
assume that
A1: r < p and
A2: s <= q;
let t;
thus t in ].r,s.[ /\ [.p,q.] implies t in [.p,s.[
proof
assume
A3: t in ].r,s.[ /\ [.p,q.];
then
A4: t in ].r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.] by A3,XBOOLE_0:def 4;
A6: t < s by A4,Th4;
p <= t by A5,Th1;
hence thesis by A6,Th3;
end;
assume
A7: t in [.p,s.[;
then
A8: p <= t by Th3;
A9: t < s by A7,Th3;
A10: r < t by A1,A8,XXREAL_0:2;
A11: t <= q by A2,A9,XXREAL_0:2;
A12: t in ].r,s.[ by A9,A10,Th4;
t in [.p,q.] by A8,A11,Th1;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r >= p & s > q implies ].r,s.[ /\ [.p,q.] = ].r,q.]
proof
assume that
A1: r >= p and
A2: s > q;
let t;
thus t in ].r,s.[ /\ [.p,q.] implies t in ].r,q.]
proof
assume
A3: t in ].r,s.[ /\ [.p,q.];
then
A4: t in ].r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.] by A3,XBOOLE_0:def 4;
A6: r < t by A4,Th4;
t <= q by A5,Th1;
hence thesis by A6,Th2;
end;
assume
A7: t in ].r,q.];
then
A8: r < t by Th2;
A9: t <= q by A7,Th2;
then
A10: t < s by A2,XXREAL_0:2;
A11: p <= t by A1,A8,XXREAL_0:2;
A12: t in ].r,s.[ by A8,A10,Th4;
t in [.p,q.] by A9,A11,Th1;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r <= p & s <= q implies [.r,s.[ /\ [.p,q.[ = [.p,s.[
proof
assume that
A1: r <= p and
A2: s <= q;
let t;
thus t in [.r,s.[ /\ [.p,q.[ implies t in [.p,s.[
proof
assume
A3: t in [.r,s.[ /\ [.p,q.[;
then
A4: t in [.r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.[ by A3,XBOOLE_0:def 4;
A6: t < s by A4,Th3;
p <= t by A5,Th3;
hence thesis by A6,Th3;
end;
assume
A7: t in [.p,s.[;
then
A8: p <= t by Th3;
A9: t < s by A7,Th3;
A10: r <= t by A1,A8,XXREAL_0:2;
A11: t < q by A2,A9,XXREAL_0:2;
A12: t in [.r,s.[ by A9,A10,Th3;
t in [.p,q.[ by A8,A11,Th3;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r >= p & s >= q implies [.r,s.[ /\ [.p,q.[ = [.r,q.[
proof
assume that
A1: r >= p and
A2: s >= q;
let t;
thus t in [.r,s.[ /\ [.p,q.[ implies t in [.r,q.[
proof
assume
A3: t in [.r,s.[ /\ [.p,q.[;
then
A4: t in [.r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.[ by A3,XBOOLE_0:def 4;
A6: r <= t by A4,Th3;
t < q by A5,Th3;
hence thesis by A6,Th3;
end;
assume
A7: t in [.r,q.[;
then
A8: r <= t by Th3;
A9: t < q by A7,Th3;
then
A10: t < s by A2,XXREAL_0:2;
A11: p <= t by A1,A8,XXREAL_0:2;
A12: t in [.r,s.[ by A8,A10,Th3;
t in [.p,q.[ by A9,A11,Th3;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem Th152:
r < p & s < q implies ].r,s.] /\ [.p,q.[ = [.p,s.]
proof
assume that
A1: r < p and
A2: s < q;
let t;
thus t in ].r,s.] /\ [.p,q.[ implies t in [.p,s.]
proof
assume
A3: t in ].r,s.] /\ [.p,q.[;
then
A4: t in ].r,s.] by XBOOLE_0:def 4;
A5: t in [.p,q.[ by A3,XBOOLE_0:def 4;
A6: t <= s by A4,Th2;
p <= t by A5,Th3;
hence thesis by A6,Th1;
end;
assume
A7: t in [.p,s.];
then
A8: p <= t by Th1;
A9: t <= s by A7,Th1;
A10: r < t by A1,A8,XXREAL_0:2;
A11: t < q by A2,A9,XXREAL_0:2;
A12: t in ].r,s.] by A9,A10,Th2;
t in [.p,q.[ by A8,A11,Th3;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r >= p & s >= q implies ].r,s.] /\ [.p,q.[ = ].r,q.[
proof
assume that
A1: r >= p and
A2: s >= q;
let t;
thus t in ].r,s.] /\ [.p,q.[ implies t in ].r,q.[
proof
assume
A3: t in ].r,s.] /\ [.p,q.[;
then
A4: t in ].r,s.] by XBOOLE_0:def 4;
A5: t in [.p,q.[ by A3,XBOOLE_0:def 4;
A6: r < t by A4,Th2;
t < q by A5,Th3;
hence thesis by A6,Th4;
end;
assume
A7: t in ].r,q.[;
then
A8: r < t by Th4;
A9: t < q by A7,Th4;
then
A10: t <= s by A2,XXREAL_0:2;
A11: p <= t by A1,A8,XXREAL_0:2;
A12: t in ].r,s.] by A8,A10,Th2;
t in [.p,q.[ by A9,A11,Th3;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem Th154:
r < p & s <= q implies ].r,s.[ /\ [.p,q.[ = [.p,s.[
proof
assume that
A1: r < p and
A2: s <= q;
let t;
thus t in ].r,s.[ /\ [.p,q.[ implies t in [.p,s.[
proof
assume
A3: t in ].r,s.[ /\ [.p,q.[;
then
A4: t in ].r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.[ by A3,XBOOLE_0:def 4;
A6: t < s by A4,Th4;
p <= t by A5,Th3;
hence thesis by A6,Th3;
end;
assume
A7: t in [.p,s.[;
then
A8: p <= t by Th3;
A9: t < s by A7,Th3;
A10: r < t by A1,A8,XXREAL_0:2;
A11: t < q by A2,A9,XXREAL_0:2;
A12: t in ].r,s.[ by A9,A10,Th4;
t in [.p,q.[ by A8,A11,Th3;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r >= p & s >= q implies ].r,s.[ /\ [.p,q.[ = ].r,q.[
proof
assume that
A1: r >= p and
A2: s >= q;
let t;
thus t in ].r,s.[ /\ [.p,q.[ implies t in ].r,q.[
proof
assume
A3: t in ].r,s.[ /\ [.p,q.[;
then
A4: t in ].r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.[ by A3,XBOOLE_0:def 4;
A6: r < t by A4,Th4;
t < q by A5,Th3;
hence thesis by A6,Th4;
end;
assume
A7: t in ].r,q.[;
then
A8: r < t by Th4;
A9: t < q by A7,Th4;
then
A10: t < s by A2,XXREAL_0:2;
A11: p <= t by A1,A8,XXREAL_0:2;
A12: t in ].r,s.[ by A8,A10,Th4;
t in [.p,q.[ by A9,A11,Th3;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r <= p & s <= q implies ].r,s.] /\ ].p,q.] = ].p,s.]
proof
assume that
A1: r <= p and
A2: s <= q;
let t;
thus t in ].r,s.] /\ ].p,q.] implies t in ].p,s.]
proof
assume
A3: t in ].r,s.] /\ ].p,q.];
then
A4: t in ].r,s.] by XBOOLE_0:def 4;
A5: t in ].p,q.] by A3,XBOOLE_0:def 4;
A6: t <= s by A4,Th2;
p < t by A5,Th2;
hence thesis by A6,Th2;
end;
assume
A7: t in ].p,s.];
then
A8: p < t by Th2;
A9: t <= s by A7,Th2;
A10: r < t by A1,A8,XXREAL_0:2;
A11: t <= q by A2,A9,XXREAL_0:2;
A12: t in ].r,s.] by A9,A10,Th2;
t in ].p,q.] by A8,A11,Th2;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r >= p & s >= q implies ].r,s.] /\ ].p,q.] = ].r,q.]
proof
assume that
A1: r >= p and
A2: s >= q;
let t;
thus t in ].r,s.] /\ ].p,q.] implies t in ].r,q.]
proof
assume
A3: t in ].r,s.] /\ ].p,q.];
then
A4: t in ].r,s.] by XBOOLE_0:def 4;
A5: t in ].p,q.] by A3,XBOOLE_0:def 4;
A6: r < t by A4,Th2;
t <= q by A5,Th2;
hence thesis by A6,Th2;
end;
assume
A7: t in ].r,q.];
then
A8: r < t by Th2;
A9: t <= q by A7,Th2;
then
A10: t <= s by A2,XXREAL_0:2;
A11: p < t by A1,A8,XXREAL_0:2;
A12: t in ].r,s.] by A8,A10,Th2;
t in ].p,q.] by A9,A11,Th2;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
r <= p & s <= q implies ].r,s.[ /\ ].p,q.] = ].p,s.[
proof
assume that
A1: r <= p and
A2: s <= q;
let t;
thus t in ].r,s.[ /\ ].p,q.] implies t in ].p,s.[
proof
assume
A3: t in ].r,s.[ /\ ].p,q.];
then
A4: t in ].r,s.[ by XBOOLE_0:def 4;
A5: t in ].p,q.] by A3,XBOOLE_0:def 4;
A6: t < s by A4,Th4;
p < t by A5,Th2;
hence thesis by A6,Th4;
end;
assume
A7: t in ].p,s.[;
then
A8: p < t by Th4;
A9: t < s by A7,Th4;
A10: r < t by A1,A8,XXREAL_0:2;
A11: t <= q by A2,A9,XXREAL_0:2;
A12: t in ].r,s.[ by A9,A10,Th4;
t in ].p,q.] by A8,A11,Th2;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem Th159:
r >= p & s > q implies ].r,s.[ /\ ].p,q.] = ].r,q.]
proof
assume that
A1: r >= p and
A2: s > q;
let t;
thus t in ].r,s.[ /\ ].p,q.] implies t in ].r,q.]
proof
assume
A3: t in ].r,s.[ /\ ].p,q.];
then
A4: t in ].r,s.[ by XBOOLE_0:def 4;
A5: t in ].p,q.] by A3,XBOOLE_0:def 4;
A6: r < t by A4,Th4;
t <= q by A5,Th2;
hence thesis by A6,Th2;
end;
assume
A7: t in ].r,q.];
then
A8: r < t by Th2;
A9: t <= q by A7,Th2;
then
A10: t < s by A2,XXREAL_0:2;
A11: p < t by A1,A8,XXREAL_0:2;
A12: t in ].r,s.[ by A8,A10,Th4;
t in ].p,q.] by A9,A11,Th2;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem Th160:
r <= p & s <= q implies ].r,s.[ /\ ].p,q.[ = ].p,s.[
proof
assume that
A1: r <= p and
A2: s <= q;
let t;
thus t in ].r,s.[ /\ ].p,q.[ implies t in ].p,s.[
proof
assume
A3: t in ].r,s.[ /\ ].p,q.[;
then
A4: t in ].r,s.[ by XBOOLE_0:def 4;
A5: t in ].p,q.[ by A3,XBOOLE_0:def 4;
A6: t < s by A4,Th4;
p < t by A5,Th4;
hence thesis by A6,Th4;
end;
assume
A7: t in ].p,s.[;
then
A8: p < t by Th4;
A9: t < s by A7,Th4;
A10: r < t by A1,A8,XXREAL_0:2;
A11: t < q by A2,A9,XXREAL_0:2;
A12: t in ].r,s.[ by A9,A10,Th4;
t in ].p,q.[ by A8,A11,Th4;
hence thesis by A12,XBOOLE_0:def 4;
end;
theorem
[.r,s.[ \/ [.p,q.[ c= [.min(r,p),max(s,q).[
proof
let t;
assume t in [.r,s.[ \/ [.p,q.[;
then t in [.r,s.[ or t in [.p,q.[ by XBOOLE_0:def 3;
then
A1: r <= t & t < s or p <= t & t < q by Th3;
then
A2: min(r,p) <= t by XXREAL_0:23;
t < max(s,q) by A1,XXREAL_0:30;
hence thesis by A2,Th3;
end;
theorem
[.r,s.[ meets [.p,q.[ implies [.r,s.[ \/ [.p,q.[ = [.min(r,p),max(s,q).[
proof
assume [.r,s.[ meets [.p,q.[;
then consider u such that
A1: u in [.r,s.[ and
A2: u in [.p,q.[;
let t;
thus t in [.r,s.[ \/ [.p,q.[ implies t in [.min(r,p),max(s,q).[
proof
assume t in [.r,s.[ \/ [.p,q.[;
then t in [.r,s.[ or t in [.p,q.[ by XBOOLE_0:def 3;
then
A3: r <= t & t < s or p <= t & t < q by Th3;
then
A4: min(r,p) <= t by XXREAL_0:23;
t < max(s,q) by A3,XXREAL_0:30;
hence thesis by A4,Th3;
end;
A5: r <= u by A1,Th3;
A6: u < s by A1,Th3;
A7: p <= u by A2,Th3;
A8: u < q by A2,Th3;
assume
A9: t in [.min(r,p),max(s,q).[;
then
A10: min(r,p) <= t by Th3;
A11: t < max(s,q) by A9,Th3;
per cases by A10,A11,XXREAL_0:21,28;
suppose r <= t & t < s or p <= t & t < q;
then t in [.r,s.[ or t in [.p,q.[ by Th3;
hence thesis by XBOOLE_0:def 3;
end;
suppose that
A12: p <= t and
A13: t < s;
u <= t or t <= u;
then r <= t or t < q by A5,A8,XXREAL_0:2;
then t in [.r,s.[ or t in [.p,q.[ by A12,A13,Th3;
hence thesis by XBOOLE_0:def 3;
end;
suppose that
A14: r <= t and
A15: t < q;
u <= t or t <= u;
then t < s or p <= t by A6,A7,XXREAL_0:2;
then t in [.r,s.[ or t in [.p,q.[ by A14,A15,Th3;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem
].r,s.] \/ ].p,q.] c= ].min(r,p),max(s,q).]
proof
let t;
assume t in ].r,s.] \/ ].p,q.];
then t in ].r,s.] or t in ].p,q.] by XBOOLE_0:def 3;
then
A1: r < t & t <= s or p < t & t <= q by Th2;
then
A2: min(r,p) < t by XXREAL_0:22;
t <= max(s,q) by A1,XXREAL_0:31;
hence thesis by A2,Th2;
end;
theorem
].r,s.] meets ].p,q.] implies ].r,s.] \/ ].p,q.] = ].min(r,p),max(s,q).]
proof
assume ].r,s.] meets ].p,q.];
then consider u such that
A1: u in ].r,s.] and
A2: u in ].p,q.];
let t;
thus t in ].r,s.] \/ ].p,q.] implies t in ].min(r,p),max(s,q).]
proof
assume t in ].r,s.] \/ ].p,q.];
then t in ].r,s.] or t in ].p,q.] by XBOOLE_0:def 3;
then
A3: r < t & t <= s or p < t & t <= q by Th2;
then
A4: min(r,p) < t by XXREAL_0:22;
t <= max(s,q) by A3,XXREAL_0:31;
hence thesis by A4,Th2;
end;
A5: r < u by A1,Th2;
A6: u <= s by A1,Th2;
A7: p < u by A2,Th2;
A8: u <= q by A2,Th2;
assume
A9: t in ].min(r,p),max(s,q).];
then
A10: min(r,p) < t by Th2;
A11: t <= max(s,q) by A9,Th2;
per cases by A10,A11,XXREAL_0:20,29;
suppose r < t & t <= s or p < t & t <= q;
then t in ].r,s.] or t in ].p,q.] by Th2;
hence thesis by XBOOLE_0:def 3;
end;
suppose that
A12: p < t and
A13: t <= s;
u <= t or t <= u;
then r < t or t <= q by A5,A8,XXREAL_0:2;
then t in ].r,s.] or t in ].p,q.] by A12,A13,Th2;
hence thesis by XBOOLE_0:def 3;
end;
suppose that
A14: r < t and
A15: t <= q;
u <= t or t <= u;
then t <= s or p < t by A6,A7,XXREAL_0:2;
then t in ].r,s.] or t in ].p,q.] by A14,A15,Th2;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem
r <= s & s <= t implies [.r,s.] \/ [.s,t.] = [.r,t.]
proof
assume that
A1: r <= s and
A2: s <= t;
let p;
thus p in [.r,s.] \/ [.s,t.] implies p in [.r,t.]
proof
assume p in [.r,s.] \/ [.s,t.];
then p in [.r,s.] or p in [.s,t.] by XBOOLE_0:def 3;
then
A3: r <= p & p <= s or s <= p & p <= t by Th1;
then
A4: r <= p by A1,XXREAL_0:2;
p <= t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th1;
end;
assume p in [.r,t.];
then r <= p & p <= s or s <= p & p <= t by Th1;
then p in [.r,s.] or p in [.s,t.] by Th1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th166:
r <= s & s <= t implies [.r,s.[ \/ [.s,t.] = [.r,t.]
proof
assume that
A1: r <= s and
A2: s <= t;
let p;
thus p in [.r,s.[ \/ [.s,t.] implies p in [.r,t.]
proof
assume p in [.r,s.[ \/ [.s,t.];
then p in [.r,s.[ or p in [.s,t.] by XBOOLE_0:def 3;
then
A3: r <= p & p < s or s <= p & p <= t by Th1,Th3;
then
A4: r <= p by A1,XXREAL_0:2;
p <= t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th1;
end;
assume p in [.r,t.];
then r <= p & p < s or s <= p & p <= t by Th1;
then p in [.r,s.[ or p in [.s,t.] by Th1,Th3;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th167:
r <= s & s <= t implies [.r,s.] \/ ].s,t.] = [.r,t.]
proof
assume that
A1: r <= s and
A2: s <= t;
let p;
thus p in [.r,s.] \/ ].s,t.] implies p in [.r,t.]
proof
assume p in [.r,s.] \/ ].s,t.];
then p in [.r,s.] or p in ].s,t.] by XBOOLE_0:def 3;
then
A3: r <= p & p <= s or s < p & p <= t by Th1,Th2;
then
A4: r <= p by A1,XXREAL_0:2;
p <= t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th1;
end;
assume p in [.r,t.];
then r <= p & p <= s or s < p & p <= t by Th1;
then p in [.r,s.] or p in ].s,t.] by Th1,Th2;
hence thesis by XBOOLE_0:def 3;
end;
theorem
r <= s & s <= t implies [.r,s.[ \/ [.s,t.[ = [.r,t.[
proof
assume that
A1: r <= s and
A2: s <= t;
let p;
thus p in [.r,s.[ \/ [.s,t.[ implies p in [.r,t.[
proof
assume p in [.r,s.[ \/ [.s,t.[;
then p in [.r,s.[ or p in [.s,t.[ by XBOOLE_0:def 3;
then
A3: r <= p & p < s or s <= p & p < t by Th3;
then
A4: r <= p by A1,XXREAL_0:2;
p < t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th3;
end;
assume p in [.r,t.[;
then r <= p & p < s or s <= p & p < t by Th3;
then p in [.r,s.[ or p in [.s,t.[ by Th3;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th169:
r <= s & s < t implies [.r,s.] \/ ].s,t.[ = [.r,t.[
proof
assume that
A1: r <= s and
A2: s < t;
let p;
thus p in [.r,s.] \/ ].s,t.[ implies p in [.r,t.[
proof
assume p in [.r,s.] \/ ].s,t.[;
then p in [.r,s.] or p in ].s,t.[ by XBOOLE_0:def 3;
then
A3: r <= p & p <= s or s < p & p < t by Th1,Th4;
then
A4: r <= p by A1,XXREAL_0:2;
p < t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th3;
end;
assume p in [.r,t.[;
then r <= p & p <= s or s < p & p < t by Th3;
then p in [.r,s.] or p in ].s,t.[ by Th1,Th4;
hence thesis by XBOOLE_0:def 3;
end;
theorem
r <= s & s <= t implies ].r,s.] \/ ].s,t.] = ].r,t.]
proof
assume that
A1: r <= s and
A2: s <= t;
let p;
thus p in ].r,s.] \/ ].s,t.] implies p in ].r,t.]
proof
assume p in ].r,s.] \/ ].s,t.];
then p in ].r,s.] or p in ].s,t.] by XBOOLE_0:def 3;
then
A3: r < p & p <= s or s < p & p <= t by Th2;
then
A4: r < p by A1,XXREAL_0:2;
p <= t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th2;
end;
assume p in ].r,t.];
then r < p & p <= s or s < p & p <= t by Th2;
then p in ].r,s.] or p in ].s,t.] by Th2;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th171:
r <= s & s < t implies ].r,s.] \/ ].s,t.[ = ].r,t.[
proof
assume that
A1: r <= s and
A2: s < t;
let p;
thus p in ].r,s.] \/ ].s,t.[ implies p in ].r,t.[
proof
assume p in ].r,s.] \/ ].s,t.[;
then p in ].r,s.] or p in ].s,t.[ by XBOOLE_0:def 3;
then
A3: r < p & p <= s or s < p & p < t by Th2,Th4;
then
A4: r < p by A1,XXREAL_0:2;
p < t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th4;
end;
assume p in ].r,t.[;
then r < p & p <= s or s < p & p < t by Th4;
then p in ].r,s.] or p in ].s,t.[ by Th2,Th4;
hence thesis by XBOOLE_0:def 3;
end;
theorem
r < s & s < t implies ].r,s.] \/ [.s,t.[ = ].r,t.[
proof
assume that
A1: r < s and
A2: s < t;
let p;
thus p in ].r,s.] \/ [.s,t.[ implies p in ].r,t.[
proof
assume p in ].r,s.] \/ [.s,t.[;
then p in ].r,s.] or p in [.s,t.[ by XBOOLE_0:def 3;
then
A3: r < p & p <= s or s <= p & p < t by Th2,Th3;
then
A4: r < p by A1,XXREAL_0:2;
p < t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th4;
end;
assume p in ].r,t.[;
then r < p & p <= s or s < p & p < t by Th4;
then p in ].r,s.] or p in [.s,t.[ by Th2,Th3;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th173:
r < s & s < t implies ].r,s.[ \/ [.s,t.[ = ].r,t.[
proof
assume that
A1: r < s and
A2: s < t;
let p;
thus p in ].r,s.[ \/ [.s,t.[ implies p in ].r,t.[
proof
assume p in ].r,s.[ \/ [.s,t.[;
then p in ].r,s.[ or p in [.s,t.[ by XBOOLE_0:def 3;
then
A3: r < p & p < s or s <= p & p < t by Th3,Th4;
then
A4: r < p by A1,XXREAL_0:2;
p < t by A2,A3,XXREAL_0:2;
hence thesis by A4,Th4;
end;
assume p in ].r,t.[;
then r < p & p < s or s <= p & p < t by Th4;
then p in ].r,s.[ or p in [.s,t.[ by Th3,Th4;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th174:
p <= s & r <= q & s <= r implies [.p,r.] \/ [.s,q.] = [.p,q.]
proof
assume that
A1: p <= s and
A2: r <= q and
A3: s <= r;
let t;
thus t in [.p,r.] \/ [.s,q.] implies t in [.p,q.]
proof
assume t in [.p,r.] \/ [.s,q.];
then t in [.p,r.] or t in [.s,q.] by XBOOLE_0:def 3;
then
A4: p <= t & t <= r or s <= t & t <= q by Th1;
then
A5: p <= t by A1,XXREAL_0:2;
t <= q by A2,A4,XXREAL_0:2;
hence thesis by A5,Th1;
end;
assume t in [.p,q.];
then p <= t & t <= r or s <= t & t <= q by A3,Th1,XXREAL_0:2;
then t in [.p,r.] or t in [.s,q.] by Th1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th175:
p <= s & r <= q & s < r implies [.p,r.[ \/ ].s,q.] = [.p,q.]
proof
assume that
A1: p <= s and
A2: r <= q and
A3: s < r;
let t;
thus t in [.p,r.[ \/ ].s,q.] implies t in [.p,q.]
proof
assume t in [.p,r.[ \/ ].s,q.];
then t in [.p,r.[ or t in ].s,q.] by XBOOLE_0:def 3;
then
A4: p <= t & t <= r or s <= t & t <= q by Th2,Th3;
then
A5: p <= t by A1,XXREAL_0:2;
t <= q by A2,A4,XXREAL_0:2;
hence thesis by A5,Th1;
end;
assume t in [.p,q.];
then p <= t & t < r or s < t & t <= q by A3,Th1,XXREAL_0:2;
then t in [.p,r.[ or t in ].s,q.] by Th2,Th3;
hence thesis by XBOOLE_0:def 3;
end;
theorem
p <= s & s <= r & r < q implies [.p,r.] \/ [.s,q.[ = [.p,q.[
proof
assume that
A1: p <= s and
A2: s <= r and
A3: r < q;
let t;
thus t in [.p,r.] \/ [.s,q.[ implies t in [.p,q.[
proof
assume t in [.p,r.] \/ [.s,q.[;
then t in [.p,r.] or t in [.s,q.[ by XBOOLE_0:def 3;
then
A4: p <= t & t <= r or s <= t & t < q by Th1,Th3;
then
A5: p <= t by A1,XXREAL_0:2;
t < q by A3,A4,XXREAL_0:2;
hence thesis by A5,Th3;
end;
assume t in [.p,q.[;
then p <= t & t <= r or s <= t & t < q by A2,Th3,XXREAL_0:2;
then t in [.p,r.] or t in [.s,q.[ by Th1,Th3;
hence thesis by XBOOLE_0:def 3;
end;
theorem
p < s & r <= q & s <= r implies ].p,r.] \/ [.s,q.] = ].p,q.]
proof
assume that
A1: p < s and
A2: r <= q and
A3: s <= r;
let t;
thus t in ].p,r.] \/ [.s,q.] implies t in ].p,q.]
proof
assume t in ].p,r.] \/ [.s,q.];
then t in ].p,r.] or t in [.s,q.] by XBOOLE_0:def 3;
then
A4: p < t & t <= r or s <= t & t <= q by Th1,Th2;
then
A5: p < t by A1,XXREAL_0:2;
t <= q by A2,A4,XXREAL_0:2;
hence thesis by A5,Th2;
end;
assume t in ].p,q.];
then p < t & t <= r or s <= t & t <= q by A3,Th2,XXREAL_0:2;
then t in ].p,r.] or t in [.s,q.] by Th1,Th2;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th178:
p < s & r < q & s <= r implies ].p,r.] \/ [.s,q.[ = ].p,q.[
proof
assume that
A1: p < s and
A2: r < q and
A3: s <= r;
let t;
thus t in ].p,r.] \/ [.s,q.[ implies t in ].p,q.[
proof
assume t in ].p,r.] \/ [.s,q.[;
then t in ].p,r.] or t in [.s,q.[ by XBOOLE_0:def 3;
then
A4: p < t & t <= r or s <= t & t < q by Th2,Th3;
then
A5: p < t by A1,XXREAL_0:2;
t < q by A2,A4,XXREAL_0:2;
hence thesis by A5,Th4;
end;
assume t in ].p,q.[;
then p < t & t <= r or s <= t & t < q by A3,Th4,XXREAL_0:2;
then t in ].p,r.] or t in [.s,q.[ by Th2,Th3;
hence thesis by XBOOLE_0:def 3;
end;
theorem
p<=r & p<=s & r<=q & s<=q implies [.p,r.[ \/ [.r,s.] \/ ].s,q.] = [.p,q.]
proof
assume that
A1: p <= r and
A2: p <= s and
A3: r <= q and
A4: s <= q;
per cases;
suppose r <= s;
hence [.p,r.[ \/ [.r,s.] \/ ].s,q.] = [.p,s.] \/ ].s,q.] by A1,Th166
.= [.p,q.] by A2,A4,Th167;
end;
suppose
A5: s < r;
hence [.p,r.[ \/ [.r,s.] \/ ].s,q.] = [.p,r.[ \/ {} \/ ].s,q.] by Th29
.= [.p,q.] by A2,A3,A5,Th175;
end;
end;
theorem
p s by TARSKI:def 1;
then r <= p & p < s or s < p & p <= t by A3,Th1,XXREAL_0:1;
then p in [.r,s.[ or p in ].s,t.] by Th2,Th3;
hence thesis by XBOOLE_0:def 3;
end;
assume p in [.r,s.[ \/ ].s,t.];
then p in [.r,s.[ or p in ].s,t.] by XBOOLE_0:def 3;
then
A4: r <= p & p < s or s < p & p <= t by Th2,Th3;
then
A5: r <= p by A1,XXREAL_0:2;
p <= t by A2,A4,XXREAL_0:2;
then
A6: p in [.r,t.] by A5,Th1;
not p in {s} by A4,TARSKI:def 1;
hence thesis by A6,XBOOLE_0:def 5;
end;
theorem
r <= s & s < t implies [.r,t.[ \ {s} = [.r,s.[ \/ ].s,t.[
proof
assume that
A1: r <= s and
A2: s < t;
let p;
thus p in [.r,t.[ \ {s} implies p in [.r,s.[ \/ ].s,t.[
proof
assume
A3: p in [.r,t.[ \ {s};
then not p in {s} by XBOOLE_0:def 5;
then p <> s by TARSKI:def 1;
then r <= p & p < s or s < p & p < t by A3,Th3,XXREAL_0:1;
then p in [.r,s.[ or p in ].s,t.[ by Th3,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume p in [.r,s.[ \/ ].s,t.[;
then p in [.r,s.[ or p in ].s,t.[ by XBOOLE_0:def 3;
then
A4: r <= p & p < s or s < p & p < t by Th3,Th4;
then
A5: r <= p by A1,XXREAL_0:2;
p < t by A2,A4,XXREAL_0:2;
then
A6: p in [.r,t.[ by A5,Th3;
not p in {s} by A4,TARSKI:def 1;
hence thesis by A6,XBOOLE_0:def 5;
end;
theorem
r < s & s <= t implies ].r,t.] \ {s} = ].r,s.[ \/ ].s,t.]
proof
assume that
A1: r < s and
A2: s <= t;
let p;
thus p in ].r,t.] \ {s} implies p in ].r,s.[ \/ ].s,t.]
proof
assume
A3: p in ].r,t.] \ {s};
then not p in {s} by XBOOLE_0:def 5;
then p <> s by TARSKI:def 1;
then r < p & p < s or s < p & p <= t by A3,Th2,XXREAL_0:1;
then p in ].r,s.[ or p in ].s,t.] by Th2,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume p in ].r,s.[ \/ ].s,t.];
then p in ].r,s.[ or p in ].s,t.] by XBOOLE_0:def 3;
then
A4: r < p & p < s or s < p & p <= t by Th2,Th4;
then
A5: r < p by A1,XXREAL_0:2;
p <= t by A2,A4,XXREAL_0:2;
then
A6: p in ].r,t.] by A5,Th2;
not p in {s} by A4,TARSKI:def 1;
hence thesis by A6,XBOOLE_0:def 5;
end;
theorem
r < s & s < t implies ].r,t.[ \ {s} = ].r,s.[ \/ ].s,t.[
proof
assume that
A1: r < s and
A2: s < t;
let p;
thus p in ].r,t.[ \ {s} implies p in ].r,s.[ \/ ].s,t.[
proof
assume
A3: p in ].r,t.[ \ {s};
then not p in {s} by XBOOLE_0:def 5;
then p <> s by TARSKI:def 1;
then r < p & p < s or s < p & p < t by A3,Th4,XXREAL_0:1;
then p in ].r,s.[ or p in ].s,t.[ by Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume p in ].r,s.[ \/ ].s,t.[;
then p in ].r,s.[ or p in ].s,t.[ by XBOOLE_0:def 3;
then
A4: r < p & p < s or s < p & p < t by Th4;
then
A5: r < p by A1,XXREAL_0:2;
p < t by A2,A4,XXREAL_0:2;
then
A6: p in ].r,t.[ by A5,Th4;
not p in {s} by A4,TARSKI:def 1;
hence thesis by A6,XBOOLE_0:def 5;
end;
theorem
not s in ].r,s .[ \/ ].s,t.[
proof
assume s in ].r,s .[ \/ ].s,t.[;
then s in ].r,s .[ or s in ].s,t.[ by XBOOLE_0:def 3;
hence contradiction by Th4;
end;
theorem
not s in [.r,s .[ \/ ].s,t.[
proof
assume s in [.r,s .[ \/ ].s,t.[;
then s in [.r,s .[ or s in ].s,t.[ by XBOOLE_0:def 3;
hence contradiction by Th3,Th4;
end;
theorem
not s in ].r,s .[ \/ ].s,t.]
proof
assume s in ].r,s .[ \/ ].s,t.];
then s in ].r,s .[ or s in ].s,t.] by XBOOLE_0:def 3;
hence contradiction by Th2,Th4;
end;
theorem
not s in [.r,s .[ \/ ].s,t.]
proof
assume s in [.r,s .[ \/ ].s,t.];
then s in [.r,s .[ or s in ].s,t.] by XBOOLE_0:def 3;
hence contradiction by Th2,Th3;
end;
begin :: -infty & + infty
theorem
[.-infty,+infty.] = ExtREAL
proof
let r;
thus r in [.-infty,+infty.] implies r in ExtREAL by XXREAL_0:def 1;
assume r in ExtREAL;
A1: -infty <= r by XXREAL_0:5;
r <= +infty by XXREAL_0:3;
hence thesis by A1,Th1;
end;
theorem :: MEASURE6:36
].p,-infty.[ = {}
proof
not ex x being object st x in ].p,-infty.[
proof
given x being object such that
A1: x in ].p,-infty.[;
reconsider s = x as ExtReal by A1;
s < -infty by A1,Th4;
hence contradiction by XXREAL_0:5;
end;
hence thesis;
end;
theorem :: MEASURE6:36
[.p,-infty.[ = {}
proof
not ex x being object st x in [.p,-infty.[
proof
given x being object such that
A1: x in [.p,-infty.[;
reconsider s = x as ExtReal by A1;
s < -infty by A1,Th3;
hence contradiction by XXREAL_0:5;
end;
hence thesis;
end;
theorem :: MEASURE6:36
].p,-infty.] = {}
proof
not ex x being object st x in ].p,-infty.]
proof
given x being object such that
A1: x in ].p,-infty.];
reconsider s = x as ExtReal by A1;
A2: p < s by A1,Th2;
s <= -infty by A1,Th2;
then p < -infty by A2,XXREAL_0:2;
hence contradiction by XXREAL_0:5;
end;
hence thesis;
end;
theorem :: MEASURE6:36
p <> -infty implies [.p,-infty.] = {}
proof
assume
A1: p <> -infty;
not ex x being object st x in [.p,-infty.]
proof
given x being object such that
A2: x in [.p,-infty.];
reconsider s = x as ExtReal by A2;
A3: p <= s by A2,Th1;
s <= -infty by A2,Th1;
hence contradiction by A1,A3,XXREAL_0:2,6;
end;
hence thesis;
end;
theorem :: MEASURE6:37
].+infty,p.[ = {}
proof
not ex x being object st x in ].+infty,p.[
proof
given x being object such that
A1: x in ].+infty,p.[;
reconsider s = x as ExtReal by A1;
+infty < s by A1,Th4;
hence contradiction by XXREAL_0:3;
end;
hence thesis;
end;
theorem :: MEASURE6:37
[.+infty,p.[ = {}
proof
not ex x being object st x in [.+infty,p.[
proof
given x being object such that
A1: x in [.+infty,p.[;
reconsider s = x as ExtReal by A1;
A2: +infty <= s by A1,Th3;
s < p by A1,Th3;
then p > +infty by A2,XXREAL_0:2;
hence contradiction by XXREAL_0:3;
end;
hence thesis;
end;
theorem :: MEASURE6:37
].+infty,p.] = {}
proof
not ex x being object st x in ].+infty,p.]
proof
given x being object such that
A1: x in ].+infty,p.];
reconsider s = x as ExtReal by A1;
+infty < s by A1,Th2;
hence contradiction by XXREAL_0:3;
end;
hence thesis;
end;
theorem :: MEASURE6:37
p <> +infty implies [.+infty,p.] = {}
proof
assume
A1: p <> +infty;
not ex x being object st x in [.+infty,p.]
proof
given x being object such that
A2: x in [.+infty,p.];
reconsider s = x as ExtReal by A2;
A3: +infty <= s by A2,Th1;
s <= p by A2,Th1;
hence contradiction by A1,A3,XXREAL_0:2,4;
end;
hence thesis;
end;
theorem
p > q implies p in ].q, +infty.]
by XXREAL_0:3,Th2;
theorem
q <= p implies p in [.q, +infty.]
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th1;
end;
theorem
p <= q implies p in [.-infty,q.]
proof
p >= -infty by XXREAL_0:5;
hence thesis by Th1;
end;
theorem
p < q implies p in [.-infty, q.[
by XXREAL_0:5,Th3;
begin :: Additional
theorem
p <= q implies [.p,q.] = [.p,q.] \/ [.q,p.]
proof
assume
A1: p <= q;
then
A2: [.q,p.] c= {p} by Th85;
p in [.p,q.] by A1,Th1;
then {p} c= [.p,q.] by ZFMISC_1:31;
hence thesis by A2,XBOOLE_1:1,12;
end;
theorem
r <= s & s <= t implies not r in ].s,t.[ \/ ].t,p.[
proof
assume that
A1: r <= s and
A2: s <= t;
assume r in ].s,t.[ \/ ].t,p.[;
then r in ].s,t.[ or r in ].t,p.[ by XBOOLE_0:def 3;
then s < r & r < t or t < r & r < p by Th4;
hence contradiction by A1,A2,XXREAL_0:2;
end;
:: from LIMFUNC1, 2008.06.12, A.T.
theorem Th224:
REAL = ].-infty,+infty.[
proof
let x be ExtReal;
thus x in REAL implies x in ].-infty,+infty.[
proof
assume
A1: x in REAL;
then
A2: -infty < x by XXREAL_0:12;
x < +infty by A1,XXREAL_0:9;
hence thesis by A2,Th4;
end;
assume
A3: x in ].-infty,+infty.[;
then
A4: -infty < x by Th4;
x < +infty by A3,Th4;
hence thesis by A4,XXREAL_0:14;
end;
theorem Th225:
].p,q.[ c= REAL
proof
let x be ExtReal;
assume
A1: x in ].p,q.[;
then
A2: p < x by Th4;
x < q by A1,Th4;
hence thesis by A2,XXREAL_0:48;
end;
theorem Th226:
p in REAL implies [.p,q.[ c= REAL
proof
assume
A1: p in REAL;
let x be ExtReal;
assume
A2: x in [.p,q.[;
then
A3: p <= x by Th3;
x < q by A2,Th3;
hence thesis by A1,A3,XXREAL_0:46;
end;
theorem Th227:
q in REAL implies ].p,q.] c= REAL
proof
assume
A1: q in REAL;
let x be ExtReal;
assume
A2: x in ].p,q.];
then
A3: p < x by Th2;
x <= q by A2,Th2;
hence thesis by A1,A3,XXREAL_0:47;
end;
theorem Th228:
p in REAL & q in REAL implies [.p,q.] c= REAL
proof
assume that
A1: p in REAL and
A2: q in REAL;
let x be ExtReal;
assume
A3: x in [.p,q.];
then
A4: p <= x by Th1;
x <= q by A3,Th1;
hence thesis by A1,A2,A4,XXREAL_0:45;
end;
registration
let p,q;
cluster ].p,q.[ -> real-membered;
coherence by Th225,MEMBERED:21;
end;
registration
let p be Real, q;
cluster [.p,q.[ -> real-membered;
coherence
proof
p in REAL by XREAL_0:def 1;
then [.p,q.[ c= REAL by Th226;
hence thesis;
end;
end;
registration
let q be Real, p;
cluster ].p,q.] -> real-membered;
coherence
proof
q in REAL by XREAL_0:def 1;
then ].p,q.] c= REAL by Th227;
hence thesis;
end;
end;
registration
let p,q be Real;
cluster [.p,q.] -> real-membered;
coherence
proof
A1: p in REAL by XREAL_0:def 1;
q in REAL by XREAL_0:def 1;
then [.p,q.] c= REAL by A1,Th228;
hence thesis;
end;
end;
:: from LIMFUNC1,2008.06.13, A.T.
theorem
].-infty,s.[ = {g : g