Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Some Properties of the Intervals

by
Jozef Bialas

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

```environ

vocabulary FUNCT_1, RELAT_1, SUPINF_1, SUPINF_2, RLVECT_1, ARYTM_3, ORDINAL2,
ARYTM_1, FINSEQ_1, MEASURE5, RCOMP_1, BOOLE, MEASURE6, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, REAL_1, NAT_1, SUPINF_1, SUPINF_2,
MEASURE5;
constructors DOMAIN_1, NAT_1, REAL_1, SUPINF_2, MEASURE5, WELLORD2, MEMBERED,
XBOOLE_0;
clusters SUBSET_1, SUPINF_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1,
XBOOLE_0, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;

begin

::
::                   Some theorems about R_eal numbers
::

theorem :: MEASURE6:1
ex F being Function of NAT,[:NAT,NAT:] st F is one-to-one &
dom F = NAT & rng F = [:NAT,NAT:];

theorem :: MEASURE6:2
for F being Function of NAT,ExtREAL holds
F is nonnegative implies 0. <=' SUM(F);

theorem :: MEASURE6:3
for F being Function of NAT,ExtREAL holds
for x being R_eal holds
((ex n being Nat st x <=' F.n) &
F is nonnegative) implies x <=' SUM(F);

canceled 4;

theorem :: MEASURE6:8
for x,y being R_eal holds
x is Real implies y - x + x = y & y + x - x = y;

canceled;

theorem :: MEASURE6:10
for x,y,z being R_eal holds
z in REAL & y <' x implies (z + x) - (z + y) = x - y;

theorem :: MEASURE6:11
for x,y,z being R_eal holds
z in REAL & x <=' y implies
z + x <=' z + y & x + z <=' y + z & x - z <=' y - z;

theorem :: MEASURE6:12
for x,y,z being R_eal holds
z in REAL & x <' y implies
z + x <' z + y & x + z <' y + z & x - z <' y - z;

definition
let x be real number;
func R_EAL x -> R_eal equals
:: MEASURE6:def 1
x;
end;

theorem :: MEASURE6:13
for x,y being real number holds
x <= y iff R_EAL x <=' R_EAL y;

theorem :: MEASURE6:14
for x,y being real number holds
x < y iff R_EAL x <' R_EAL y;

theorem :: MEASURE6:15
for x,y,z being R_eal holds
x <' y & y <' z implies y is Real;

theorem :: MEASURE6:16
for x,y,z being R_eal holds
x is Real & z is Real & x <=' y & y <=' z implies y is Real;

theorem :: MEASURE6:17
for x,y,z being R_eal st
(x is Real & x <=' y & y <' z) holds y is Real;

theorem :: MEASURE6:18
for x,y,z being R_eal st
(x <' y & y <=' z & z is Real) holds y is Real;

theorem :: MEASURE6:19
for x,y being R_eal st
0. <' x & x <' y holds 0. <' y - x;

theorem :: MEASURE6:20
for x,y,z being R_eal holds
(0. <=' x & 0. <=' z & z + x <' y) implies z <' y - x;

theorem :: MEASURE6:21
for x being R_eal holds x - 0. = x;

theorem :: MEASURE6:22
for x,y,z being R_eal holds
0. <=' x & 0. <=' z & z + x <' y implies z <=' y;

theorem :: MEASURE6:23
for x being R_eal holds
0. <' x implies ex y being R_eal st 0. <' y & y <' x;

theorem :: MEASURE6:24
for x,z being R_eal st
(0. <' x & x <' z) holds
ex y being R_eal st 0. <' y & x + y <' z & y in REAL;

theorem :: MEASURE6:25
for x,z being R_eal holds
0. <=' x & x <' z implies ex y being R_eal st
0. <' y & x + y <' z & y in REAL;

theorem :: MEASURE6:26
for x being R_eal st 0. <' x holds
ex y being R_eal st 0. <' y & y + y <' x;

definition
let x be R_eal;
assume 0. <' x;
func Seg(x) -> non empty Subset of ExtREAL means
:: MEASURE6:def 2
for y being R_eal holds y in it iff (0. <' y & y + y <' x);
end;

definition
let x be R_eal;
func len(x) -> R_eal equals
:: MEASURE6:def 3
sup Seg(x);
end;

theorem :: MEASURE6:27
for x being R_eal st
0. <' x holds 0. <' len(x);

theorem :: MEASURE6:28
for x being R_eal st
0. <' x holds len(x) <=' x;

theorem :: MEASURE6:29
for x being R_eal st
0. <' x & x <' +infty holds len(x) is Real;

theorem :: MEASURE6:30
for x being R_eal st
0. <' x holds len(x) + len(x) <=' x;

theorem :: MEASURE6:31
for eps being R_eal st 0. <' eps
ex F being Function of NAT,ExtREAL st
(for n being Nat holds 0. <' F.n) & SUM(F) <' eps;

theorem :: MEASURE6:32
for eps being R_eal holds
for X being non empty Subset of ExtREAL holds
0. <' eps & inf X is Real implies
ex x being R_eal st x in X & x <' inf X + eps;

theorem :: MEASURE6:33
for eps being R_eal holds
for X being non empty Subset of ExtREAL holds
0. <' eps & sup X is Real implies
ex x being R_eal st x in X & sup X - eps <' x;

theorem :: MEASURE6:34
for F being Function of NAT,ExtREAL holds
F is nonnegative & SUM(F) <' +infty implies
for n being Nat holds F.n in REAL;

::
::                      PROPERTIES OF THE INTERVALS
::

definition
redefine func -infty -> R_eal;

redefine func +infty -> R_eal;
end;

theorem :: MEASURE6:35
REAL is Interval &
REAL = ].-infty,+infty.[ & REAL = [.-infty,+infty.] &
REAL = [.-infty,+infty.[ & REAL = ].-infty,+infty.];

theorem :: MEASURE6:36
for a,b being R_eal holds b = -infty implies
].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {};

theorem :: MEASURE6:37
for a,b being R_eal holds
a = +infty implies
].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {};

theorem :: MEASURE6:38
for A being Interval,
a, b being R_eal,
c, d, e being Real st
A = ].a,b.[ & c in A & d in A & c <= e & e <= d holds e in A;

theorem :: MEASURE6:39
for A being Interval,
a, b being R_eal,
c, d, e being Real st
A = [.a,b.] & c in A & d in A & c <= e & e <= d holds e in A;

theorem :: MEASURE6:40
for A being Interval,
a, b being R_eal,
c, d, e being Real st
A = ].a,b.] & c in A & d in A & c <= e & e <= d holds e in A;

theorem :: MEASURE6:41
for A being Interval,
a, b being R_eal,
c, d, e being Real st
A = [.a,b.[ & c in A & d in A & c <= e & e <= d holds e in A;

theorem :: MEASURE6:42
for A being non empty Subset of ExtREAL holds
for m,M being R_eal st m = inf A & M = sup A holds
(((for c,d being Real st c in A & d in A holds
for e being Real st c <= e & e <= d holds
e in A) & not m in A & not M in A) implies A = ].m,M.[);

theorem :: MEASURE6:43
for A being non empty Subset of ExtREAL holds
for m,M being R_eal st m = inf A & M = sup A holds
(((for c,d being Real st c in A & d in A holds
for e being Real st c <= e & e <= d holds
e in A) & m in A & M in A & A c= REAL) implies A = [.m,M.]);

theorem :: MEASURE6:44
for A being non empty Subset of ExtREAL holds
for m,M being R_eal st m = inf A & M = sup A holds
(((for c,d being Real st c in A & d in A holds
for e being Real st c <= e & e <= d holds
e in A) & m in A & not M in A & A c= REAL) implies A = [.m,M.[);

theorem :: MEASURE6:45
for A being non empty Subset of ExtREAL holds
for m,M being R_eal st m = inf A & M = sup A holds
(((for c,d being Real st c in A & d in A holds
for e being Real st c <= e & e <= d holds
e in A) & not m in A & M in A & A c= REAL) implies A = ].m,M.]);

theorem :: MEASURE6:46
for A being Subset of REAL holds
A is Interval iff
for a,b being Real st a in A & b in A holds
for c being Real st a <= c & c <= b holds
c in A;

theorem :: MEASURE6:47
for A,B being Interval st A meets B holds A \/ B is Interval;

definition
let A be Interval;
assume  A <> {};
func ^^A -> R_eal means
:: MEASURE6:def 4
ex b being R_eal st it <=' b &
(A = ].it,b.[ or A = ].it,b.] or A = [.it,b.] or A = [.it,b.[);
end;

definition
let A be Interval;
assume  A <> {};
func A^^ -> R_eal means
:: MEASURE6:def 5
ex a being R_eal st a <=' it &
(A = ].a,it.[ or A = ].a,it.] or A = [.a,it.] or A = [.a,it.[);
end;

theorem :: MEASURE6:48
for A being Interval holds
A is open_interval & A <> {} implies ^^A <=' A^^ & A = ].^^A,A^^.[;

theorem :: MEASURE6:49
for A being Interval holds
A is closed_interval & A <> {} implies ^^A <=' A^^ & A = [.^^A,A^^.];

theorem :: MEASURE6:50
for A being Interval holds
A is right_open_interval & A <> {} implies ^^A <=' A^^ & A = [.^^A,A^^.[;

theorem :: MEASURE6:51
for A being Interval holds
A is left_open_interval & A <> {} implies ^^A <=' A^^ & A = ].^^A,A^^.];

theorem :: MEASURE6:52
for A being Interval holds
A <> {} implies ^^A <=' A^^ &
(A = ].^^A,A^^.[ or A = ].^^A,A^^.] or A = [.^^A,A^^.] or A = [.^^A,A^^.[);

canceled;

theorem :: MEASURE6:54
for A being Interval holds
for a being real number holds
a in A implies ^^A <=' R_EAL a & R_EAL a <=' A^^;

theorem :: MEASURE6:55
for A,B being Interval holds
for a,b being real number st a in A & b in B holds
A^^ <=' ^^B implies a <= b;

theorem :: MEASURE6:56
for A being Interval holds
for a being R_eal st a in A holds
^^A <=' a & a <=' A^^;

theorem :: MEASURE6:57
for A being Interval st A <> {} holds
for a being R_eal st ^^A <' a & a <' A^^ holds a in A;

theorem :: MEASURE6:58
for A,B being Interval holds
A^^ = ^^B & (A^^ in A or ^^B in B) implies A \/ B is Interval;

definition
let A be Subset of REAL;
let x be real number;
func x + A -> Subset of REAL means
:: MEASURE6:def 6
for y being Real holds
y in it iff ex z being Real st z in A & y = x + z;
end;

theorem :: MEASURE6:59
for A being Subset of REAL holds
for x being real number holds
-x + (x + A) = A;

theorem :: MEASURE6:60
for x being real number holds
for A being Subset of REAL holds
A = REAL implies x + A = A;

theorem :: MEASURE6:61
for x being real number holds x + {} = {};

theorem :: MEASURE6:62
for A being Interval holds
for x being real number holds
A is open_interval iff x + A is open_interval;

theorem :: MEASURE6:63
for A being Interval holds
for x being real number holds
A is closed_interval iff x + A is closed_interval;

theorem :: MEASURE6:64
for A being Interval holds
for x being real number holds
A is right_open_interval iff x + A is right_open_interval;

theorem :: MEASURE6:65
for A being Interval holds
for x being real number holds
A is left_open_interval iff x + A is left_open_interval;

theorem :: MEASURE6:66
for A being Interval holds
for x being real number holds
x + A is Interval;

definition
let A be Interval;
let x be real number;
cluster x + A -> interval;
end;

theorem :: MEASURE6:67
for A being Interval holds
for x being real number holds
vol(A) = vol(x + A);

```