:: Some Properties of Dyadic Numbers and Intervals
:: by J\'ozef Bia{\l}as and Yatsuka Nakamura
::
:: Received February 16, 2001
:: Copyright (c) 2001-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, CARD_1, RELAT_1, MEMBER_1, TARSKI,
ARYTM_3, XBOOLE_0, SUPINF_1, XXREAL_0, MEASURE5, XXREAL_1, ORDINAL2,
XXREAL_2, MEMBERED, SEQ_4, ARYTM_1, NEWTON, INT_1, URYSOHN1, CARD_3,
PROB_1, LIMFUNC1, NAT_1, COMPLEX1, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NUMBERS, MEMBERED, MEMBER_1, NEWTON, INT_1, NAT_1,
XXREAL_1, XXREAL_2, SUPINF_1, MEASURE5, PROB_1, URYSOHN1, INTEGRA2,
LIMFUNC1, SEQ_4, SUPINF_2, EXTREAL1;
constructors DOMAIN_1, REAL_1, NAT_1, PROB_1, LIMFUNC1, NEWTON, SUPINF_2,
URYSOHN1, INTEGRA2, SUPINF_1, EXTREAL1, SEQ_4, PSCOMP_1, MEASURE5,
BINOP_2;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, XXREAL_1, SEQ_4, XXREAL_2, XXREAL_3, MEASURE5, MEMBER_1,
NEWTON, ORDINAL1;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
begin :: Properties of the Intervals
theorem :: URYSOHN2:1
for A being Subset of REAL, x being Real st x <> 0 holds
x" ** (x ** A) = A;
theorem :: URYSOHN2:2
for x being Real st x <> 0 holds for A being Subset of REAL holds
A = REAL implies x ** A = A;
theorem :: URYSOHN2:3
for A being Subset of REAL st A <> {} holds 0 ** A = {0};
theorem :: URYSOHN2:4
for x being Real holds x ** {} = {};
theorem :: URYSOHN2:5
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:6
for A being Interval holds 0 ** A is interval;
theorem :: URYSOHN2:7
for A being non empty Interval, x being Real st x<>0 holds A is
open_interval implies x ** A is open_interval;
theorem :: URYSOHN2:8
for A being non empty Interval, x being Real st x<>0 holds A is
closed_interval implies x ** A is closed_interval;
theorem :: URYSOHN2:9
for A being non empty Interval, x being Real st 0 < x holds A is
right_open_interval implies x ** A is right_open_interval;
theorem :: URYSOHN2:10
for A being non empty Interval, x being Real st x < 0 holds A is
right_open_interval implies x ** A is left_open_interval;
theorem :: URYSOHN2:11
for A being non empty Interval, x being Real st 0 < x holds A is
left_open_interval implies x ** A is left_open_interval;
theorem :: URYSOHN2:12
for A being non empty Interval, x being Real st x < 0 holds A is
left_open_interval implies x ** A is right_open_interval;
theorem :: URYSOHN2:13
for A being non empty Interval, x being Real st 0 < x for B
being non empty Interval st B = x ** A holds A = [.inf A,sup A.] implies (B =
[.inf B,sup B.] & for s,t being Real st s = inf A & t = sup A holds inf B = x *
s & sup B = x * t);
theorem :: URYSOHN2:14
for A being non empty Interval, x being Real st 0 < x for B
being non empty Interval st B = x ** A holds A = ].inf A,sup A.] implies (B =
].inf B,sup B.] & for s,t being Real st s = inf A & t = sup A holds inf B = x *
s & sup B = x * t);
theorem :: URYSOHN2:15
for A being non empty Interval, x being Real st 0 < x for B
being non empty Interval st B = x ** A holds A = ].inf A,sup A.[ implies (B =
].inf B,sup B.[ & for s,t being Real st s = inf A & t = sup A holds inf B = x *
s & sup B = x * t);
theorem :: URYSOHN2:16
for A being non empty Interval, x being Real st 0 < x for B
being non empty Interval st B = x ** A holds A = [.inf A,sup A.[ implies (B =
[.inf B,sup B.[ & for s,t being Real st s = inf A & t = sup A holds inf B = x *
s & sup B = x * t);
theorem :: URYSOHN2:17
for A being non empty Interval, x being Real holds x ** A is
Interval;
registration
let A be interval Subset of REAL;
let x be Real;
cluster x ** A -> interval;
end;
theorem :: URYSOHN2:18
for A being non empty Subset of REAL, x being Real, y being
R_eal st x = y & 0 <= y holds sup(x ** A) = y * sup A;
theorem :: URYSOHN2:19
for A being non empty Subset of REAL, x being Real, y being
R_eal st x = y & 0 <= y holds inf(x ** A) = y * inf A;
theorem :: URYSOHN2:20
for A being Interval, x,y being Real st 0 <= x & y
= diameter(A) holds x * y = diameter(x ** A);
theorem :: URYSOHN2:21
for eps being Real st 0 < eps
ex n being Nat st 1 < 2|^n * eps;
theorem :: URYSOHN2:22
for a,b being Real st 0 <= a & 1 < b - a
ex n being Nat st a < n & n < b;
theorem :: URYSOHN2:23
for n being Nat holds dyadic(n) c= DYADIC;
theorem :: URYSOHN2:24
for a,b being Real st a < b & 0 <= a & b <= 1
ex c being Real st c in DYADIC & a < c & c < b;
theorem :: URYSOHN2:25
for a,b being Real st a < b
ex c being Real st c in DOM & a < c & c < b;
theorem :: URYSOHN2:26
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:27
0 in DYADIC & 1 in DYADIC;
theorem :: URYSOHN2:28
DYADIC c= [. 0,1 .];
theorem :: URYSOHN2:29
for n,k being Nat st n <= k holds dyadic(n) c= dyadic(k);
theorem :: URYSOHN2:30 :: JGRAPH_1:31
for a,b,c,d being Real st a < c & c < b & a < d & d < b holds
|.d - c qua Complex.| < b - a;
theorem :: URYSOHN2:31
for eps being Real st 0 < eps
for d being Real st 0 < d
ex r1,r2 being Real
st r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (
right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps;
begin :: Addenda
:: missing, 2008.06.10, A.T.
theorem :: URYSOHN2:32
for A being non empty Subset of REAL, x being Real
st x > 0 & x**A is
bounded_above holds A is bounded_above;
theorem :: URYSOHN2:33
for A being non empty Subset of REAL, x being Real
st x > 0 & x**A is
bounded_below holds A is bounded_below;