Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

### Some Properties of Dyadic Numbers and Intervals

by
Jozef Bialas, and
Yatsuka Nakamura

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

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

theorem :: URYSOHN2:32
for a,b being R_eal st a = 0 & b = 1 holds

theorem :: URYSOHN2:33
for n,k being Nat st n <= k holds

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;

```