Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

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

Back to top