:: 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-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 <t by A1,A4,XXREAL_0:2;
t <= q by A2,A5,XXREAL_0:2;
hence thesis by A6,Th2;
end;
theorem Th40:
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,Th39;
hence thesis by A1;
end;
theorem Th41:
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 Th4;
A5: t < s by A3,Th4;
A6: p < t by A1,A4,XXREAL_0:2;
t < q by A2,A5,XXREAL_0:2;
hence thesis by A6,Th2;
end;
theorem Th42:
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 Th2;
A5: t <= s by A3,Th2;
A6: p < t by A1,A4,XXREAL_0:2;
t <= q by A2,A5,XXREAL_0:2;
hence thesis by A6,Th2;
end;
theorem Th43:
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,Th3;
end;
theorem Th44:
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,Th43;
hence thesis by A1;
end;
theorem Th45:
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 Th4;
A5: t < s by A3,Th4;
A6: p <= t by A1,A4,XXREAL_0:2;
t < q by A2,A5,XXREAL_0:2;
hence thesis by A6,Th3;
end;
theorem Th46:
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 Th4;
A5: t < s by A3,Th4;
A6: p < t by A1,A4,XXREAL_0:2;
t < q by A2,A5,XXREAL_0:2;
hence thesis by A6,Th4;
end;
theorem Th47:
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,Th4;
end;
theorem Th48:
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,Th4;
end;
theorem Th49:
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 Th2;
A5: t <= s by A3,Th2;
A6: p < t by A1,A4,XXREAL_0:2;
t < q by A2,A5,XXREAL_0:2;
hence thesis by A6,Th4;
end;
theorem Th50:
r <= s & [.r,s.] c= [.p,q.] implies p <= r & s <= q
proof
assume
A1: r <= s;
then
A2: r in [.r,s.] by Th1;
s in [.r,s.] by A1,Th1;
hence thesis by A2,Th1;
end;
theorem Th51:
r < s & ].r,s.[ c= [.p,q.] implies p <= r & s <= q
proof
assume that
A1: r < s and
A2: ].r,s.[ c= [.p,q.];
now
let t;
assume that
A3: r < t and
A4: t < s;
t in ].r,s.[ by A3,A4,Th4;
hence p <= t by A2,Th1;
end;
hence p <= r by A1,XREAL_1:228;
now
let t;
assume that
A5: r < t and
A6: t < s;
t in ].r,s.[ by A5,A6,Th4;
hence t <= q by A2,Th1;
end;
hence thesis by A1,XREAL_1:229;
end;
theorem Th52:
r < s & [.r,s.[ c= [.p,q.] implies p <= r & s <= q
proof
assume that
A1: r < s and
A2: [.r,s.[ c= [.p,q.];
].r,s.[ c= [.r,s.[ by Th22;
then ].r,s.[ c= [.p,q.] by A2;
hence thesis by A1,Th51;
end;
theorem Th53:
r < s & ].r,s.] c= [.p,q.] implies p <= r & s <= q
proof
assume that
A1: r < s and
A2: ].r,s.] c= [.p,q.];
].r,s.[ c= ].r,s.] by Th21;
then ].r,s.[ c= [.p,q.] by A2;
hence thesis by A1,Th51;
end;
theorem Th54:
r <= s & [.r,s.] c= [.p,q.[ implies p <= r & s < q
proof
assume that
A1: r <= s and
A2: [.r,s.] c= [.p,q.[;
[.p,q.[ c= [.p,q.] by Th24;
then [.r,s.] c= [.p,q.] by A2;
hence p <= r by A1,Th50;
s in [.r,s.] by A1,Th1;
hence thesis by A2,Th3;
end;
theorem Th55:
r < s & [.r,s.[ c= [.p,q.[ implies p <= r & s <= q
proof
assume that
A1: r < s and
A2: [.r,s.[ c= [.p,q.[;
].r,s.[ c= [.r,s.[ by Th22;
then
A3: ].r,s.[ c= [.p,q.[ by A2;
[.p,q.[ c= [.p,q.] by Th24;
then ].r,s.[ c= [.p,q.] by A3;
hence thesis by A1,Th51;
end;
theorem Th56:
r < s & ].r,s.[ c= [.p,q.[ implies p <= r & s <= q
proof
assume that
A1: r < s and
A2: ].r,s.[ c= [.p,q.[;
[.p,q.[ c= [.p,q.] by Th24;
then ].r,s.[ c= [.p,q.] by A2;
hence thesis by A1,Th51;
end;
theorem Th57:
r < s & ].r,s.] c= [.p,q.[ implies p <= r & s < q
proof
assume that
A1: r < s and
A2: ].r,s.] c= [.p,q.[;
[.p,q.[ c= [.p,q.] by Th24;
then ].r,s.] c= [.p,q.] by A2;
hence p <= r by A1,Th53;
s in ].r,s.] by A1,Th2;
hence thesis by A2,Th3;
end;
theorem Th58:
r <= s & [.r,s.] c= ].p,q.] implies p < r & s <= q
proof
assume that
A1: r <= s and
A2: [.r,s.] c= ].p,q.];
].p,q.] c= [.p,q.] by Th23;
then
A3: [.r,s.] c= [.p,q.] by A2;
r in [.r,s.] by A1,Th1;
hence p < r by A2,Th2;
thus thesis by A1,A3,Th50;
end;
theorem Th59:
r < s & ].r,s.[ c= ].p,q.] implies p <= r & s <= q
proof
assume that
A1: r < s and
A2: ].r,s.[ c= ].p,q.];
].p,q.] c= [.p,q.] by Th23;
then ].r,s.[ c= [.p,q.] by A2;
hence thesis by A1,Th51;
end;
theorem Th60:
r < s & [.r,s.[ c= ].p,q.] implies p < r & s <= q
proof
assume that
A1: r < s and
A2: [.r,s.[ c= ].p,q.];
].p,q.] c= [.p,q.] by Th23;
then
A3: [.r,s.[ c= [.p,q.] by A2;
r in [.r,s.[ by A1,Th3;
hence p < r by A2,Th2;
thus thesis by A1,A3,Th52;
end;
theorem Th61:
r < s & ].r,s.] c= ].p,q.] implies p <= r & s <= q
proof
assume that
A1: r < s and
A2: ].r,s.] c= ].p,q.];
].r,s.[ c= ].r,s.] by Th21;
then
A3: ].r,s.[ c= ].p,q.] by A2;
].p,q.] c= [.p,q.] by Th23;
then ].r,s.[ c= [.p,q.] by A3;
hence thesis by A1,Th51;
end;
theorem Th62:
r <= s & [.r,s.] c= ].p,q.[ implies p < r & s < q
proof
assume that
A1: r <= s and
A2: [.r,s.] c= ].p,q.[;
r in [.r,s.] by A1,Th1;
hence p < r by A2,Th4;
s in [.r,s.] by A1,Th1;
hence thesis by A2,Th4;
end;
theorem Th63:
r < s & ].r,s.[ c= ].p,q.[ implies p <= r & s <= q
proof
assume that
A1: r < s and
A2: ].r,s.[ c= ].p,q.[;
].p,q.[ c= [.p,q.] by Th25;
then ].r,s.[ c= [.p,q.] by A2;
hence thesis by A1,Th51;
end;
theorem Th64:
r < s & [.r,s.[ c= ].p,q.[ implies p < r & s <= q
proof
assume that
A1: r < s and
A2: [.r,s.[ c= ].p,q.[;
].p,q.[ c= [.p,q.] by Th25;
then
A3: [.r,s.[ c= [.p,q.] by A2;
r in [.r,s.[ by A1,Th3;
hence p < r by A2,Th4;
thus thesis by A1,A3,Th52;
end;
theorem Th65:
r < s & ].r,s.] c= ].p,q.[ implies p <= r & s < q
proof
assume that
A1: r < s and
A2: ].r,s.] c= ].p,q.[;
].p,q.[ c= [.p,q.] by Th25;
then ].r,s.] c= [.p,q.] by A2;
hence p <= r by A1,Th53;
s in ].r,s.] by A1,Th2;
hence thesis by A2,Th4;
end;
theorem :: INTEGRA1:6 ??
p <= q & [.p,q.] = [.r,s.] implies p = r & q = s
proof
assume that
A1: p <= q and
A2: [.p,q.] = [.r,s.];
A3: r <= p by A1,A2,Th50;
A4: q <= s by A1,A2,Th50;
r <= q by A1,A3,XXREAL_0:2;
then
A5: r <= s by A4,XXREAL_0:2;
then
A6: p <= r by A2,Th50;
s <= q by A2,A5,Th50;
hence thesis by A3,A4,A6,XXREAL_0:1;
end;
theorem
p < q & ].p,q.[ = ].r,s.[ implies p = r & q = s
proof
assume that
A1: p < q and
A2: ].p,q.[ = ].r,s.[;
A3: r <= p by A1,A2,Th63;
A4: q <= s by A1,A2,Th63;
r < q by A1,A3,XXREAL_0:2;
then
A5: r < s by A4,XXREAL_0:2;
then
A6: p <= r by A2,Th63;
s <= q by A2,A5,Th63;
hence thesis by A3,A4,A6,XXREAL_0:1;
end;
theorem
p < q & ].p,q.] = ].r,s.] implies p = r & q = s
proof
assume that
A1: p < q and
A2: ].p,q.] = ].r,s.];
A3: r <= p by A1,A2,Th61;
A4: q <= s by A1,A2,Th61;
r < q by A1,A3,XXREAL_0:2;
then
A5: r < s by A4,XXREAL_0:2;
then
A6: p <= r by A2,Th61;
s <= q by A2,A5,Th61;
hence thesis by A3,A4,A6,XXREAL_0:1;
end;
theorem
p < q & [.p,q.[ = [.r,s.[ implies p = r & q = s
proof
assume that
A1: p < q and
A2: [.p,q.[ = [.r,s.[;
A3: r <= p by A1,A2,Th55;
A4: q <= s by A1,A2,Th55;
r < q by A1,A3,XXREAL_0:2;
then
A5: r < s by A4,XXREAL_0:2;
then
A6: p <= r by A2,Th55;
s <= q by A2,A5,Th55;
hence thesis by A3,A4,A6,XXREAL_0:1;
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 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<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,Th171
.= ].p,q.[ by A2,A4,Th173;
end;
suppose
A5: s <= r;
hence ].p,r.] \/ ].r,s.[ \/ [.s,q.[ = ].p,r.] \/ {} \/ [.s,q.[ by Th28
.= ].p,q.[ by A2,A3,A5,Th178;
end;
end;
theorem
p <= r & r <= s & s <= q implies [.p,r.] \/ ].r,s.[ \/ [.s,q.] = [.p,q.]
proof
assume that
A1: p <= r and
A2: r <= s and
A3: s <= q;
A4: p <= s by A1,A2,XXREAL_0:2;
A5: r <= q by A2,A3,XXREAL_0:2;
per cases;
suppose r < s;
hence [.p,r.] \/ ].r,s.[ \/ [.s,q.] = [.p,s.[ \/ [.s,q.] by A1,Th169
.= [.p,q.] by A3,A4,Th166;
end;
suppose
A6: s <= r;
hence [.p,r.] \/ ].r,s.[ \/ [.s,q.] = [.p,r.] \/ {} \/ [.s,q.] by Th28
.= [.p,q.] by A4,A5,A6,Th174;
end;
end;
theorem Th182:
r <= s implies [.r,t.] \ [.r,s.] = ].s,t.]
proof
assume that
A1: r <= s;
let p;
thus p in [.r,t.] \ [.r,s.] implies p in ].s,t.]
proof
assume
A2: p in [.r,t.] \ [.r,s.];
then
A3: not p in [.r,s.] by XBOOLE_0:def 5;
A4: p <= t by A2,Th1;
p < r or s < p by A3,Th1;
hence thesis by A2,A4,Th1,Th2;
end;
assume
A5: p in ].s,t.];
then
A6: s < p by Th2;
then
A7: r <= p by A1,XXREAL_0:2;
p <= t by A5,Th2;
then
A8: p in [.r,t.] by A7,Th1;
not p in [.r,s.] by A6,Th1;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th183:
r <= s implies [.r,t.[ \ [.r,s.] = ].s,t.[
proof
assume that
A1: r <= s;
let p;
thus p in [.r,t.[ \ [.r,s.] implies p in ].s,t.[
proof
assume
A2: p in [.r,t.[ \ [.r,s.];
then
A3: not p in [.r,s.] by XBOOLE_0:def 5;
A4: p < t by A2,Th3;
p < r or s < p by A3,Th1;
hence thesis by A2,A4,Th3,Th4;
end;
assume
A5: p in ].s,t.[;
then
A6: s < p by Th4;
then
A7: r <= p by A1,XXREAL_0:2;
p < t by A5,Th4;
then
A8: p in [.r,t.[ by A7,Th3;
not p in [.r,s.] by A6,Th1;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th184:
r < s implies [.r,t.] \ [.r,s.[ = [.s,t.]
proof
assume that
A1: r < s;
let p;
thus p in [.r,t.] \ [.r,s.[ implies p in [.s,t.]
proof
assume
A2: p in [.r,t.] \ [.r,s.[;
then
A3: not p in [.r,s.[ by XBOOLE_0:def 5;
A4: p <= t by A2,Th1;
p < r or s <= p by A3,Th3;
hence thesis by A2,A4,Th1;
end;
assume
A5: p in [.s,t.];
then
A6: s <= p by Th1;
then
A7: r <= p by A1,XXREAL_0:2;
p <= t by A5,Th1;
then
A8: p in [.r,t.] by A7,Th1;
not p in [.r,s.[ by A6,Th3;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th185:
r < s implies [.r,t.[ \ [.r,s.[ = [.s,t.[
proof
assume that
A1: r < s;
let p;
thus p in [.r,t.[ \ [.r,s.[ implies p in [.s,t.[
proof
assume
A2: p in [.r,t.[ \ [.r,s.[;
then
A3: not p in [.r,s.[ by XBOOLE_0:def 5;
A4: p < t by A2,Th3;
p < r or s <= p by A3,Th3;
hence thesis by A2,A4,Th3;
end;
assume
A5: p in [.s,t.[;
then
A6: s <= p by Th3;
then
A7: r <= p by A1,XXREAL_0:2;
p < t by A5,Th3;
then
A8: p in [.r,t.[ by A7,Th3;
not p in [.r,s.[ by A6,Th3;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th186:
r <= s implies [.r,t.] \ [.r,s.] = ].s,t.]
proof
assume that
A1: r <= s;
let p;
thus p in [.r,t.] \ [.r,s.] implies p in ].s,t.]
proof
assume
A2: p in [.r,t.] \ [.r,s.];
then
A3: not p in [.r,s.] by XBOOLE_0:def 5;
A4: p <= t by A2,Th1;
p < r or s < p by A3,Th1;
hence thesis by A2,A4,Th1,Th2;
end;
assume
A5: p in ].s,t.];
then
A6: s < p by Th2;
then
A7: r <= p by A1,XXREAL_0:2;
p <= t by A5,Th2;
then
A8: p in [.r,t.] by A7,Th1;
not p in [.r,s.] by A6,Th1;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th187:
r < s implies ].r,t.[ \ ].r,s.] = ].s,t.[
proof
assume that
A1: r < s;
let p;
thus p in ].r,t.[ \ ].r,s.] implies p in ].s,t.[
proof
assume
A2: p in ].r,t.[ \ ].r,s.];
then
A3: not p in ].r,s.] by XBOOLE_0:def 5;
A4: p < t by A2,Th4;
p <= r or s < p by A3,Th2;
hence thesis by A2,A4,Th4;
end;
assume
A5: p in ].s,t.[;
then
A6: s < p by Th4;
then
A7: r < p by A1,XXREAL_0:2;
p < t by A5,Th4;
then
A8: p in ].r,t.[ by A7,Th4;
not p in ].r,s.] by A6,Th2;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th188:
r < s implies ].r,t.] \ ].r,s.[ = [.s,t.]
proof
assume that
A1: r < s;
let p;
thus p in ].r,t.] \ ].r,s.[ implies p in [.s,t.]
proof
assume
A2: p in ].r,t.] \ ].r,s.[;
then
A3: not p in ].r,s.[ by XBOOLE_0:def 5;
A4: p <= t by A2,Th2;
p <= r or s <= p by A3,Th4;
hence thesis by A2,A4,Th1,Th2;
end;
assume
A5: p in [.s,t.];
then
A6: s <= p by Th1;
then
A7: r < p by A1,XXREAL_0:2;
p <= t by A5,Th1;
then
A8: p in ].r,t.] by A7,Th2;
not p in ].r,s.[ by A6,Th4;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th189:
r < s implies ].r,t.[ \ ].r,s.[ = [.s,t.[
proof
assume that
A1: r < s;
let p;
thus p in ].r,t.[ \ ].r,s.[ implies p in [.s,t.[
proof
assume
A2: p in ].r,t.[ \ ].r,s.[;
then
A3: not p in ].r,s.[ by XBOOLE_0:def 5;
A4: p < t by A2,Th4;
p <= r or s <= p by A3,Th4;
hence thesis by A2,A4,Th3,Th4;
end;
assume
A5: p in [.s,t.[;
then
A6: s <= p by Th3;
then
A7: r < p by A1,XXREAL_0:2;
p < t by A5,Th3;
then
A8: p in ].r,t.[ by A7,Th4;
not p in ].r,s.[ by A6,Th4;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th190:
s <= t implies [.r,t.] \ [.s,t.] = [.r,s.[
proof
assume that
A1: s <= t;
let p;
thus p in [.r,t.] \ [.s,t.] implies p in [.r,s.[
proof
assume
A2: p in [.r,t.] \ [.s,t.];
then
A3: not p in [.s,t.] by XBOOLE_0:def 5;
A4: r <= p by A2,Th1;
p < s or t < p by A3,Th1;
hence thesis by A2,A4,Th1,Th3;
end;
assume
A5: p in [.r,s.[;
then
A6: p < s by Th3;
A7: r <= p by A5,Th3;
p <= t by A1,A6,XXREAL_0:2;
then
A8: p in [.r,t.] by A7,Th1;
not p in [.s,t.] by A6,Th1;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th191:
s <= t implies ].r,t.] \ [.s,t.] = ].r,s.[
proof
assume that
A1: s <= t;
let p;
thus p in ].r,t.] \ [.s,t.] implies p in ].r,s.[
proof
assume
A2: p in ].r,t.] \ [.s,t.];
then
A3: not p in [.s,t.] by XBOOLE_0:def 5;
A4: r < p by A2,Th2;
p < s or t < p by A3,Th1;
hence thesis by A2,A4,Th2,Th4;
end;
assume
A5: p in ].r,s.[;
then
A6: p < s by Th4;
A7: r < p by A5,Th4;
p <= t by A1,A6,XXREAL_0:2;
then
A8: p in ].r,t.] by A7,Th2;
not p in [.s,t.] by A6,Th1;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th192:
s < t implies [.r,t.] \ ].s,t.] = [.r,s.]
proof
assume that
A1: s < t;
let p;
thus p in [.r,t.] \ ].s,t.] implies p in [.r,s.]
proof
assume
A2: p in [.r,t.] \ ].s,t.];
then
A3: not p in ].s,t.] by XBOOLE_0:def 5;
A4: r <= p by A2,Th1;
p <= s or t < p by A3,Th2;
hence thesis by A2,A4,Th1;
end;
assume
A5: p in [.r,s.];
then
A6: p <= s by Th1;
A7: r <= p by A5,Th1;
p <= t by A1,A6,XXREAL_0:2;
then
A8: p in [.r,t.] by A7,Th1;
not p in ].s,t.] by A6,Th2;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th193:
s < t implies ].r,t.] \ ].s,t.] = ].r,s.]
proof
assume that
A1: s < t;
let p;
thus p in ].r,t.] \ ].s,t.] implies p in ].r,s.]
proof
assume
A2: p in ].r,t.] \ ].s,t.];
then
A3: not p in ].s,t.] by XBOOLE_0:def 5;
A4: r < p by A2,Th2;
p <= s or t < p by A3,Th2;
hence thesis by A2,A4,Th2;
end;
assume
A5: p in ].r,s.];
then
A6: p <= s by Th2;
A7: r < p by A5,Th2;
p <= t by A1,A6,XXREAL_0:2;
then
A8: p in ].r,t.] by A7,Th2;
not p in ].s,t.] by A6,Th2;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th194:
s < t implies [.r,t.[ \ [.s,t.[ = [.r,s.[
proof
assume that
A1: s < t;
let p;
thus p in [.r,t.[ \ [.s,t.[ implies p in [.r,s.[
proof
assume
A2: p in [.r,t.[ \ [.s,t.[;
then
A3: not p in [.s,t.[ by XBOOLE_0:def 5;
A4: r <= p by A2,Th3;
p < s or t <= p by A3,Th3;
hence thesis by A2,A4,Th3;
end;
assume
A5: p in [.r,s.[;
then
A6: p < s by Th3;
A7: r <= p by A5,Th3;
p < t by A1,A6,XXREAL_0:2;
then
A8: p in [.r,t.[ by A7,Th3;
not p in [.s,t.[ by A6,Th3;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th195:
s < t implies ].r,t.[ \ [.s,t.[ = ].r,s.[
proof
assume that
A1: s < t;
let p;
thus p in ].r,t.[ \ [.s,t.[ implies p in ].r,s.[
proof
assume
A2: p in ].r,t.[ \ [.s,t.[;
then
A3: not p in [.s,t.[ by XBOOLE_0:def 5;
A4: r < p by A2,Th4;
p < s or t <= p by A3,Th3;
hence thesis by A2,A4,Th4;
end;
assume
A5: p in ].r,s.[;
then
A6: p < s by Th4;
A7: r < p by A5,Th4;
p < t by A1,A6,XXREAL_0:2;
then
A8: p in ].r,t.[ by A7,Th4;
not p in [.s,t.[ by A6,Th3;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th196:
s < t implies [.r,t.[ \ ].s,t.[ = [.r,s.]
proof
assume that
A1: s < t;
let p;
thus p in [.r,t.[ \ ].s,t.[ implies p in [.r,s.]
proof
assume
A2: p in [.r,t.[ \ ].s,t.[;
then
A3: not p in ].s,t.[ by XBOOLE_0:def 5;
A4: r <= p by A2,Th3;
p <= s or t <= p by A3,Th4;
hence thesis by A2,A4,Th1,Th3;
end;
assume
A5: p in [.r,s.];
then
A6: p <= s by Th1;
A7: r <= p by A5,Th1;
p < t by A1,A6,XXREAL_0:2;
then
A8: p in [.r,t.[ by A7,Th3;
not p in ].s,t.[ by A6,Th4;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem Th197:
s < t implies ].r,t.[ \ ].s,t.[ = ].r,s.]
proof
assume that
A1: s < t;
let p;
thus p in ].r,t.[ \ ].s,t.[ implies p in ].r,s.]
proof
assume
A2: p in ].r,t.[ \ ].s,t.[;
then
A3: not p in ].s,t.[ by XBOOLE_0:def 5;
A4: r < p by A2,Th4;
p <= s or t <= p by A3,Th4;
hence thesis by A2,A4,Th2,Th4;
end;
assume
A5: p in ].r,s.];
then
A6: p <= s by Th2;
A7: r < p by A5,Th2;
p < t by A1,A6,XXREAL_0:2;
then
A8: p in ].r,t.[ by A7,Th4;
not p in ].s,t.[ by A6,Th4;
hence thesis by A8,XBOOLE_0:def 5;
end;
theorem
[.p,q.[ meets [.r,s.[ implies [.p,q.[ \ [.r,s.[ = [.p,r.[ \/ [.s,q.[
proof
assume [.p,q.[ meets [.r,s.[;
then consider u such that
A1: u in [.r,s.[ and
A2: u in [.p,q.[;
A3: r <= u by A1,Th3;
A4: u <= s by A1,Th3;
A5: p <= u by A2,Th3;
u <= q by A2,Th3;
then
A6: r <= q by A3,XXREAL_0:2;
A7: p <= s by A4,A5,XXREAL_0:2;
let t;
thus t in [.p,q.[ \ [.r,s.[ implies t in [.p,r.[ \/ [.s,q.[
proof
assume
A8: t in [.p,q.[ \ [.r,s.[;
then
A9: not t in [.r,s.[ by XBOOLE_0:def 5;
A10: p <= t by A8,Th3;
A11: t < q by A8,Th3;
t < r or s <= t by A9,Th3;
then t in [.p,r.[ or t in [.s,q.[ by A10,A11,Th3;
hence thesis by XBOOLE_0:def 3;
end;
assume t in [.p,r.[ \/ [.s,q.[;
then t in [.p,r.[ or t in [.s,q.[ by XBOOLE_0:def 3;
then
A12: p <= t & t < r or s <= t & t < q by Th3;
then
A13: p <= t by A7,XXREAL_0:2;
t < q by A6,A12,XXREAL_0:2;
then
A14: t in [.p,q.[ by A13,Th3;
not t in [.r,s.[ by A12,Th3;
hence thesis by A14,XBOOLE_0:def 5;
end;
theorem
].p,q.] meets ].r,s.] implies ].p,q.] \ ].r,s.] = ].p,r.] \/ ].s,q.]
proof
assume ].p,q.] meets ].r,s.];
then consider u such that
A1: u in ].r,s.] and
A2: u in ].p,q.];
A3: r < u by A1,Th2;
A4: u <= s by A1,Th2;
A5: p < u by A2,Th2;
u <= q by A2,Th2;
then
A6: r <= q by A3,XXREAL_0:2;
A7: p <= s by A4,A5,XXREAL_0:2;
let t;
thus t in ].p,q.] \ ].r,s.] implies t in ].p,r.] \/ ].s,q.]
proof
assume
A8: t in ].p,q.] \ ].r,s.];
then
A9: not t in ].r,s.] by XBOOLE_0:def 5;
A10: p < t by A8,Th2;
A11: t <= q by A8,Th2;
t <= r or s < t by A9,Th2;
then t in ].p,r.] or t in ].s,q.] by A10,A11,Th2;
hence thesis by XBOOLE_0:def 3;
end;
assume t in ].p,r.] \/ ].s,q.];
then t in ].p,r.] or t in ].s,q.] by XBOOLE_0:def 3;
then
A12: p < t & t <= r or s < t & t <= q by Th2;
then
A13: p < t by A7,XXREAL_0:2;
t <= q by A6,A12,XXREAL_0:2;
then
A14: t in ].p,q.] by A13,Th2;
not t in ].r,s.] by A12,Th2;
hence thesis by A14,XBOOLE_0:def 5;
end;
theorem
p <= r & s <= q implies [.p,q.] \ ([.p,r.] \/ [.s,q.]) = ].r,s.[
proof
assume that
A1: p <= r and
A2: s <= q;
thus [.p,q.] \ ([.p,r.] \/ [.s,q.])
= [.p,q.] \ [.p,r.] \ [.s,q.] by XBOOLE_1:41
.= ].r,q.] \ [.s,q.] by A1,Th182
.= ].r,s.[ by A2,Th191;
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,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<s}
proof
thus ].-infty,s.[ c= {g : g<s}
proof
let x be Real;
assume
A1: x in ].-infty,s.[;
A2: x < s by A1,Th4;
thus thesis by A2;
end;
let x be object;
assume x in {g : g<s};
then consider g such that
A3: x = g and
A4: g < s;
g in REAL by XREAL_0:def 1;
then -infty < g by XXREAL_0:12;
hence thesis by A3,A4,Th4;
end;
theorem
].s,+infty.[ = {g : s<g}
proof
thus ].s,+infty.[ c= {g : s<g}
proof
let x be Real;
assume
x in ].s,+infty.[;
then
A1: s < x by Th4;
thus thesis by A1;
end;
let x be object;
assume x in {g : s<g};
then consider g such that
A2: x = g and
A3: s < g;
g in REAL by XREAL_0:def 1;
then g < +infty by XXREAL_0:9;
hence thesis by A2,A3,Th4;
end;
theorem
for s being Real holds ].-infty,s.] = {g : g<=s}
proof
let s be Real;
thus ].-infty,s.] c= {g : g<=s}
proof
let x be Real;
assume x in ].-infty,s.];
then
A1: x <= s by Th2;
thus thesis by A1;
end;
let x be object;
assume x in {g : g<=s};
then consider g such that
A2: x = g and
A3: g <= s;
g in REAL by XREAL_0:def 1;
then -infty < g by XXREAL_0:12;
hence thesis by A2,A3,Th2;
end;
theorem
for s being Real holds [.s,+infty.[ = {g : s<=g}
proof
let s be Real;
thus [.s,+infty.[ c= {g : s<=g}
proof
let x be Real;
assume x in [.s,+infty.[;
then
A1: s <= x by Th3;
thus thesis by A1;
end;
let x be object;
assume x in {g : s<=g};
then consider g such that
A2: x = g and
A3: s <= g;
g in REAL by XREAL_0:def 1;
then g < +infty by XXREAL_0:9;
hence thesis by A2,A3,Th3;
end;
theorem
for x being Real holds x in ].-infty,u.[ iff x < u
proof
let x be Real;
x in REAL by XREAL_0:def 1;
then -infty < x by XXREAL_0:12;
hence thesis by Th4;
end;
theorem
for x being Real holds x in ].-infty,u.] iff x <= u
proof
let x be Real;
x in REAL by XREAL_0:def 1;
then -infty < x by XXREAL_0:12;
hence thesis by Th2;
end;
theorem
for x being Real holds x in ].u,+infty.[ iff u < x
proof
let x be Real;
x in REAL by XREAL_0:def 1;
then x < +infty by XXREAL_0:9;
hence thesis by Th4;
end;
theorem
for x being Real holds x in [.u,+infty.[ iff u <= x
proof
let x be Real;
x in REAL by XREAL_0:def 1;
then x < +infty by XXREAL_0:9;
hence thesis by Th3;
end;
theorem
p <= r implies [.r,s.] c= [.p,+infty.]
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th34;
end;
theorem
p <= r implies [.r,s.[ c= [.p,+infty.]
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th35;
end;
theorem
p <= r implies ].r,s.] c= [.p,+infty.]
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th36;
end;
theorem
p <= r implies ].r,s.[ c= [.p,+infty.]
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th37;
end;
theorem
p <= r implies [.r,s.[ c= [.p,+infty.[
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th38;
end;
theorem
p < r implies [.r,s.] c= ].p,+infty.] by Th39,XXREAL_0:3;
theorem
p < r implies [.r,s.[ c= ].p,+infty.] by Th40,XXREAL_0:3;
theorem
p <= r implies ].r,s.[ c= ].p,+infty.]
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th41;
end;
theorem
p <= r implies ].r,s.] c= ].p,+infty.]
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th42;
end;
theorem
p <= r implies ].r,s.[ c= [.p,+infty.[
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th45;
end;
theorem
p <= r implies ].r,s.[ c= ].p,+infty.[
proof
s <= +infty by XXREAL_0:3;
hence thesis by Th46;
end;
theorem
p < r implies [.r,s.[ c= ].p,+infty.[ by Th48,XXREAL_0:3;
theorem
for s being Real st p < r holds [.r,s.] c= ].p,+infty.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
then s < +infty by XXREAL_0:9;
hence thesis by Th47;
end;
theorem
for s being Real st p <= r holds ].r,s.] c= ].p,+infty.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th49,XXREAL_0:9;
end;
theorem
for s being Real st p <= r holds [.r,s.] c= [.p,+infty.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th43,XXREAL_0:9;
end;
theorem
for s being Real st p <= r holds ].r,s.] c= [.p,+infty.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th44,XXREAL_0:9;
end;
theorem
s <= q implies [.r,s.] c= [.-infty,q.]
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th34;
end;
theorem
s <= q implies [.r,s.[ c= [.-infty,q.]
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th35;
end;
theorem
s <= q implies ].r,s.] c= [.-infty,q.]
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th36;
end;
theorem
s <= q implies ].r,s.[ c= [.-infty,q.]
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th37;
end;
theorem
s <= q implies [.r,s.[ c= [.-infty,q.[
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th38;
end;
theorem
s <= q implies ].r,s.[ c= ].-infty,q.]
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th41;
end;
theorem
s <= q implies ].r,s.] c= ].-infty,q.]
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th42;
end;
theorem
s < q implies [.r,s.] c= [.-infty,q.[ by Th43,XXREAL_0:5;
theorem
s < q implies ].r,s.] c= [.-infty,q.[ by Th44,XXREAL_0:5;
theorem
s <= q implies ].r,s.[ c= [.-infty,q.[
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th45;
end;
theorem
s <= q implies ].r,s.[ c= ].-infty,q.[
proof
-infty <= r by XXREAL_0:5;
hence thesis by Th46;
end;
theorem
s < q implies ].r,s.] c= ].-infty,q.[ by Th49,XXREAL_0:5;
theorem
for r being Real st s <= q holds [.r,s.] c= ].-infty,q.]
proof
let r be Real;
r in REAL by XREAL_0:def 1;
hence thesis by Th39,XXREAL_0:12;
end;
theorem
for r being Real st s <= q holds [.r,s.[ c= ].-infty,q.]
proof
let r be Real;
r in REAL by XREAL_0:def 1;
hence thesis by Th40,XXREAL_0:12;
end;
theorem
for r being Real st s < q holds [.r,s.] c= ].-infty,q.[
proof
let r be Real;
r in REAL by XREAL_0:def 1;
then -infty < r by XXREAL_0:12;
hence thesis by Th47;
end;
theorem
for r being Real st s <= q holds [.r,s.[ c= ].-infty,q.[
proof
let r be Real;
r in REAL by XREAL_0:def 1;
hence thesis by Th48,XXREAL_0:12;
end;
theorem :: LIMFUNC1:18
for a,b being ExtReal holds ].-infty,b.[ /\ ].a,+infty.[ = ].a,b.[
proof
let a,b be ExtReal;
A1: -infty <= a by XXREAL_0:5;
b <= +infty by XXREAL_0:3;
hence thesis by A1,Th160;
end;
theorem :: BORSUK_5:91
for b being Real holds ].-infty,b.] /\ ].p,+infty.[ = ].p,b.]
proof
let b be Real;
A1: b in REAL by XREAL_0:def 1;
-infty <= p by XXREAL_0:5;
hence thesis by A1,Th159,XXREAL_0:9;
end;
theorem
for a being Real holds ].-infty,p.[ /\ [.a,+infty.[ = [.a,p.[
proof
let a be Real;
a in REAL by XREAL_0:def 1;
then -infty < a by XXREAL_0:12;
hence thesis by Th154,XXREAL_0:3;
end;
theorem :: LIMFUNC1:19
for a,b being Real holds ].-infty,a.] /\ [.b,+infty.[ = [.b,a.]
proof
let a,b be Real;
A1: a in REAL by XREAL_0:def 1;
b in REAL by XREAL_0:def 1;
then
A2: -infty < b by XXREAL_0:12;
a < +infty by A1,XXREAL_0:9;
hence thesis by A2,Th152;
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 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 Th3;
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 be Real;
assume t in ].r,s.[;
then t <= s by Th4;
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 Th4;
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 Th1;
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 Th1;
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 Th2;
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 Th2;
then t < p by A1,XXREAL_0:2;
hence thesis by Th1;
end;
theorem
[.-infty,t.] \ [.-infty,s.] = ].s,t.] by Th182,XXREAL_0:5;
theorem
[.-infty,t.[ \ [.-infty,s.] = ].s,t.[ by Th183,XXREAL_0:5;
theorem
[.-infty,t.] \ [.-infty,s.] = ].s,t.] by Th186,XXREAL_0:5;
theorem
[.r,+infty.] \ [.s,+infty.] = [.r,s.[ by Th190,XXREAL_0:3;
theorem
].r,+infty.] \ [.s,+infty.] = ].r,s.[ by Th191,XXREAL_0:3;
theorem
for s being Real holds [.-infty,t.] \ [.-infty,s.[ = [.s,t.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th184,XXREAL_0:12;
end;
theorem
for s being Real holds [.-infty,t.[ \ [.-infty,s.[ = [.s,t.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th185,XXREAL_0:12;
end;
theorem
for s being Real holds ].-infty,t.[ \ ].-infty,s.] = ].s,t.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th187,XXREAL_0:12;
end;
theorem
for s being Real holds ].-infty,t.] \ ].-infty,s.[ = [.s,t.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th188,XXREAL_0:12;
end;
theorem
for s being Real holds ].-infty,t.[ \ ].-infty,s.[ = [.s,t.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th189,XXREAL_0:12;
end;
theorem
for s being Real holds [.r,+infty.] \ ].s,+infty.] = [.r,s.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th192,XXREAL_0:9;
end;
theorem
for s being Real holds ].r,+infty.] \ ].s,+infty.] = ].r,s.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th193,XXREAL_0:9;
end;
theorem
for s being Real holds [.r,+infty.[ \ [.s,+infty.[ = [.r,s.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th194,XXREAL_0:9;
end;
theorem
for s being Real holds ].r,+infty.[ \ [.s,+infty.[ = ].r,s.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th195,XXREAL_0:9;
end;
theorem
for s being Real holds [.r,+infty.[ \ ].s,+infty.[ = [.r,s.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th196,XXREAL_0:9;
end;
theorem
for s being Real holds ].r,+infty.[ \ ].s,+infty.[ = ].r,s.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th197,XXREAL_0:9;
end;
theorem Th297:
r < s & p < q implies ].r,q.[ \ ].p,s.[ = ].r,p.] \/ [.s,q.[
proof
assume that
A1: r < s and
A2: p < q;
let x be ExtReal;
thus x in ].r,q.[ \ ].p,s.[ implies x in ].r,p.] \/ [.s,q.[
proof
assume
A3: x in ].r,q.[ \ ].p,s.[;
then
A4: not x in ].p,s.[ by XBOOLE_0:def 5;
A5: r < x by A3,Th4;
A6: x < q by A3,Th4;
not(p < x & x < s) by A4,Th4;
then x in ].r,p.] or x in [.s,q.[ by A5,A6,Th2,Th3;
hence thesis by XBOOLE_0:def 3;
end;
assume x in ].r,p.] \/ [.s,q.[;
then x in ].r,p.] or x in [.s,q.[ by XBOOLE_0:def 3;
then
A7: r < x & x <= p or s <= x & x < q by Th2,Th3;
then
A8: r < x by A1,XXREAL_0:2;
x < q by A2,A7,XXREAL_0:2;
then
A9: x in ].r,q.[ by A8,Th4;
not x in ].p,s.[ by A7,Th4;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th298:
r <= s & p < q implies [.r,q.[ \ ].p,s.[ = [.r,p.] \/ [.s,q.[
proof
assume that
A1: r <= s and
A2: p < q;
let x be ExtReal;
thus x in [.r,q.[ \ ].p,s.[ implies x in [.r,p.] \/ [.s,q.[
proof
assume
A3: x in [.r,q.[ \ ].p,s.[;
then
A4: not x in ].p,s.[ by XBOOLE_0:def 5;
A5: r <= x by A3,Th3;
A6: x < q by A3,Th3;
not(p < x & x < s) by A4,Th4;
then x in [.r,p.] or x in [.s,q.[ by A5,A6,Th1,Th3;
hence thesis by XBOOLE_0:def 3;
end;
assume x in [.r,p.] \/ [.s,q.[;
then x in [.r,p.] or x in [.s,q.[ by XBOOLE_0:def 3;
then
A7: r <= x & x <= p or s <= x & x < q by Th1,Th3;
then
A8: r <= x by A1,XXREAL_0:2;
x < q by A2,A7,XXREAL_0:2;
then
A9: x in [.r,q.[ by A8,Th3;
not x in ].p,s.[ by A7,Th4;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th299:
r < s & p <= q implies ].r,q.] \ ].p,s.[ = ].r,p.] \/ [.s,q.]
proof
assume that
A1: r < s and
A2: p <= q;
let x be ExtReal;
thus x in ].r,q.] \ ].p,s.[ implies x in ].r,p.] \/ [.s,q.]
proof
assume
A3: x in ].r,q.] \ ].p,s.[;
then
A4: not x in ].p,s.[ by XBOOLE_0:def 5;
A5: r < x by A3,Th2;
A6: x <= q by A3,Th2;
not(p < x & x < s) by A4,Th4;
then x in ].r,p.] or x in [.s,q.] by A5,A6,Th1,Th2;
hence thesis by XBOOLE_0:def 3;
end;
assume x in ].r,p.] \/ [.s,q.];
then x in ].r,p.] or x in [.s,q.] by XBOOLE_0:def 3;
then
A7: r < x & x <= p or s <= x & x <= q by Th1,Th2;
then
A8: r < x by A1,XXREAL_0:2;
x <= q by A2,A7,XXREAL_0:2;
then
A9: x in ].r,q.] by A8,Th2;
not x in ].p,s.[ by A7,Th4;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th300:
r <= s & p <= q implies [.r,q.] \ ].p,s.[ = [.r,p.] \/ [.s,q.]
proof
assume that
A1: r <= s and
A2: p <= q;
let x be ExtReal;
thus x in [.r,q.] \ ].p,s.[ implies x in [.r,p.] \/ [.s,q.]
proof
assume
A3: x in [.r,q.] \ ].p,s.[;
then
A4: not x in ].p,s.[ by XBOOLE_0:def 5;
A5: r <= x by A3,Th1;
A6: x <= q by A3,Th1;
not(p < x & x < s) by A4,Th4;
then x in [.r,p.] or x in [.s,q.] by A5,A6,Th1;
hence thesis by XBOOLE_0:def 3;
end;
assume x in [.r,p.] \/ [.s,q.];
then x in [.r,p.] or x in [.s,q.] by XBOOLE_0:def 3;
then
A7: r <= x & x <= p or s <= x & x <= q by Th1;
then
A8: r <= x by A1,XXREAL_0:2;
x <= q by A2,A7,XXREAL_0:2;
then
A9: x in [.r,q.] by A8,Th1;
not x in ].p,s.[ by A7,Th4;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th301:
r < s & p <= q implies ].r,q.[ \ [.p,s.[ = ].r,p.[ \/ [.s,q.[
proof
assume that
A1: r < s and
A2: p <= q;
let x be ExtReal;
thus x in ].r,q.[ \ [.p,s.[ implies x in ].r,p.[ \/ [.s,q.[
proof
assume
A3: x in ].r,q.[ \ [.p,s.[;
then
A4: not x in [.p,s.[ by XBOOLE_0:def 5;
A5: r < x by A3,Th4;
A6: x < q by A3,Th4;
not(p <= x & x < s) by A4,Th3;
then x in ].r,p.[ or x in [.s,q.[ by A5,A6,Th3,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume x in ].r,p.[ \/ [.s,q.[;
then x in ].r,p.[ or x in [.s,q.[ by XBOOLE_0:def 3;
then
A7: r < x & x < p or s <= x & x < q by Th3,Th4;
then
A8: r < x by A1,XXREAL_0:2;
x < q by A2,A7,XXREAL_0:2;
then
A9: x in ].r,q.[ by A8,Th4;
not x in [.p,s.[ by A7,Th3;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th302:
r <= s & p <= q implies [.r,q.[ \ [.p,s.[ = [.r,p.[ \/ [.s,q.[
proof
assume that
A1: r <= s and
A2: p <= q;
let x be ExtReal;
thus x in [.r,q.[ \ [.p,s.[ implies x in [.r,p.[ \/ [.s,q.[
proof
assume
A3: x in [.r,q.[ \ [.p,s.[;
then
A4: not x in [.p,s.[ by XBOOLE_0:def 5;
A5: r <= x by A3,Th3;
A6: x < q by A3,Th3;
not(p <= x & x < s) by A4,Th3;
then x in [.r,p.[ or x in [.s,q.[ by A5,A6,Th3;
hence thesis by XBOOLE_0:def 3;
end;
assume x in [.r,p.[ \/ [.s,q.[;
then x in [.r,p.[ or x in [.s,q.[ by XBOOLE_0:def 3;
then
A7: r <= x & x < p or s <= x & x < q by Th3;
then
A8: r <= x by A1,XXREAL_0:2;
x < q by A2,A7,XXREAL_0:2;
then
A9: x in [.r,q.[ by A8,Th3;
not x in [.p,s.[ by A7,Th3;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th303:
r < s & p <= q implies ].r,q.] \ [.p,s.[ = ].r,p.[ \/ [.s,q.]
proof
assume that
A1: r < s and
A2: p <= q;
let x be ExtReal;
thus x in ].r,q.] \ [.p,s.[ implies x in ].r,p.[ \/ [.s,q.]
proof
assume
A3: x in ].r,q.] \ [.p,s.[;
then
A4: not x in [.p,s.[ by XBOOLE_0:def 5;
A5: r < x by A3,Th2;
A6: x <= q by A3,Th2;
not(p <= x & x < s) by A4,Th3;
then x in ].r,p.[ or x in [.s,q.] by A5,A6,Th1,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume x in ].r,p.[ \/ [.s,q.];
then x in ].r,p.[ or x in [.s,q.] by XBOOLE_0:def 3;
then
A7: r < x & x < p or s <= x & x <= q by Th1,Th4;
then
A8: r < x by A1,XXREAL_0:2;
x <= q by A2,A7,XXREAL_0:2;
then
A9: x in ].r,q.] by A8,Th2;
not x in [.p,s.[ by A7,Th3;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th304:
r <= s & p <= q implies [.r,q.] \ [.p,s.[ = [.r,p.[ \/ [.s,q.]
proof
assume that
A1: r <= s and
A2: p <= q;
let x be ExtReal;
thus x in [.r,q.] \ [.p,s.[ implies x in [.r,p.[ \/ [.s,q.]
proof
assume
A3: x in [.r,q.] \ [.p,s.[;
then
A4: not x in [.p,s.[ by XBOOLE_0:def 5;
A5: r <= x by A3,Th1;
A6: x <= q by A3,Th1;
not(p <= x & x < s) by A4,Th3;
then x in [.r,p.[ or x in [.s,q.] by A5,A6,Th1,Th3;
hence thesis by XBOOLE_0:def 3;
end;
assume x in [.r,p.[ \/ [.s,q.];
then x in [.r,p.[ or x in [.s,q.] by XBOOLE_0:def 3;
then
A7: r <= x & x < p or s <= x & x <= q by Th1,Th3;
then
A8: r <= x by A1,XXREAL_0:2;
x <= q by A2,A7,XXREAL_0:2;
then
A9: x in [.r,q.] by A8,Th1;
not x in [.p,s.[ by A7,Th3;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th305:
r < s & p < q implies ].r,q.[ \ ].p,s.] = ].r,p.] \/ ].s,q.[
proof
assume that
A1: r < s and
A2: p < q;
let x be ExtReal;
thus x in ].r,q.[ \ ].p,s.] implies x in ].r,p.] \/ ].s,q.[
proof
assume
A3: x in ].r,q.[ \ ].p,s.];
then
A4: not x in ].p,s.] by XBOOLE_0:def 5;
A5: r < x by A3,Th4;
A6: x < q by A3,Th4;
not(p < x & x <= s) by A4,Th2;
then x in ].r,p.] or x in ].s,q.[ by A5,A6,Th2,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume x in ].r,p.] \/ ].s,q.[;
then x in ].r,p.] or x in ].s,q.[ by XBOOLE_0:def 3;
then
A7: r < x & x <= p or s < x & x < q by Th2,Th4;
then
A8: r < x by A1,XXREAL_0:2;
x < q by A2,A7,XXREAL_0:2;
then
A9: x in ].r,q.[ by A8,Th4;
not x in ].p,s.] by A7,Th2;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th306:
r <= s & p < q implies [.r,q.[ \ ].p,s.] = [.r,p.] \/ ].s,q.[
proof
assume that
A1: r <= s and
A2: p < q;
let x be ExtReal;
thus x in [.r,q.[ \ ].p,s.] implies x in [.r,p.] \/ ].s,q.[
proof
assume
A3: x in [.r,q.[ \ ].p,s.];
then
A4: not x in ].p,s.] by XBOOLE_0:def 5;
A5: r <= x by A3,Th3;
A6: x < q by A3,Th3;
not(p < x & x <= s) by A4,Th2;
then x in [.r,p.] or x in ].s,q.[ by A5,A6,Th1,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume x in [.r,p.] \/ ].s,q.[;
then x in [.r,p.] or x in ].s,q.[ by XBOOLE_0:def 3;
then
A7: r <= x & x <= p or s < x & x < q by Th1,Th4;
then
A8: r <= x by A1,XXREAL_0:2;
x < q by A2,A7,XXREAL_0:2;
then
A9: x in [.r,q.[ by A8,Th3;
not x in ].p,s.] by A7,Th2;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th307:
r < s & p <= q implies ].r,q.] \ ].p,s.] = ].r,p.] \/ ].s,q.]
proof
assume that
A1: r < s and
A2: p <= q;
let x be ExtReal;
thus x in ].r,q.] \ ].p,s.] implies x in ].r,p.] \/ ].s,q.]
proof
assume
A3: x in ].r,q.] \ ].p,s.];
then
A4: not x in ].p,s.] by XBOOLE_0:def 5;
A5: r < x by A3,Th2;
A6: x <= q by A3,Th2;
not(p < x & x <= s) by A4,Th2;
then x in ].r,p.] or x in ].s,q.] by A5,A6,Th2;
hence thesis by XBOOLE_0:def 3;
end;
assume x in ].r,p.] \/ ].s,q.];
then x in ].r,p.] or x in ].s,q.] by XBOOLE_0:def 3;
then
A7: r < x & x <= p or s < x & x <= q by Th2;
then
A8: r < x by A1,XXREAL_0:2;
x <= q by A2,A7,XXREAL_0:2;
then
A9: x in ].r,q.] by A8,Th2;
not x in ].p,s.] by A7,Th2;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th308:
r <= s & p <= q implies [.r,q.] \ ].p,s.] = [.r,p.] \/ ].s,q.]
proof
assume that
A1: r <= s and
A2: p <= q;
let x be ExtReal;
thus x in [.r,q.] \ ].p,s.] implies x in [.r,p.] \/ ].s,q.]
proof
assume
A3: x in [.r,q.] \ ].p,s.];
then
A4: not x in ].p,s.] by XBOOLE_0:def 5;
A5: r <= x by A3,Th1;
A6: x <= q by A3,Th1;
not(p < x & x <= s) by A4,Th2;
then x in [.r,p.] or x in ].s,q.] by A5,A6,Th1,Th2;
hence thesis by XBOOLE_0:def 3;
end;
assume x in [.r,p.] \/ ].s,q.];
then x in [.r,p.] or x in ].s,q.] by XBOOLE_0:def 3;
then
A7: r <= x & x <= p or s < x & x <= q by Th1,Th2;
then
A8: r <= x by A1,XXREAL_0:2;
x <= q by A2,A7,XXREAL_0:2;
then
A9: x in [.r,q.] by A8,Th1;
not x in ].p,s.] by A7,Th2;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th309:
r <= s & p <= q implies ].r,q.[ \ [.p,s.] = ].r,p.[ \/ ].s,q.[
proof
assume that
A1: r <= s and
A2: p <= q;
let x be Real;
thus x in ].r,q.[ \ [.p,s.] implies x in ].r,p.[ \/ ].s,q.[
proof
assume
A3: x in ].r,q.[ \ [.p,s.];
then
A4: not x in [.p,s.] by XBOOLE_0:def 5;
A5: r < x by A3,Th4;
A6: x < q by A3,Th4;
not(p <= x & x <= s) by A4,Th1;
then x in ].r,p.[ or x in ].s,q.[ by A5,A6,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume x in ].r,p.[ \/ ].s,q.[;
then x in ].r,p.[ or x in ].s,q.[ by XBOOLE_0:def 3;
then
A7: r < x & x < p or s < x & x < q by Th4;
then
A8: r < x by A1,XXREAL_0:2;
x < q by A2,A7,XXREAL_0:2;
then
A9: x in ].r,q.[ by A8,Th4;
not x in [.p,s.] by A7,Th1;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th310:
r <= s & p <= q implies [.r,q.[ \ [.p,s.] = [.r,p.[ \/ ].s,q.[
proof
assume that
A1: r <= s and
A2: p <= q;
let x be ExtReal;
thus x in [.r,q.[ \ [.p,s.] implies x in [.r,p.[ \/ ].s,q.[
proof
assume
A3: x in [.r,q.[ \ [.p,s.];
then
A4: not x in [.p,s.] by XBOOLE_0:def 5;
A5: r <= x by A3,Th3;
A6: x < q by A3,Th3;
not(p <= x & x <= s) by A4,Th1;
then x in [.r,p.[ or x in ].s,q.[ by A5,A6,Th3,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume x in [.r,p.[ \/ ].s,q.[;
then x in [.r,p.[ or x in ].s,q.[ by XBOOLE_0:def 3;
then
A7: r <= x & x < p or s < x & x < q by Th3,Th4;
then
A8: r <= x by A1,XXREAL_0:2;
x < q by A2,A7,XXREAL_0:2;
then
A9: x in [.r,q.[ by A8,Th3;
not x in [.p,s.] by A7,Th1;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th311:
r < s & p <= q implies ].r,q.] \ [.p,s.] = ].r,p.[ \/ ].s,q.]
proof
assume that
A1: r < s and
A2: p <= q;
let x be ExtReal;
thus x in ].r,q.] \ [.p,s.] implies x in ].r,p.[ \/ ].s,q.]
proof
assume
A3: x in ].r,q.] \ [.p,s.];
then
A4: not x in [.p,s.] by XBOOLE_0:def 5;
A5: r < x by A3,Th2;
A6: x <= q by A3,Th2;
not(p <= x & x <= s) by A4,Th1;
then x in ].r,p.[ or x in ].s,q.] by A5,A6,Th2,Th4;
hence thesis by XBOOLE_0:def 3;
end;
assume x in ].r,p.[ \/ ].s,q.];
then x in ].r,p.[ or x in ].s,q.] by XBOOLE_0:def 3;
then
A7: r < x & x < p or s < x & x <= q by Th2,Th4;
then
A8: r < x by A1,XXREAL_0:2;
x <= q by A2,A7,XXREAL_0:2;
then
A9: x in ].r,q.] by A8,Th2;
not x in [.p,s.] by A7,Th1;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th312:
r <= s & p <= q implies [.r,q.] \ [.p,s.] = [.r,p.[ \/ ].s,q.]
proof
assume that
A1: r <= s and
A2: p <= q;
let x be ExtReal;
thus x in [.r,q.] \ [.p,s.] implies x in [.r,p.[ \/ ].s,q.]
proof
assume
A3: x in [.r,q.] \ [.p,s.];
then
A4: not x in [.p,s.] by XBOOLE_0:def 5;
A5: r <= x by A3,Th1;
A6: x <= q by A3,Th1;
not(p <= x & x <= s) by A4,Th1;
then x in [.r,p.[ or x in ].s,q.] by A5,A6,Th2,Th3;
hence thesis by XBOOLE_0:def 3;
end;
assume x in [.r,p.[ \/ ].s,q.];
then x in [.r,p.[ or x in ].s,q.] by XBOOLE_0:def 3;
then
A7: r <= x & x < p or s < x & x <= q by Th2,Th3;
then
A8: r <= x by A1,XXREAL_0:2;
x <= q by A2,A7,XXREAL_0:2;
then
A9: x in [.r,q.] by A8,Th1;
not x in [.p,s.] by A7,Th1;
hence thesis by A9,XBOOLE_0:def 5;
end;
theorem Th313:
r <= p & p <= q implies ].r,q.[ \ {p} = ].r,p.[ \/ ].p,q.[
proof
[.p,p.] = {p} by Th17;
hence thesis by Th309;
end;
theorem Th314:
r <= p & p <= q implies [.r,q.[ \ {p} = [.r,p.[ \/ ].p,q.[
proof
[.p,p.] = {p} by Th17;
hence thesis by Th310;
end;
theorem Th315:
r < p & p <= q implies ].r,q.] \ {p} = ].r,p.[ \/ ].p,q.]
proof
[.p,p.] = {p} by Th17;
hence thesis by Th311;
end;
theorem Th316:
r <= p & p <= q implies [.r,q.] \ {p} = [.r,p.[ \/ ].p,q.]
proof
[.p,p.] = {p} by Th17;
hence thesis by Th312;
end;
theorem Th317:
r < q & p <= q implies ].r,q.] \ ].p,q.[ = ].r,p.] \/ {q}
proof
[.q,q.] = {q} by Th17;
hence thesis by Th299;
end;
theorem Th318:
r <= q & p <= q implies [.r,q.] \ ].p,q.[ = [.r,p.] \/ {q}
proof
[.q,q.] = {q} by Th17;
hence thesis by Th300;
end;
theorem Th319:
r < q & p <= q implies ].r,q.] \ [.p,q.[ = ].r,p.[ \/ {q}
proof
[.q,q.] = {q} by Th17;
hence thesis by Th303;
end;
theorem Th320:
r <= q & p <= q implies [.r,q.] \ [.p,q.[ = [.r,p.[ \/ {q}
proof
[.q,q.] = {q} by Th17;
hence thesis by Th304;
end;
theorem Th321:
p <= s & p < q implies [.p,q.[ \ ].p,s.[ = {p} \/ [.s,q.[
proof
[.p,p.] = {p} by Th17;
hence thesis by Th298;
end;
theorem Th322:
p <= s & p <= q implies [.p,q.] \ ].p,s.[ = {p} \/ [.s,q.]
proof
[.p,p.] = {p} by Th17;
hence thesis by Th300;
end;
theorem Th323:
p <= s & p < q implies [.p,q.[ \ ].p,s.] = {p} \/ ].s,q.[
proof
[.p,p.] = {p} by Th17;
hence thesis by Th306;
end;
theorem Th324:
p <= s & p <= q implies [.p,q.] \ ].p,s.] = {p} \/ ].s,q.]
proof
[.p,p.] = {p} by Th17;
hence thesis by Th308;
end;
theorem Th325:
p < q implies [.-infty,q.[ \ ].p,s.[ = [.-infty,p.] \/ [.s,q.[
by Th298,XXREAL_0:5;
theorem Th326:
p <= q implies [.-infty,q.] \ ].p,s.[ = [.-infty,p.] \/ [.s,q.]
proof
-infty <= s by XXREAL_0:5;
hence thesis by Th300;
end;
theorem Th327:
p <= q implies [.-infty,q.[ \ [.p,s.[ = [.-infty,p.[ \/ [.s,q.[
proof
-infty <= s by XXREAL_0:5;
hence thesis by Th302;
end;
theorem Th328:
p <= q implies [.-infty,q.] \ [.p,s.[ = [.-infty,p.[ \/ [.s,q.]
proof
-infty <= s by XXREAL_0:5;
hence thesis by Th304;
end;
theorem Th329:
p < q implies [.-infty,q.[ \ ].p,s.] = [.-infty,p.] \/ ].s,q.[
by Th306,XXREAL_0:5;
theorem Th330:
p <= q implies [.-infty,q.] \ ].p,s.] = [.-infty,p.] \/ ].s,q.]
proof
-infty <= s by XXREAL_0:5;
hence thesis by Th308;
end;
theorem Th331:
p <= q implies [.-infty,q.[ \ [.p,s.] = [.-infty,p.[ \/ ].s,q.[
proof
-infty <= s by XXREAL_0:5;
hence thesis by Th310;
end;
theorem Th332:
p <= q implies [.-infty,q.] \ [.p,s.] = [.-infty,p.[ \/ ].s,q.]
proof
-infty <= s by XXREAL_0:5;
hence thesis by Th312;
end;
theorem Th333:
for s being Real holds p < q
implies ].-infty,q.[ \ ].p,s.[ = ].-infty,p.] \/ [.s,q.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
then -infty < s by XXREAL_0:12;
hence thesis by Th297;
end;
theorem Th334:
for s being Real holds p <= q
implies ].-infty,q.] \ ].p,s.[ = ].-infty,p.] \/ [.s,q.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th299,XXREAL_0:12;
end;
theorem Th335:
for s being Real holds p <= q
implies ].-infty,q.[ \ [.p,s.[ = ].-infty,p.[ \/ [.s,q.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th301,XXREAL_0:12;
end;
theorem Th336:
for s being Real holds p <= q
implies ].-infty,q.] \ [.p,s.[ = ].-infty,p.[ \/ [.s,q.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th303,XXREAL_0:12;
end;
theorem Th337:
for s being Real holds p < q
implies ].-infty,q.[ \ ].p,s.] = ].-infty,p.] \/ ].s,q.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
then -infty < s by XXREAL_0:12;
hence thesis by Th305;
end;
theorem Th338:
for s being Real holds p <= q
implies ].-infty,q.] \ ].p,s.] = ].-infty,p.] \/ ].s,q.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th307,XXREAL_0:12;
end;
theorem Th339:
p <= q implies ].-infty,q.[ \ [.p,s.] = ].-infty,p.[ \/ ].s,q.[
proof
-infty <= s by XXREAL_0:5;
hence thesis by Th309;
end;
theorem Th340:
for s being Real holds p <= q
implies ].-infty,q.] \ [.p,s.] = ].-infty,p.[ \/ ].s,q.]
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th311,XXREAL_0:12;
end;
theorem Th341:
p <= q implies [.-infty,q.[ \ {p} = [.-infty,p.[ \/ ].p,q.[
proof
-infty <= p by XXREAL_0:5;
hence thesis by Th314;
end;
theorem Th342:
p <= q implies [.-infty,q.] \ {p} = [.-infty,p.[ \/ ].p,q.]
proof
-infty <= p by XXREAL_0:5;
hence thesis by Th316;
end;
theorem
p <= q implies [.-infty,q.] \ ].p,q.[ = [.-infty,p.] \/ {q}
proof
-infty <= q by XXREAL_0:5;
hence thesis by Th318;
end;
theorem
p <= q implies [.-infty,q.] \ [.p,q.[ = [.-infty,p.[ \/ {q}
proof
-infty <= q by XXREAL_0:5;
hence thesis by Th320;
end;
theorem
[.-infty,q.] \ ].-infty,s.[ = {-infty} \/ [.s,q.]
proof
A1: -infty <= s by XXREAL_0:5;
-infty <= q by XXREAL_0:5;
hence thesis by A1,Th322;
end;
theorem
[.-infty,q.] \ ].-infty,s.] = {-infty} \/ ].s,q.]
proof
A1: -infty <= s by XXREAL_0:5;
-infty <= q by XXREAL_0:5;
hence thesis by A1,Th324;
end;
theorem
for q being Real holds
[.-infty,q.[ \ ].-infty,s.[ = {-infty} \/ [.s,q.[
proof
let q be Real;
A1: q in REAL by XREAL_0:def 1;
-infty <= s by XXREAL_0:5;
hence thesis by A1,Th321,XXREAL_0:12;
end;
theorem
for q being Real holds
[.-infty,q.[ \ ].-infty,s.] = {-infty} \/ ].s,q.[
proof
let q be Real;
A1: q in REAL by XREAL_0:def 1;
-infty <= s by XXREAL_0:5;
hence thesis by A1,Th323,XXREAL_0:12;
end;
theorem Th349:
p <= q implies ].-infty,q.[ \ {p} = ].-infty,p.[ \/ ].p,q.[
proof
-infty <= p by XXREAL_0:5;
hence thesis by Th313;
end;
theorem Th350:
for p being Real holds p <= q
implies ].-infty,q.] \ {p} = ].-infty,p.[ \/ ].p,q.]
proof
let p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th315,XXREAL_0:12;
end;
theorem
for q being Real holds p <= q
implies ].-infty,q.] \ ].p,q.[ = ].-infty,p.] \/ {q}
proof
let q be Real;
q in REAL by XREAL_0:def 1;
hence thesis by Th317,XXREAL_0:12;
end;
theorem
for q being Real holds p <= q
implies ].-infty,q.] \ [.p,q.[ = ].-infty,p.[ \/ {q}
proof
let q be Real;
q in REAL by XREAL_0:def 1;
hence thesis by Th319,XXREAL_0:12;
end;
theorem
r < s implies ].r,+infty.] \ ].p,s.[ = ].r,p.] \/ [.s,+infty.]
by Th299,XXREAL_0:3;
theorem
r <= s implies [.r,+infty.] \ ].p,s.[ = [.r,p.] \/ [.s,+infty.]
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th300;
end;
theorem
r < s implies ].r,+infty.[ \ [.p,s.[ = ].r,p.[ \/ [.s,+infty.[
by Th301,XXREAL_0:3;
theorem
r <= s implies [.r,+infty.[ \ [.p,s.[ = [.r,p.[ \/ [.s,+infty.[
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th302;
end;
theorem
r < s implies ].r,+infty.] \ [.p,s.[ = ].r,p.[ \/ [.s,+infty.]
by Th303,XXREAL_0:3;
theorem
r <= s implies [.r,+infty.] \ [.p,s.[ = [.r,p.[ \/ [.s,+infty.]
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th304;
end;
theorem
r < s implies ].r,+infty.] \ ].p,s.] = ].r,p.] \/ ].s,+infty.]
by Th307,XXREAL_0:3;
theorem
r <= s implies [.r,+infty.] \ ].p,s.] = [.r,p.] \/ ].s,+infty.]
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th308;
end;
theorem
r <= s implies ].r,+infty.[ \ [.p,s.] = ].r,p.[ \/ ].s,+infty.[
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th309;
end;
theorem
r <= s implies [.r,+infty.[ \ [.p,s.] = [.r,p.[ \/ ].s,+infty.[
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th310;
end;
theorem
r < s implies ].r,+infty.] \ [.p,s.] = ].r,p.[ \/ ].s,+infty.]
by Th311,XXREAL_0:3;
theorem
r <= s implies [.r,+infty.] \ [.p,s.] = [.r,p.[ \/ ].s,+infty.]
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th312;
end;
theorem
r <= p implies ].r,+infty.[ \ {p} = ].r,p.[ \/ ].p,+infty.[
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th313;
end;
theorem
r <= p implies [.r,+infty.[ \ {p} = [.r,p.[ \/ ].p,+infty.[
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th314;
end;
theorem
r < p implies ].r,+infty.] \ {p} = ].r,p.[ \/ ].p,+infty.]
by Th315,XXREAL_0:3;
theorem
r <= p implies [.r,+infty.] \ {p} = [.r,p.[ \/ ].p,+infty.]
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th316;
end;
theorem
[.r,+infty.] \ ].p,+infty.[ = [.r,p.] \/ {+infty}
proof
A1: r <= +infty by XXREAL_0:3;
p <= +infty by XXREAL_0:3;
hence thesis by A1,Th318;
end;
theorem
[.r,+infty.] \ [.p,+infty.[ = [.r,p.[ \/ {+infty}
proof
A1: r <= +infty by XXREAL_0:3;
p <= +infty by XXREAL_0:3;
hence thesis by A1,Th320;
end;
theorem
for r being Real
holds ].r,+infty.] \ ].p,+infty.[ = ].r,p.] \/ {+infty}
proof
let r be Real;
r in REAL by XREAL_0:def 1;
then r < +infty by XXREAL_0:9;
hence thesis by Th317,XXREAL_0:3;
end;
theorem
for r being Real
holds ].r,+infty.] \ [.p,+infty.[ = ].r,p.[ \/ {+infty}
proof
let r be Real;
r in REAL by XREAL_0:def 1;
then r < +infty by XXREAL_0:9;
hence thesis by Th319,XXREAL_0:3;
end;
theorem
p <= s implies [.p,+infty.] \ ].p,s.[ = {p} \/ [.s,+infty.]
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th322;
end;
theorem
p <= s implies [.p,+infty.] \ ].p,s.] = {p} \/ ].s,+infty.]
proof
p <= +infty by XXREAL_0:3;
hence thesis by Th324;
end;
theorem
[.-infty,+infty.] \ ].p,s.[ = [.-infty,p.] \/ [.s,+infty.]
by Th326,XXREAL_0:3;
theorem
[.-infty,+infty.[ \ [.p,s.[ = [.-infty,p.[ \/ [.s,+infty.[
by Th327,XXREAL_0:3;
theorem
[.-infty,+infty.] \ [.p,s.[ = [.-infty,p.[ \/ [.s,+infty.]
by Th328,XXREAL_0:3;
theorem
[.-infty,+infty.] \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.]
by Th330,XXREAL_0:3;
theorem
[.-infty,+infty.[ \ [.p,s.] = [.-infty,p.[ \/ ].s,+infty.[
by Th331,XXREAL_0:3;
theorem
[.-infty,+infty.] \ [.p,s.] = [.-infty,p.[ \/ ].s,+infty.]
by Th332,XXREAL_0:3;
theorem
for s being Real holds
].-infty,+infty.] \ ].p,s.[ = ].-infty,p.] \/ [.s,+infty.]
by Th334,XXREAL_0:3;
theorem
for s being Real holds REAL \ [.p,s.[ = ].-infty,p.[ \/ [.s,+infty.[
by Th224,Th335,XXREAL_0:3;
theorem
for s being Real holds
].-infty,+infty.] \ [.p,s.[ = ].-infty,p.[ \/ [.s,+infty.]
by Th336,XXREAL_0:3;
theorem
for s being Real holds
].-infty,+infty.] \ ].p,s.] = ].-infty,p.] \/ ].s,+infty.]
by Th338,XXREAL_0:3;
theorem
REAL \ [.p,s.] = ].-infty,p.[ \/ ].s,+infty.[ by Th224,Th339,XXREAL_0:3;
theorem
for s being Real holds
].-infty,+infty.] \ [.p,s.] = ].-infty,p.[ \/ ].s,+infty.]
by Th340,XXREAL_0:3;
theorem
[.-infty,+infty.[ \ {p} = [.-infty,p.[ \/ ].p,+infty.[ by Th341,XXREAL_0:3;
theorem
[.-infty,+infty.] \ {p} = [.-infty,p.[ \/ ].p,+infty.] by Th342,XXREAL_0:3;
theorem
REAL \ {p} = ].-infty,p.[ \/ ].p,+infty.[ by Th224,Th349,XXREAL_0:3;
theorem
for p being Real holds
].-infty,+infty.] \ {p} = ].-infty,p.[ \/ ].p,+infty.]
by Th350,XXREAL_0:3;
theorem
for p being Real holds
r < s implies ].r,+infty.[ \ ].p,s.[ = ].r,p.] \/ [.s,+infty.[
proof
let p be Real;
p in REAL by XREAL_0:def 1;
then p < +infty by XXREAL_0:9;
hence thesis by Th297;
end;
theorem
for p being Real holds
r <= s implies [.r,+infty.[ \ ].p,s.[ = [.r,p.] \/ [.s,+infty.[
proof
let p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th298,XXREAL_0:9;
end;
theorem
for p being Real holds
r < s implies ].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[
proof
let p be Real;
p in REAL by XREAL_0:def 1;
then p < +infty by XXREAL_0:9;
hence thesis by Th305;
end;
theorem
for p being Real holds
r <= s implies [.r,+infty.[ \ ].p,s.] = [.r,p.] \/ ].s,+infty.[
proof
let p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th306,XXREAL_0:9;
end;
theorem
for p being Real holds
p <= s implies [.p,+infty.[ \ ].p,s.] = {p} \/ ].s,+infty.[
proof
let p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th323,XXREAL_0:9;
end;
theorem
for p being Real holds
[.-infty,+infty.[ \ ].p,s.[ = [.-infty,p.] \/ [.s,+infty.[
proof
let p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th325,XXREAL_0:9;
end;
theorem
for p being Real holds
[.-infty,+infty.[ \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.[
proof
let p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th329,XXREAL_0:9;
end;
theorem
for s,p being Real holds REAL \ ].p,s.[ = ].-infty,p.] \/ [.s,+infty.[
proof
let s,p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th224,Th333,XXREAL_0:9;
end;
theorem
for s,p being Real holds REAL \ ].p,s.] = ].-infty,p.] \/ ].s,+infty.[
proof
let s,p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th224,Th337,XXREAL_0:9;
end;
theorem
for p being Real holds
p <= s implies [.p,+infty.[ \ ].p,s.[ = {p} \/ [.s,+infty.[
proof
let p be Real;
p in REAL by XREAL_0:def 1;
hence thesis by Th321,XXREAL_0:9;
end;
theorem Th401:
r < s implies [.r,s.] \ [.r,s.[ = {s}
proof
[.s,s.] = {s} by Th17;
hence thesis by Th184;
end;
theorem Th402:
r < s implies ].r,s.] \ ].r,s.[ = {s}
proof
[.s,s.] = {s} by Th17;
hence thesis by Th188;
end;
theorem Th403:
r < t implies [.r,t.] \ ].r,t.] = {r}
proof
[.r,r.] = {r} by Th17;
hence thesis by Th192;
end;
theorem Th404:
r < t implies [.r,t.[ \ ].r,t.[ = {r}
proof
[.r,r.] = {r} by Th17;
hence thesis by Th196;
end;
theorem
for s being Real holds [.-infty,s.] \ [.-infty,s.[ = {s}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th401,XXREAL_0:12;
end;
theorem
for s being Real holds ].-infty,s.] \ ].-infty,s.[ = {s}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th402,XXREAL_0:12;
end;
theorem
for s being Real holds [.-infty,s.] \ ].-infty,s.] = {-infty}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th403,XXREAL_0:12;
end;
theorem
for s being Real holds [.-infty,s.[ \ ].-infty,s.[ = {-infty}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th404,XXREAL_0:12;
end;
theorem
for s being Real holds [.s,+infty.] \ [.s,+infty.[ = {+infty}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th401,XXREAL_0:9;
end;
theorem
for s being Real holds ].s,+infty.] \ ].s,+infty.[ = {+infty}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th402,XXREAL_0:9;
end;
theorem
for s being Real holds [.s,+infty.] \ ].s,+infty.] = {s}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th403,XXREAL_0:9;
end;
theorem
for s being Real holds [.s,+infty.[ \ ].s,+infty.[ = {s}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th404,XXREAL_0:9;
end;
:: analogous to Th165
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,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 Th1,Th3;
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 Th1,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 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 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;
:: analogous to Th138
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,Th1;
hence x = s by A5,XXREAL_0:1;
end;
assume
A6: x = s;
A7: s in [.r,s.] by A1,Th1;
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 & 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 Th1;
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,Th1;
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 & 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 Th1;
p <= s by A4,Th1;
hence x = s by A5,XXREAL_0:1;
end;
assume
A6: x = s;
A7: s in [.r,s.] by A1,Th1;
s in [.s,t.] by A2,Th1;
hence x in [.r,s.] /\ [.s,t.] by A6,A7,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
:: special cases of Th128-Th132
theorem
[.-infty,s.] = ].-infty,s.[ \/ {-infty,s} by Th128,XXREAL_0:5;
theorem
[.-infty,s.] = [.-infty,s.[ \/ {s} by Th129,XXREAL_0:5;
theorem
[.-infty,s.] = {-infty} \/ ].-infty,s.] by Th130,XXREAL_0:5;
theorem
for s being Real holds [.-infty,s.[ = {-infty} \/ ].-infty,s.[
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th131,XXREAL_0:12;
end;
theorem
for s being Real holds ].-infty,s.] = ].-infty,s.[ \/ {s}
proof
let s be Real;
s in REAL by XREAL_0:def 1;
hence thesis by Th132,XXREAL_0:12;
end;
theorem
[.r,+infty.] = ].r,+infty.[ \/ {r,+infty} by Th128,XXREAL_0:3;
theorem
[.r,+infty.] = [.r,+infty.[ \/ {+infty} by Th129,XXREAL_0:3;
theorem
[.r,+infty.] = {r} \/ ].r,+infty.] by Th130,XXREAL_0:3;
theorem
for r being Real holds [.r,+infty.[ = {r} \/ ].r,+infty.[
proof
let r be Real;
r in REAL by XREAL_0:def 1;
hence thesis by Th131,XXREAL_0:9;
end;
theorem
for r being Real holds ].r,+infty.] = ].r,+infty.[ \/ {+infty}
proof
let r be Real;
r in REAL by XREAL_0:def 1;
hence thesis by Th132,XXREAL_0:9;
end;