Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Properties of the Intervals of Real Numbers

by
Jozef Bialas

MML identifier: MEASURE5
[ Mizar article, MML identifier index ]

```environ

vocabulary SUPINF_1, ARYTM_3, RLVECT_1, ARYTM_1, ORDINAL2, RCOMP_1, BOOLE,
MEASURE5, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, REAL_1, SUPINF_1,
SUPINF_2;
constructors REAL_1, SUPINF_2, MEMBERED, XBOOLE_0;
clusters SUBSET_1, XREAL_0, XBOOLE_0, MEMBERED, ZFMISC_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin  :: Some theorems about R_eal numbers

reserve x,y,a,b,a1,b1,a2,b2 for R_eal;

theorem :: MEASURE5:1
x <> -infty & x <> +infty & x <=' y implies
0. <=' y - x;

theorem :: MEASURE5:2
(not (x = -infty & y = -infty) & not (x = +infty & y = +infty) & x <=' y)
implies 0. <=' y - x;

canceled 5;

theorem :: MEASURE5:8
for a,b,c being R_eal holds
(b <> -infty & b <> +infty &
not (a = -infty & c = -infty) & not (a = +infty & c = +infty)) implies
(c - b) + (b - a) = c - a;

theorem :: MEASURE5:9
inf{a1,a2} <=' a1 & inf{a1,a2} <=' a2 &
a1 <=' sup{a1,a2} & a2 <=' sup{a1,a2};

definition let a,b be R_eal;
func [.a,b.] -> Subset of REAL means
:: MEASURE5:def 1
for x being R_eal holds
x in it iff a <=' x & x <=' b & x in REAL;

func ].a,b.[ -> Subset of REAL means
:: MEASURE5:def 2
for x being R_eal holds
x in it iff (a <' x & x <' b & x in REAL);

func ].a,b.] -> Subset of REAL means
:: MEASURE5:def 3
for x being R_eal holds
x in it iff (a <' x & x <=' b & x in REAL);

func [.a,b.[ -> Subset of REAL means
:: MEASURE5:def 4
for x being R_eal holds
x in it iff (a <=' x & x <' b & x in REAL);
end;

definition let IT be Subset of REAL;
attr IT is open_interval means
:: MEASURE5:def 5
ex a,b being R_eal st a <=' b & IT = ].a,b.[;
attr IT is closed_interval means
:: MEASURE5:def 6
ex a,b being R_eal st a <=' b & IT = [.a,b.];
end;

definition
cluster open_interval Subset of REAL;
cluster closed_interval Subset of REAL;
end;

definition let IT be Subset of REAL;
attr IT is right_open_interval means
:: MEASURE5:def 7
ex a,b being R_eal st a <=' b & IT = [.a,b.[;
synonym IT is left_closed_interval;
end;

definition let IT be Subset of REAL;
attr IT is left_open_interval means
:: MEASURE5:def 8
ex a,b being R_eal st a <=' b & IT = ].a,b.];
synonym IT is right_closed_interval;
end;

definition
cluster right_open_interval Subset of REAL;
cluster left_open_interval Subset of REAL;
end;

definition let IT be Subset of REAL;
attr IT is interval means
:: MEASURE5:def 9
IT is open_interval or IT is closed_interval or
IT is right_open_interval or IT is left_open_interval;
end;

definition
cluster interval Subset of REAL;
end;

definition
mode Interval is interval Subset of REAL;
end;

reserve A,B for Interval;

definition
cluster open_interval -> interval Subset of REAL;
cluster closed_interval -> interval Subset of REAL;
cluster right_open_interval -> interval Subset of REAL;
cluster left_open_interval -> interval Subset of REAL;
end;

canceled;

theorem :: MEASURE5:11
for x being set,
a,b being R_eal st
(x in ].a,b.[ or x in [.a,b.] or x in [.a,b.[ or x in ].a,b.]) holds
x is R_eal;

theorem :: MEASURE5:12
for a,b being R_eal st b <' a holds
].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {};

theorem :: MEASURE5:13
for a being R_eal holds
].a,a.[ = {} & [.a,a.[ = {} & ].a,a.] = {};

theorem :: MEASURE5:14
for a being R_eal holds
((a = -infty or a = +infty) implies [.a,a.] = {}) &
((a <> -infty & a <> +infty) implies [.a,a.] = {a});

theorem :: MEASURE5:15
for a,b being R_eal st b <=' a holds
].a,b.[ = {} & [.a,b.[ = {} & ].a,b.] = {} &
[.a,b.] c= {a} & [.a,b.] c= {b};

theorem :: MEASURE5:16
for a,b,c being R_eal st a <' b & b <' c holds b in REAL;

theorem :: MEASURE5:17
for a,b being R_eal st a <' b
ex x being R_eal st a <' x & x <' b & x in REAL;

theorem :: MEASURE5:18
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:19
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;

theorem :: MEASURE5:20
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ & not x in ].a2,b2.[) or
(not x in ].a1,b1.[ & x in ].a2,b2.[));

theorem :: MEASURE5:21
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.[) or (not x in ].a1,b1.[ & x in ].a2,b2.[));

theorem :: MEASURE5:22
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[));

theorem :: MEASURE5:23
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[));

theorem :: MEASURE5:24
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]));

theorem :: MEASURE5:25
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]));

theorem :: MEASURE5:26
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[));

theorem :: MEASURE5:27
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[));

theorem :: MEASURE5:28
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[));

theorem :: MEASURE5:29
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[));

theorem :: MEASURE5:30
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]));

theorem :: MEASURE5:31
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]));

theorem :: MEASURE5:32
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[));

theorem :: MEASURE5:33
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[));

theorem :: MEASURE5:34
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]));

theorem :: MEASURE5:35
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]));

theorem :: MEASURE5:36
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[));

theorem :: MEASURE5:37
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[));

theorem :: MEASURE5:38
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.]) or (not x in [.a1,b1.[ & x in [.a2,b2.]));

theorem :: MEASURE5:39
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.]) or (not x in [.a1,b1.[ & x in [.a2,b2.]));

theorem :: MEASURE5:40
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.]) or (not x in [.a1,b1.] & x in ].a2,b2.]));

theorem :: MEASURE5:41
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.]) or (not x in [.a1,b1.] & x in ].a2,b2.]));

theorem :: MEASURE5:42
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.]) or (not x in ].a1,b1.] & x in [.a2,b2.]));

theorem :: MEASURE5:43
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.]) or (not x in ].a1,b1.] & x in [.a2,b2.]));

theorem :: MEASURE5:44
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.[) or (not x in [.a1,b1.[ & x in [.a2,b2.[));

theorem :: MEASURE5:45
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.[) or (not x in [.a1,b1.[ & x in [.a2,b2.[));

theorem :: MEASURE5:46
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.]) or (not x in [.a1,b1.[ & x in ].a2,b2.]));

theorem :: MEASURE5:47
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.]) or (not x in [.a1,b1.[ & x in ].a2,b2.]));

theorem :: MEASURE5:48
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.[) or (not x in ].a1,b1.] & x in [.a2,b2.[));

theorem :: MEASURE5:49
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.[) or (not x in ].a1,b1.] & x in [.a2,b2.[));

theorem :: MEASURE5:50
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]));

theorem :: MEASURE5:51
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]));

theorem :: MEASURE5:52
(a1 <' b1 &
((A = ].a1,b1.[ or A = [.a1,b1.] or A = [.a1,b1.[ or A = ].a1,b1.]) &
(A = ].a2,b2.[ or A = [.a2,b2.] or A = [.a2,b2.[ or A = ].a2,b2.])))
implies (a1 = a2 & b1 = b2);

definition let A be Interval;
func vol A -> R_eal means
:: MEASURE5:def 10
ex a,b being R_eal st
((A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]) &
(a <' b implies it = b - a) &
(b <=' a implies it = 0.));
end;

theorem :: MEASURE5:53
for A being open_interval Subset of REAL holds
for a,b being R_eal holds
A = ].a,b.[ implies
((a <' b implies vol(A) = b - a) &
(b <=' a implies vol(A) = 0.));

theorem :: MEASURE5:54
for A being closed_interval Subset of REAL holds
for a,b being R_eal holds
A = [.a,b.] implies
((a <' b implies vol(A) = b - a) &
(b <=' a implies vol(A) = 0.));

theorem :: MEASURE5:55
for A being right_open_interval Subset of REAL holds
for a,b being R_eal holds
A = [.a,b.[ implies
((a <' b implies vol(A) = b - a) &
(b <=' a implies vol(A) = 0.));

theorem :: MEASURE5:56
for A being left_open_interval Subset of REAL holds
for a,b being R_eal holds
A = ].a,b.] implies
((a <' b implies vol(A) = b - a) &
(b <=' a implies vol(A) = 0.));

theorem :: MEASURE5:57
for a,b,c being R_eal holds
(a = -infty & b in REAL & c = +infty &
(A = ].a,b.[ or A = ].b,c.[ or A = [.a,b.] or A = [.b,c.] or
A = [.a,b.[ or A = [.b,c.[ or A = ].a,b.] or A = ].b,c.]))
implies vol(A) = +infty;

theorem :: MEASURE5:58
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 vol(A) = +infty;

definition
cluster empty Interval;
end;

definition
redefine func {} -> empty Interval;
end;

canceled;

theorem :: MEASURE5:60
vol {} = 0.;

theorem :: MEASURE5:61
(A c= B & B =[.a,b.] & b <=' a) implies
(vol(A) = 0. & vol(B) = 0.);

theorem :: MEASURE5:62
A c= B implies vol A <=' vol B;

theorem :: MEASURE5:63
0. <=' vol(A);

```