:: Properties of the Intervals of Real Numbers
:: by J\'ozef Bia{\l}as
::
:: Received January 12, 1993
:: Copyright (c) 1993-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 NUMBERS, SUPINF_1, SUBSET_1, TARSKI, XXREAL_1, ARYTM_3, XXREAL_0,
CARD_1, XXREAL_2, ORDINAL2, REAL_1, SUPINF_2, MEMBERED, ARYTM_1,
XBOOLE_0, MEASURE5, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0,
XREAL_0, REAL_1, XXREAL_1, RCOMP_1, XXREAL_2,
XXREAL_3, SUPINF_1, SUPINF_2;
constructors DOMAIN_1, REAL_1, RCOMP_1, SUPINF_2, SUPINF_1, FINSET_1;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, XXREAL_1,
XXREAL_2, SUBSET_1, FINSET_1, ORDINAL1;
requirements SUBSET, BOOLE, NUMERALS, REAL;
definitions MEMBERED, XBOOLE_0;
equalities XXREAL_1, XXREAL_3;
theorems TARSKI, XREAL_0, XBOOLE_0, XREAL_1, XXREAL_0, NUMBERS, XXREAL_1,
XXREAL_2, XXREAL_3;
begin :: Some theorems about R_eal numbers
reserve a,b for R_eal;
:: PROPERTIES OF THE INTERVALS
scheme
RSetEq {P[set]} : for X1,X2 being Subset of REAL st (for x being R_eal holds
x in X1 iff P[x]) & (for x being R_eal holds x in X2 iff P[x]) holds X1 = X2
proof
let A1,A2 be Subset of REAL such that
A1: for x being R_eal holds x in A1 iff P[x] and
A2: for x being R_eal holds x in A2 iff P[x];
thus A1 c= A2
proof
let x be Real;
assume
A3: x in A1;
then x in REAL;
then reconsider x as R_eal by NUMBERS:31;
P[x] by A1,A3;
hence thesis by A2;
end;
let x be Real;
assume
A4: x in A2;
then x in REAL;
then reconsider x as R_eal by NUMBERS:31;
P[x] by A2,A4;
hence thesis by A1;
end;
definition
let a,b be R_eal;
redefine func ].a,b.[ -> Subset of REAL means :: redefines ]. (XXREAL_1, definition)
for x being R_eal holds x in it iff a < x & x < b;
coherence
proof
for x being set st x in ]. a,b .[ holds x in REAL;
hence thesis;
end;
compatibility
proof
let X be Subset of REAL;
thus X = ].a,b.[ implies for x being R_eal holds x in X iff a < x & x < b
by XXREAL_1:4;
assume
A1: for x being R_eal holds x in X iff a < x & x < b;
thus X c= ].a,b.[
proof
let x be Real;
assume
A2: x in X;
then x in REAL;
then reconsider t=x as R_eal by NUMBERS:31;
a < t & t < b by A1,A2;
hence thesis;
end;
let x be Real;
reconsider t=x as R_eal by XXREAL_0:def 1;
assume x in ].a,b.[;
then a < t & t < b by XXREAL_1:4;
hence thesis by A1;
end;
end;
definition
let IT be Subset of REAL;
attr IT is open_interval means
ex a,b being R_eal st IT = ].a,b.[;
attr IT is closed_interval means
ex a,b being Real st IT = [.a,b.];
end;
registration
cluster non empty open_interval for Subset of REAL;
existence
proof
take ].-infty,+infty.[;
In(0,REAL) in ].-infty,+infty.[ by XXREAL_1:224;
hence ].-infty,+infty.[ is non empty;
take -infty,+infty;
thus thesis;
end;
cluster non empty closed_interval for Subset of REAL;
existence
proof
take [.0,1.];
thus [.0,1.] is non empty by XXREAL_1:30;
take 0,1;
thus thesis;
end;
end;
definition
let IT be Subset of REAL;
attr IT is right_open_interval means
ex a being Real, b being R_eal st IT = [.a,b.[;
end;
notation
let IT be Subset of REAL;
synonym IT is left_closed_interval for IT is right_open_interval;
end;
definition
let IT be Subset of REAL;
attr IT is left_open_interval means
ex a being R_eal,b being Real st IT = ].a,b.];
end;
notation
let IT be Subset of REAL;
synonym IT is right_closed_interval for IT is left_open_interval;
end;
registration
cluster non empty right_open_interval for Subset of REAL;
existence
proof
take [.0,+infty.[;
0 in [.0,+infty.[ by XXREAL_1:236;
hence [.0,+infty.[ is non empty;
take 0,+infty;
thus thesis;
end;
cluster non empty left_open_interval for Subset of REAL;
existence
proof
take ].-infty,1.];
1 in ].-infty,1.] by XXREAL_1:234;
hence ].-infty,1.] is non empty;
take -infty,1;
thus thesis;
end;
end;
definition
mode Interval is interval Subset of REAL;
end;
reserve A,B for Interval;
registration
cluster open_interval -> interval for Subset of REAL;
coherence;
cluster closed_interval -> interval for Subset of REAL;
coherence;
cluster right_open_interval -> interval for Subset of REAL;
coherence;
cluster left_open_interval -> interval for Subset of REAL;
coherence;
end;
theorem
for I being interval Subset of REAL holds
I is open_interval or I is closed_interval or
I is right_open_interval or I is left_open_interval
proof let I be interval Subset of REAL;
per cases;
suppose
A1: I is left_end right_end;
reconsider a = inf I,b = sup I as R_eal;
A2: a in I & I = [.a,b.] by A1,XXREAL_2:75,def 5;
thus thesis by A1,A2;
end;
suppose
A3: I is non left_end right_end;
set a = inf I, b = sup I;
A4: I = ].a,b.] by A3,XXREAL_2:76;
A5: b in I by A3,XXREAL_2:def 6;
thus thesis by A5,A4;
end;
suppose
A6: I is left_end non right_end;
set a = inf I, b = sup I;
A7: I = [.a,b.[ by A6,XXREAL_2:77;
A8: a in I by A6,XXREAL_2:def 5;
thus thesis by A8,A7;
end;
suppose
I is non left_end non right_end;
then consider a,b being ExtReal such that
A9: a <= b and
A10: I = ].a,b.[ by XXREAL_2:79;
reconsider a,b as R_eal by XXREAL_0:def 1;
a <= b by A9;
hence thesis by A10;
end;
end;
theorem Th2:
for a,b being R_eal st a < b ex x being R_eal st a < x & x < b & x in REAL
proof
let a,b be R_eal;
A1: a in REAL or a in {-infty,+infty} by XBOOLE_0:def 3,XXREAL_0:def 4;
A2: b in REAL or b in {-infty,+infty} by XBOOLE_0:def 3,XXREAL_0:def 4;
assume
A3: a < b;
then
A4: ( not a = +infty)& not b = -infty by XXREAL_0:4,6;
per cases by A1,A2,A4,TARSKI:def 2;
suppose
a in REAL & b in REAL;
then consider x,y being Real such that
A5: x = a & y = b and
x<=y by A3;
consider z being Real such that
A6: x<z & z<y by A3,A5,XREAL_1:5;
reconsider z as Element of REAL by XREAL_0:def 1;
reconsider o = z as R_eal by XXREAL_0:def 1;
take o;
thus thesis by A5,A6;
end;
suppose
A7: a in REAL & b = +infty;
then reconsider x = a as Real;
consider z being Real such that
A8: x<z by XREAL_1:1;
reconsider z as Element of REAL by XREAL_0:def 1;
reconsider o = z as R_eal by XXREAL_0:def 1;
take o;
thus thesis by A7,A8,XXREAL_0:9;
end;
suppose
A9: a = -infty & b in REAL;
then reconsider y = b as Real;
consider z being Real such that
A10: z<y by XREAL_1:2;
reconsider z as Element of REAL by XREAL_0:def 1;
reconsider o = z as R_eal by XXREAL_0:def 1;
take o;
thus thesis by A9,A10,XXREAL_0:12;
end;
suppose
A11: a = -infty & b = +infty;
take 0.;
0. = In(0,REAL);
hence thesis by A11;
end;
end;
theorem
for a,b,c being R_eal st a < b & a < c ex x being R_eal st a < x & x <
b & x < c & x in REAL
proof
let a,b,c be R_eal;
A1: min(b,c) = min{b,c} by XXREAL_2:14;
ex o being R_eal st o in {b,c} & o <= c
proof
take c;
thus thesis by TARSKI:def 2;
end;
then
A2: min(b,c) <= c by A1,XXREAL_2:62;
reconsider m = min(b,c) as R_eal by XXREAL_0:def 1;
assume a < b & a < c;
then a < min(b,c) by XXREAL_0:def 9;
then consider x being R_eal such that
A3: a < x & x < m & x in REAL by Th2;
take x;
ex o being R_eal st o in {b,c} & o <= b
proof
take b;
thus thesis by TARSKI:def 2;
end;
then min(b,c) <= b by A1,XXREAL_2:62;
hence thesis by A3,A2,XXREAL_0:2;
end;
theorem
for a,b,c being R_eal st a < c & b < c ex x being R_eal st a < x & b <
x & x < c & x in REAL
proof
let a,b,c be R_eal;
reconsider m = max(a,b) as R_eal by XXREAL_0:def 1;
A1: b in {a,b} by TARSKI:def 2;
assume a < c & b < c;
then max(a,b) < c by XXREAL_0:def 10;
then consider x being R_eal such that
A2: m < x & x < c & x in REAL by Th2;
take x;
max(a,b) = max{a,b} & a in {a,b} by TARSKI:def 2,XXREAL_2:12;
hence thesis by A2,A1,XXREAL_2:61;
end;
definition
let A be ext-real-membered set;
func diameter A -> R_eal equals
:Def6:
sup A - inf A if A <> {} otherwise
0.;
coherence;
consistency;
end;
theorem
for a,b being R_eal holds (a < b implies diameter ].a,b.[ = b - a) & (
b <= a implies diameter ].a,b.[ = 0.)
proof
let a,b being R_eal;
hereby
assume
A1: a < b;
then
A2: sup ].a,b.[ = b by XXREAL_2:32;
].a,b.[ <> {} & inf ].a,b.[ = a by A1,XXREAL_1:33,XXREAL_2:28;
hence diameter ].a,b.[ = b - a by A2,Def6;
end;
assume b <= a;
then ].a,b.[ = {} by XXREAL_1:28;
hence thesis by Def6;
end;
theorem
for a,b being R_eal holds (a <= b implies diameter [.a,b.] = b - a) &
(b < a implies diameter [.a,b.] = 0.)
proof
let a,b being R_eal;
hereby
assume
A1: a <= b;
then
A2: sup [.a,b.] = b by XXREAL_2:29;
[.a,b.] <> {} & inf [.a,b.] = a by A1,XXREAL_1:30,XXREAL_2:25;
hence diameter [.a,b.] = b - a by A2,Def6;
end;
assume b < a;
then [.a,b.] = {} by XXREAL_1:29;
hence thesis by Def6;
end;
theorem
for a,b being R_eal holds (a < b implies diameter [.a,b.[ = b - a) & (
b <= a implies diameter [.a,b.[ = 0.)
proof
let a,b being R_eal;
hereby
assume
A1: a < b;
then
A2: sup [.a,b.[ = b by XXREAL_2:31;
[.a,b.[ <> {} & inf [.a,b.[ = a by A1,XXREAL_1:31,XXREAL_2:26;
hence diameter [.a,b.[ = b - a by A2,Def6;
end;
assume b <= a;
then [.a,b.[ = {} by XXREAL_1:27;
hence thesis by Def6;
end;
theorem
for a,b being R_eal holds (a < b implies diameter ].a,b.] = b - a) & (
b <= a implies diameter ].a,b.] = 0.)
proof
let a,b being R_eal;
hereby
assume
A1: a < b;
then
A2: sup ].a,b.] = b by XXREAL_2:30;
].a,b.] <> {} & inf ].a,b.] = a by A1,XXREAL_1:32,XXREAL_2:27;
hence diameter ].a,b.] = b - a by A2,Def6;
end;
assume b <= a;
then ].a,b.] = {} by XXREAL_1:26;
hence thesis by Def6;
end;
theorem
for a,b being R_eal holds a = -infty & b = +infty & (A = ].a,b.[ or A
= [.a,b.] or A = [.a,b.[ or A = ].a,b.]) implies diameter(A) = +infty
proof
let a,b be R_eal;
assume that
A1: a = -infty & b = +infty and
A2: A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.];
A3: sup A = +infty & inf A = -infty by A1,A2,XXREAL_2:25,26,27,28,29,30,31,32;
then A is non empty by XXREAL_2:40;
then diameter(A) = b - a by A1,A3,Def6
.= +infty by A1,XXREAL_3:13;
hence thesis;
end;
registration
cluster empty -> open_interval for Subset of REAL;
coherence
proof
let S be Subset of REAL;
assume S is empty;
then S = ].0.,0..[;
hence thesis;
end;
end;
theorem
diameter {} = 0. by Def6;
Lm1: diameter A >= 0
proof
per cases;
suppose
A is empty;
hence thesis by Def6;
end;
suppose
A is non empty;
then inf A <= sup A by XXREAL_2:40;
then sup A - inf A >= 0 by XXREAL_3:40;
hence thesis by Def6;
end;
end;
Lm2: A c= B implies diameter A <= diameter B
proof
assume
A1: A c= B;
per cases;
suppose
A = {};
then diameter A = 0 by Def6;
hence thesis by Lm1;
end;
suppose
A2: A <> {};
then B <> {} by A1;
then
A3: diameter B = sup B - inf B by Def6;
A4: sup A <= sup B & inf B <= inf A by A1,XXREAL_2:59,60;
diameter A = sup A - inf A by A2,Def6;
hence thesis by A3,A4,XXREAL_3:37;
end;
end;
theorem
A c= B & B =[.a,b.] & b <= a implies diameter(A) = 0. & diameter(B) = 0.
proof
assume that
A1: A c= B and
A2: B =[.a,b.] and
A3: b <= a;
per cases by A3,XXREAL_0:1;
suppose
A4: a = b;
then B = {a} by A2,XXREAL_1:17;
then inf B = a & sup B = a by XXREAL_2:11,13;
then
A5: diameter B = a - a by A2,A4,Def6
.= 0 by XXREAL_3:7;
then diameter A <= 0 by A1,Lm2;
hence thesis by A5,Lm1;
end;
suppose
b < a;
then
A6: B = {} by A2,XXREAL_1:29;
then A = {} by A1;
hence thesis by A6,Def6;
end;
end;
theorem
A c= B implies diameter A <= diameter B by Lm2;
theorem
0. <= diameter A by Lm1;
theorem
for X being Subset of REAL holds X is non empty closed_interval
iff ex a,b being Real st a <= b & X = [.a,b.]
by XXREAL_1:29,XXREAL_1:30;