The abstract of the Mizar article:

Some Properties of Dyadic Numbers and Intervals

by

Jozef Bialas, and

Yatsuka Nakamura

Received February 16, 2001

MML identifier: URYSOHN2

[ Mizar article, MML identifier index ]

environ

 vocabulary MEASURE5, BOOLE, MEASURE6, SUPINF_1, ARYTM_1, RLVECT_1, ARYTM_3,
      RCOMP_1, RELAT_1, GROUP_1, INT_1, URYSOHN1, PRALG_2, ORDINAL2, ABSVALUE,
      ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, REAL_1,
      NUMBERS, NEWTON, INT_1, NAT_1, SUPINF_1, SUPINF_2, MEASURE5, MEASURE6,
      URYSOHN1, ABSVALUE, INTEGRA2;
 constructors RAT_1, SUPINF_2, MEASURE6, URYSOHN1, REAL_1, NAT_1, INTEGRA2,
      MEMBERED;
 clusters SUBSET_1, INT_1, SUPINF_1, XREAL_0, MEMBERED, ORDINAL2, NUMBERS;
 requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;


begin

::                    Properties of the Intervals

theorem :: URYSOHN2:1
   for A being Interval st A <> {} holds
   (^^A <' A^^ implies vol(A) = A^^ - ^^A) &
   (A^^ = ^^A implies vol(A) = 0.);

theorem :: URYSOHN2:2
     for A being Subset of REAL holds
   for x being Real st x <> 0 holds
   x" * (x * A) = A;

theorem :: URYSOHN2:3
   for x being Real st x <> 0 holds
   for A being Subset of REAL holds
   A = REAL implies x * A = A;

theorem :: URYSOHN2:4
   for A being Subset of REAL st A <> {} holds 0 * A = {0};

theorem :: URYSOHN2:5
   for x being Real holds
   x * {} = {};

theorem :: URYSOHN2:6
   for a,b being R_eal st a <=' b holds
   (a = -infty & b = -infty) or (a = -infty & b in REAL) or
   (a = -infty & b = +infty) or (a in REAL & b in REAL) or
   (a in REAL & b = +infty) or (a = +infty & b = +infty);

theorem :: URYSOHN2:7
   for x being R_eal holds
   [.x,x.] is Interval;

theorem :: URYSOHN2:8
   for A being Interval holds
   0 * A is Interval;

theorem :: URYSOHN2:9
   for A being Interval holds
   for x being Real st x<>0 holds
   A is open_interval implies x * A is open_interval;

theorem :: URYSOHN2:10
   for A being Interval holds
   for x being Real st x<>0 holds
   A is closed_interval implies x * A is closed_interval;

theorem :: URYSOHN2:11
   for A being Interval holds
   for x being Real st 0 < x holds
   A is right_open_interval implies x * A is right_open_interval;

theorem :: URYSOHN2:12
   for A being Interval holds
   for x being Real st x < 0 holds
   A is right_open_interval implies x * A is left_open_interval;

theorem :: URYSOHN2:13
   for A being Interval holds
   for x being Real st 0 < x holds
   A is left_open_interval implies x * A is left_open_interval;

theorem :: URYSOHN2:14
   for A being Interval holds
   for x being Real st x < 0 holds
   A is left_open_interval implies x * A is right_open_interval;

theorem :: URYSOHN2:15
   for A being Interval st A <> {} holds
   for x being Real st 0 < x holds
   for B being Interval st B = x * A holds
   A = [.^^A,A^^.] implies (B = [.^^B,B^^.] &
   for s,t being Real st s = ^^A & t = A^^ holds
   ^^B = x * s & B^^ = x * t);

theorem :: URYSOHN2:16
   for A being Interval st A <> {} holds
   for x being Real st 0 < x holds
   for B being Interval st B = x * A holds
   A = ].^^A,A^^.] implies (B = ].^^B,B^^.] &
   for s,t being Real st s = ^^A & t = A^^ holds
   ^^B = x * s & B^^ = x * t);

theorem :: URYSOHN2:17
   for A being Interval st A <> {} holds
   for x being Real st 0 < x holds
   for B being Interval st B = x * A holds
   A = ].^^A,A^^.[ implies (B = ].^^B,B^^.[ &
   for s,t being Real st s = ^^A & t = A^^ holds
   ^^B = x * s & B^^ = x * t);

theorem :: URYSOHN2:18
   for A being Interval st A <> {} holds
   for x being Real st 0 < x holds
   for B being Interval st B = x * A holds
   A = [.^^A,A^^.[ implies (B = [.^^B,B^^.[ &
   for s,t being Real st s = ^^A & t = A^^ holds
   ^^B = x * s & B^^ = x * t);

theorem :: URYSOHN2:19
   for A being Interval holds
   for x being Real holds
   x * A is Interval;

definition
   let A be Interval;
   let x be Real;
cluster x * A -> interval;
end;

theorem :: URYSOHN2:20
     for A being Interval
   for x being Real st 0 <= x
   for y being Real st y = vol(A) holds
   x * y = vol(x * A);

canceled 2;

theorem :: URYSOHN2:23
   for eps being Real st 0 < eps holds
   ex n being Nat st 1 < 2|^n * eps;

theorem :: URYSOHN2:24
   for a,b being Real st 0 <= a & 1 < b - a holds
   ex n being Nat st a < n & n < b;

canceled 2;

theorem :: URYSOHN2:27
     for n being Nat holds dyadic(n) c= DYADIC;

theorem :: URYSOHN2:28
   for a,b being Real st a < b & 0 <= a & b <= 1 holds
   ex c being Real st c in DYADIC & a < c & c < b;

theorem :: URYSOHN2:29
   for a,b being Real st a < b
   ex c being Real st c in DOM & a < c & c < b;

theorem :: URYSOHN2:30
     for A being non empty Subset of ExtREAL holds
   for a,b being R_eal st A c= [.a,b.] holds
   a <=' inf A & sup A <=' b;

theorem :: URYSOHN2:31
     0 in DYADIC & 1 in DYADIC;

theorem :: URYSOHN2:32
     for a,b being R_eal st a = 0 & b = 1 holds
   DYADIC c= [.a,b.];

theorem :: URYSOHN2:33
     for n,k being Nat st n <= k holds
   dyadic(n) c= dyadic(k);

theorem :: URYSOHN2:34  :: JGRAPH_1:31
   for a,b,c,d being Real st a < c & c < b & a < d & d < b holds
   abs(d - c) < b - a;

theorem :: URYSOHN2:35
     for eps being Real st 0 < eps holds
   for d being Real st 0 < d & d <= 1 holds
   ex r1,r2 being Real st r1 in DYADIC \/ R>1 & r2 in DYADIC \/ R>1 &
   0 < r1 & r1 < d & d < r2 & r2 - r1 < eps;