:: Dyadic Numbers and $T_4$ Topological Spaces
::  by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 29, 1995
:: Copyright (c) 1995-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, NAT_1, SUBSET_1, REAL_1, CARD_1, XXREAL_0, NEWTON,
      ARYTM_3, CARD_3, PROB_1, XBOOLE_0, LIMFUNC1, PRE_TOPC, FUNCT_1, ZFMISC_1,
      STRUCT_0, FINSEQ_1, RELAT_1, ARYTM_1, TARSKI, CONNSP_2, RCOMP_1, TOPS_1,
      SETFAM_1, CARD_5, URYSOHN1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, DOMAIN_1,
      FUNCT_1, ENUMSET1, FUNCT_2, XCMPLX_0, XREAL_0, REAL_1, FINSEQ_1, NAT_1,
      PROB_1, LIMFUNC1, NEWTON, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_2, XXREAL_0;
 constructors SETFAM_1, DOMAIN_1, REAL_1, NAT_1, MEMBERED, XXREAL_1, PROB_1,
      LIMFUNC1, NEWTON, TOPS_1, COMPTS_1, CONNSP_2;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
      STRUCT_0, PRE_TOPC, TOPS_1, NEWTON, NAT_1, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

definition
  let n be Nat;
  func dyadic(n) -> Subset of REAL means
:: URYSOHN1:def 1

  for x being Real holds x in it
  iff ex i being Nat st i <= 2|^n & x = i/(2|^n);
end;


definition
  func DYADIC -> Subset of REAL means
:: URYSOHN1:def 2

  for a being Real holds a in it
  iff ex n being Nat st a in dyadic(n);
end;

definition
  func DOM -> Subset of REAL equals
:: URYSOHN1:def 3
  (halfline 0) \/ DYADIC \/ right_open_halfline 1;
end;

theorem :: URYSOHN1:1
  for n being Nat holds for x being Real st
  x in dyadic(n) holds 0 <= x & x <= 1;

theorem :: URYSOHN1:2
  dyadic(0) = {0,1};

theorem :: URYSOHN1:3
  dyadic(1) = {0,1/2,1};

registration
  let n be Nat;
  cluster dyadic(n) -> non empty;
end;

definition
  let n be Nat;
  func dyad(n) -> FinSequence means
:: URYSOHN1:def 4

  dom it = Seg((2|^n)+1) &
  for i being Nat st i in dom it holds it.i = (i-1)/(2|^n);
end;

theorem :: URYSOHN1:4
  for n being Nat holds
  dom dyad(n) = Seg((2|^n)+1) & rng dyad(n) = dyadic(n);

registration
  cluster DYADIC -> non empty;
end;

registration
  cluster DOM -> non empty;
end;

theorem :: URYSOHN1:5
  for n being Nat holds dyadic(n) c= dyadic(n+1);

theorem :: URYSOHN1:6
  for n being Nat holds 0 in dyadic(n) & 1 in dyadic(n);

theorem :: URYSOHN1:7
  for n,i being Nat st 0 < i & i <= 2|^n holds (i*2-1)/
  (2|^(n+1)) in dyadic(n+1) \ dyadic(n);

theorem :: URYSOHN1:8
  for n,i being Nat st 0 <= i & i < 2|^n holds (i*2+1)/
  (2|^(n+1)) in dyadic(n+1) \ dyadic(n);

theorem :: URYSOHN1:9
  for n being Nat holds 1/(2|^(n+1)) in dyadic(n+1) \ dyadic(n);

definition
  let n be Nat;
  let x be Element of dyadic(n);
  func axis(x) -> Nat means
:: URYSOHN1:def 5

  x = it/(2|^n);
end;

theorem :: URYSOHN1:10
  for n being Nat holds for x being Element of dyadic(n) holds
  x = axis(x)/(2|^n) & axis(x) <= (2|^n);

theorem :: URYSOHN1:11
  for n being Nat holds for x being Element of dyadic(n)
  holds (axis(x)-1)/(2|^n) < x & x < (axis(x)+1)/(2|^n);

theorem :: URYSOHN1:12
  for n being Nat holds for x being Element of dyadic(n) holds
  (axis(x)-1)/(2|^n) < (axis(x)+1)/(2|^n);

