:: Properties of the Intervals of Real Numbers :: by J\'ozef Bia{\l}as :: :: Received January 12, 1993 :: Copyright (c) 1993-2021 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, 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.];