:: Some Properties of Dyadic Numbers and Intervals
:: by J\'ozef Bia{\l}as and Yatsuka Nakamura
::
:: Received February 16, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


begin

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

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

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

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

theorem Th5: :: URYSOHN2:5
for a, b being R_eal holds
( not a <= b or ( a = -infty &amp; b = -infty ) or ( a = -infty &amp; b in REAL ) or ( a = -infty &amp; b = +infty ) or ( a in REAL &amp; b in REAL ) or ( a in REAL &amp; b = +infty ) or ( a = +infty &amp; b = +infty ) )
proofend;

theorem Th6: :: URYSOHN2:6
for A being Interval holds 0 ** A is interval
proofend;

theorem Th7: :: URYSOHN2:7
for A being non empty Interval
for x being Real st x <> 0 &amp; A is open_interval holds
x ** A is open_interval
proofend;

theorem Th8: :: URYSOHN2:8
for A being non empty Interval
for x being Real st x <> 0 &amp; A is closed_interval holds
x ** A is closed_interval
proofend;

theorem Th9: :: URYSOHN2:9
for A being non empty Interval
for x being Real st 0 < x &amp; A is right_open_interval holds
x ** A is right_open_interval
proofend;

theorem Th10: :: URYSOHN2:10
for A being non empty Interval
for x being Real st x < 0 &amp; A is right_open_interval holds
x ** A is left_open_interval
proofend;

theorem Th11: :: URYSOHN2:11
for A being non empty Interval
for x being Real st 0 < x &amp; A is left_open_interval holds
x ** A is left_open_interval
proofend;

theorem Th12: :: URYSOHN2:12
for A being non empty Interval
for x being Real st x < 0 &amp; A is left_open_interval holds
x ** A is right_open_interval
proofend;

theorem :: URYSOHN2:13
for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A &amp; A = [.(inf A),(sup A).] holds
( B = [.(inf B),(sup B).] &amp; ( for s, t being Real st s = inf A &amp; t = sup A holds
( inf B = x * s &amp; sup B = x * t ) ) )
proofend;

theorem :: URYSOHN2:14
for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A &amp; A = ].(inf A),(sup A).] holds
( B = ].(inf B),(sup B).] &amp; ( for s, t being Real st s = inf A &amp; t = sup A holds
( inf B = x * s &amp; sup B = x * t ) ) )
proofend;

theorem :: URYSOHN2:15
for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A &amp; A = ].(inf A),(sup A).[ holds
( B = ].(inf B),(sup B).[ &amp; ( for s, t being Real st s = inf A &amp; t = sup A holds
( inf B = x * s &amp; sup B = x * t ) ) )
proofend;

theorem :: URYSOHN2:16
for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A &amp; A = [.(inf A),(sup A).[ holds
( B = [.(inf B),(sup B).[ &amp; ( for s, t being Real st s = inf A &amp; t = sup A holds
( inf B = x * s &amp; sup B = x * t ) ) )
proofend;

theorem Th17: :: URYSOHN2:17
for A being non empty Interval
for x being Real holds x ** A is Interval
proofend;

registration
let A be interval Subset of REAL;
let x be Real;
clusterx ** A ->  interval ;
correctness
coherence
x ** A is interval ;
proofend;
end;

Lm1:  for A being non empty Subset of REAL
for x being Real st x > 0 &amp; x ** A is bounded_above holds
A is bounded_above
proofend;

theorem Th18: :: URYSOHN2:18
for A being non empty Subset of REAL
for x being Real
for y being R_eal st x = y &amp; 0 <= y holds
sup (x ** A) = y * (sup A)
proofend;

Lm2:  for A being non empty Subset of REAL
for x being Real st x > 0 &amp; x ** A is bounded_below holds
A is bounded_below
proofend;

theorem Th19: :: URYSOHN2:19
for A being non empty Subset of REAL
for x being Real
for y being R_eal st x = y &amp; 0 <= y holds
inf (x ** A) = y * (inf A)
proofend;

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

theorem Th21: :: URYSOHN2:21
for eps being Real st 0 < eps holds
ex n being Element of NAT st 1 < (2 |^ n) * eps
proofend;

theorem Th22: :: URYSOHN2:22
for a, b being Real st 0 <= a &amp; 1 < b - a holds
ex n being Element of NAT st
( a < n &amp; n < b )
proofend;

theorem :: URYSOHN2:23
for n being Element of NAT holds dyadic n c= DYADIC
proofend;

theorem Th24: :: URYSOHN2:24
for a, b being Real st a < b &amp; 0 <= a &amp; b <= 1 holds
ex c being Real st
( c in DYADIC &amp; a < c &amp; c < b )
proofend;

theorem Th25: :: URYSOHN2:25
for a, b being Real st a < b holds
ex c being Real st
( c in DOM &amp; a < c &amp; c < b )
proofend;

theorem :: URYSOHN2:26
for A being non empty Subset of ExtREAL
for a, b being R_eal st A c= [.a,b.] holds
( a <= inf A &amp; sup A <= b )
proofend;

theorem :: URYSOHN2:27
( 0 in DYADIC &amp; 1 in DYADIC )
proofend;

theorem :: URYSOHN2:28
DYADIC c= [.0,1.]
proofend;

theorem :: URYSOHN2:29
for n, k being Element of NAT st n <= k holds
dyadic n c= dyadic k
proofend;

theorem Th30: :: URYSOHN2:30
for a, b, c, d being Real st a < c &amp; c < b &amp; a < d &amp; d < b holds
abs (d - c) < b - a
proofend;

theorem :: URYSOHN2:31
for eps being Real st 0 < eps holds
for d being Real st 0 < d holds
ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) &amp; r2 in DYADIC \/ (right_open_halfline 1) &amp; 0 < r1 &amp; r1 < d &amp; d < r2 &amp; r2 - r1 < eps )
proofend;

begin

:: missing, 2008.06.10, A.T.
theorem :: URYSOHN2:32
for A being non empty Subset of REAL
for x being Real st x > 0 &amp; x ** A is bounded_above holds
A is bounded_above by Lm1;

theorem :: URYSOHN2:33
for A being non empty Subset of REAL
for x being Real st x > 0 &amp; x ** A is bounded_below holds
A is bounded_below by Lm2;