:: Some Properties of Dyadic Numbers and Intervals
::  by J\'ozef Bia{\l}as and Yatsuka Nakamura
::
:: Received February 16, 2001
:: Copyright (c) 2001-2021 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;