The abstract of the Mizar article:

Some Properties of the Intervals

by

Jozef Bialas

Received February 5, 1994

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);