:: Properties of the Intervals of Real Numbers
:: by J\'ozef Bia{\l}as
::
:: Received January 12, 1993
:: Copyright (c) 1993-2017 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, 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, ARITHM, REAL;
begin :: Some theorems about R_eal numbers
reserve a,b for R_eal;
:: PROPERTIES OF THE INTERVALS
scheme :: MEASURE5:sch 1
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;
definition
let a,b be R_eal;
redefine func ].a,b.[ -> Subset of REAL means
:: MEASURE5:def 1
for x being R_eal holds x in it iff a < x & x < b;
end;
definition
let IT be Subset of REAL;
attr IT is open_interval means
:: MEASURE5:def 2
ex a,b being R_eal st IT = ].a,b.[;
attr IT is closed_interval means
:: MEASURE5:def 3
ex a,b being Real st IT = [.a,b.];
end;
registration
cluster non empty open_interval for Subset of REAL;
cluster non empty closed_interval for Subset of REAL;
end;
definition
let IT be Subset of REAL;
attr IT is right_open_interval means
:: MEASURE5:def 4
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
:: MEASURE5:def 5
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;
cluster non empty left_open_interval for Subset of REAL;
end;
definition
mode Interval is interval Subset of REAL;
end;
reserve A,B for Interval;
registration
cluster open_interval -> interval for Subset of REAL;
cluster closed_interval -> interval for Subset of REAL;
cluster right_open_interval -> interval for Subset of REAL;
cluster left_open_interval -> interval for Subset of REAL;
end;
theorem :: MEASURE5:1
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;
theorem :: MEASURE5:2
for a,b being R_eal st a < b ex x being R_eal st a < x & x < b & x in REAL;
theorem :: MEASURE5:3
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;
theorem :: MEASURE5:4
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;
definition
let A be ext-real-membered set;
func diameter A -> R_eal equals
:: MEASURE5:def 6
sup A - inf A if A <> {} otherwise
0.;
end;
theorem :: MEASURE5:5
for a,b being R_eal holds (a < b implies diameter ].a,b.[ = b - a) & (
b <= a implies diameter ].a,b.[ = 0.);
theorem :: MEASURE5:6
for a,b being R_eal holds (a <= b implies diameter [.a,b.] = b - a) &
(b < a implies diameter [.a,b.] = 0.);
theorem :: MEASURE5:7
for a,b being R_eal holds (a < b implies diameter [.a,b.[ = b - a) & (
b <= a implies diameter [.a,b.[ = 0.);
theorem :: MEASURE5:8
for a,b being R_eal holds (a < b implies diameter ].a,b.] = b - a) & (
b <= a implies diameter ].a,b.] = 0.);
theorem :: MEASURE5:9
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;
registration
cluster empty -> open_interval for Subset of REAL;
end;
theorem :: MEASURE5:10
diameter {} = 0.;
theorem :: MEASURE5:11
A c= B & B =[.a,b.] & b <= a implies diameter(A) = 0. & diameter(B) = 0.;
theorem :: MEASURE5:12
A c= B implies diameter A <= diameter B;
theorem :: MEASURE5:13
0. <= diameter A;
theorem :: MEASURE5:14
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.];