theorem :: URYSOHN1:13
  for n being Nat holds for x being Element of dyadic(n
+1) holds (not x in dyadic(n) implies (axis(x)-1)/(2|^(n+1)) in dyadic(n) &
  (axis(x)+1)/(2|^(n+1)) in dyadic(n) );

theorem :: URYSOHN1:14
  for n being Nat holds for x1,x2 being Element of dyadic(n) st
  x1 < x2 holds axis(x1) < axis(x2);

theorem :: URYSOHN1:15
  for n being Nat holds for x1,x2 being Element of
dyadic(n) st x1 < x2 holds x1 <= (axis(x2)-1)/(2|^n) & (axis(x1)+1)/(2|^n)
  <= x2;

theorem :: URYSOHN1:16
  for n being Nat holds for x1,x2 being Element of
dyadic(n+1) st x1 < x2 & not x1 in dyadic(n) & not x2 in dyadic(n) holds
(axis(x1)+1)/(2|^(n+1)) <= (axis(x2)-1)/(2|^(n+1));

begin

::
::                             Normal TopSpaces
::

notation
  let T be non empty TopSpace;
  let x be Point of T;
  synonym Nbhd of x,T for a_neighborhood of x;
end;

definition
  let T be non empty TopSpace;
  let x be Point of T;
  redefine mode Nbhd of x,T means
:: URYSOHN1:def 6
  ex A being Subset of T st A is open & x in A & A c= it;
end;

theorem :: URYSOHN1:17
  for T being non empty TopSpace for A being Subset of T holds
  A is open iff
  for x being Point of T holds x in A implies ex B being Nbhd of x,T st B c= A;

theorem :: URYSOHN1:18
  for T being non empty TopSpace holds for A being Subset of T holds (
  for x being Point of T st x in A holds A is Nbhd of x,T) implies A is open;

definition
  let T be TopSpace;
  redefine attr T is T_1 means
:: URYSOHN1:def 7
  for p,q being Point of T st not p = q
  ex W,V being Subset of T st W is open & V is open &
  p in W & not q in W & q in V & not p in V;
end;

theorem :: URYSOHN1:19
  for T being non empty TopSpace holds T is T_1 iff for p being
  Point of T holds {p} is closed;

theorem :: URYSOHN1:20
  for T being non empty TopSpace st T is normal holds for A,B
being open Subset of T st A <> {} & Cl(A) c=B holds ex C being Subset of T st C
  <> {} & C is open & Cl(A) c= C & Cl(C) c= B;

theorem :: URYSOHN1:21
  for T being non empty TopSpace holds T is regular iff for A being open
Subset of T for p being Point of T st p in A holds ex B being open Subset of T
  st p in B & Cl(B) c= A;

theorem :: URYSOHN1:22
  for T being non empty TopSpace st T is normal & T is T_1 holds for A
being open Subset of T st A <> {} holds ex B being Subset of T st B <> {} & Cl(
  B) c= A;

theorem :: URYSOHN1:23
  for T being non empty TopSpace st T is normal for A,B being Subset of
T st A is open & B is closed & B <> {} & B c= A ex C being Subset of T st C is
  open & B c= C & Cl(C) c= A;

begin

::
::              Some increasing family of sets in normal space
::

definition
  let T be non empty TopSpace;
  let A,B be Subset of T;
  assume
 T is normal & A <> {} & A is open & B is open & Cl(A) c= B;
  mode Between of A,B -> Subset of T means
:: URYSOHN1:def 8

    it <> {} & it is open & Cl( A) c= it & Cl(it) c= B;
end;

theorem :: URYSOHN1:24
  for T being non empty TopSpace st T is normal for A,B being closed
  Subset of T st A <> {} for n being Nat for G being Function of
  dyadic(n),bool the carrier of T st A c= G.0 & B = [#](T) \ G.1 & for r1,r2
being Element of dyadic(n) st r1 < r2 holds G.r1 is open & G.r2 is open & Cl(G.
r1) c= G.r2 ex F being Function of dyadic(n+1),bool the carrier of T st A c= F.
  0 & B = [#](T) \ F.1 & for r1,r2,r being Element of dyadic(n+1) st r1 < r2
holds F.r1 is open & F.r2 is open & Cl(F.r1) c= F.r2 & (r in dyadic(n) implies
  F.r = G.r);