The abstract of the Mizar article:

Properties of the Intervals of Real Numbers

by

Jozef Bialas

Received January 12, 1993

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