:: Dyadic Numbers and $T_4$ Topological Spaces
:: by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 29, 1995
:: Copyright (c) 1995-2016 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);