:: Dyadic Numbers and $T_4$ Topological Spaces
:: by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 29, 1995
:: Copyright (c) 1995-2026 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;
definitions TARSKI, CONNSP_2, XBOOLE_0, PRE_TOPC;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0, PRE_TOPC;
theorems TARSKI, SUBSET_1, FUNCT_1, NAT_1, FINSEQ_1, ZFMISC_1, PRE_TOPC,
TOPS_1, ENUMSET1, COMPTS_1, NEWTON, CONNSP_2, XBOOLE_0, XBOOLE_1,
SCHEME1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, XREAL_0;
schemes SUBSET_1, NAT_1, FINSEQ_1, FUNCT_2;
begin
definition
let n be Nat;
func dyadic(n) -> Subset of REAL means
:Def1:
for x being Real holds x in it
iff ex i being Nat st i <= 2|^n & x = i/(2|^n);
existence
proof
defpred P[set] means ex i being Nat st (i <= (2|^n) &
$1 = i/(2|^n));
consider X being Subset of REAL such that
A1: for x being Element of REAL holds x in X iff P[x] from SUBSET_1:sch 3;
take X;
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
x in X iff P[x] by A1;
hence thesis;
end;
uniqueness
proof
let A1,A2 be Subset of REAL;
assume that
A2: for x being Real holds x in A1 iff
ex i being Nat st i <= 2|^n &
x = i/(2|^n) and
A3: for x being Real holds x in A2 iff
ex i being Nat st i <= 2|^n &
x = i/(2|^n);
for a being object holds a in A1 iff a in A2
proof
let a be object;
thus a in A1 implies a in A2
proof
assume
A4: a in A1;
then reconsider a as Real;
ex i being Nat st i <= 2|^n & a = i/(2|^n)
by A2,A4;
hence thesis by A3;
end;
assume
A5: a in A2;
then reconsider a as Real;
ex i being Nat st i <= 2|^n & a = i/(2|^n) by A3,A5;
hence thesis by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func DYADIC -> Subset of REAL means
:Def2:
for a being Real holds a in it
iff ex n being Nat st a in dyadic(n);
existence
proof
defpred P[set] means ex i being Nat st $1 in dyadic(i);
consider X being Subset of REAL such that
A1: for x being Element of REAL holds x in X iff P[x]
from SUBSET_1:sch 3;
take X;
let a be Real;
reconsider a as Element of REAL by XREAL_0:def 1;
a in X iff P[a] by A1;
hence thesis;
end;
uniqueness
proof
let A1,A2 be Subset of REAL;
assume that
A2: for x being Real holds x in A1 iff ex n being Nat st x
in dyadic(n) and
A3: for x being Real holds x in A2 iff ex n being Nat st x
in dyadic(n);
for a being object holds a in A1 iff a in A2
proof
let a be object;
thus a in A1 implies a in A2
proof
assume
A4: a in A1;
then reconsider a as Real;
ex n being Nat st a in dyadic(n) by A2,A4;
hence thesis by A3;
end;
thus a in A2 implies a in A1
proof
assume
A5: a in A2;
then reconsider a as Real;
ex n being Nat st a in dyadic(n) by A3,A5;
hence thesis by A2;
end;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func DOM -> Subset of REAL equals
(halfline 0) \/ DYADIC \/ right_open_halfline 1;
coherence;
end;
theorem Th1:
for n being Nat holds for x being Real st
x in dyadic(n) holds 0 <= x & x <= 1
proof
let n be Nat;
let x be Real;
assume x in dyadic(n);
then consider i being Nat such that
A1: i <= 2|^n and
A2: x = i/(2|^n) by Def1;
0/(2|^n) <= i/(2|^n) & i/(2|^n) <= (2|^n)/(2|^n) by A1,XREAL_1:72;
hence thesis by A2,XCMPLX_1:60;
end;
theorem Th2:
dyadic(0) = {0,1}
proof
A1: 2|^0 = 1 by NEWTON:4;
A2: for x being Real
holds x in dyadic(0) iff ex i being Nat st
i <= 1 & x = i
proof
let x be Real;
A3: (ex i being Nat st i <= 1 & x = i) implies x in
dyadic(0)
proof
given i being Nat such that
A4: i <= 1 and
A5: x = i;
x = i/1 by A5;
hence thesis by A1,A4,Def1;
end;
x in dyadic(0) implies ex i being Nat st i <= 1 & x = i
proof
assume x in dyadic(0);
then ex i being Nat st i <= 1 & x = i/1 by A1,Def1;
hence thesis;
end;
hence thesis by A3;
end;
for x being object holds x in dyadic(0) iff x in {0,1}
proof
let x be object;
A6: x in dyadic(0) implies x in {0,1}
proof
assume
A7: x in dyadic(0);
then reconsider x as Real;
consider i being Nat such that
A8: i <= 1 and
A9: x = i by A2,A7;
i <= 0+1 by A8;
then x = 0 or x = 1 by A9,NAT_1:9;
hence thesis by TARSKI:def 2;
end;
x in {0,1} implies x in dyadic(0)
proof
assume x in {0,1};
then x = 0 or x = 1 by TARSKI:def 2;
hence thesis by A2;
end;
hence thesis by A6;
end;
hence thesis by TARSKI:2;
end;
theorem
dyadic(1) = {0,1/2,1}
proof
A1: 2|^1 = 2;
for x being object holds x in dyadic(1) iff x in {0,1/2,1}
proof
let x be object;
A2: x in {0,1/2,1} implies x in dyadic(1)
proof
assume
A3: x in {0,1/2,1};
per cases by A3,ENUMSET1:def 1;
suppose
x = 0;
then x = 0/2;
hence thesis by A1,Def1;
end;
suppose
x = 1/2;
hence thesis by A1,Def1;
end;
suppose
A4: x = 1;
then reconsider x as Real;
x = 2/2 by A4;
hence thesis by A1,Def1;
end;
end;
x in dyadic(1) implies x in {0,1/2,1}
proof
assume
A5: x in dyadic(1);
then reconsider x as Real;
consider i being Nat such that
A6: i <= 2 and
A7: x = i/2 by A1,A5,Def1;
i = 0 or ... or i = 2 by A6;
hence thesis by A7,ENUMSET1:def 1;
end;
hence thesis by A2;
end;
hence thesis by TARSKI:2;
end;
registration
let n be Nat;
cluster dyadic(n) -> non empty;
coherence
proof
ex i being Nat st 0 <= i & i <= (2|^n) & 0/(2|^n) = i/(2|^n);
hence thesis by Def1;
end;
end;
definition
let n be Nat;
func dyad(n) -> FinSequence means
:Def4:
dom it = Seg((2|^n)+1) &
for i being Nat st i in dom it holds it.i = (i-1)/(2|^n);
existence
proof
deffunc F(Nat)=($1-1)/(2|^n);
consider FS being FinSequence such that
A1: len FS = (2|^n)+1 & for i being Nat st i in dom FS holds FS.i = F(i)
from FINSEQ_1:sch 2;
take FS;
thus thesis by A1,FINSEQ_1:def 3;
end;
uniqueness
proof
let F1,F2 be FinSequence;
assume that
A2: dom F1 = Seg((2|^n)+1) and
A3: for i being Nat st i in dom F1 holds F1.i = (i-1)/(2|^n ) and
A4: dom F2 = Seg((2|^n)+1) and
A5: for i being Nat st i in dom F2 holds F2.i = (i-1)/(2|^n );
consider X being set such that
A6: X = dom F1;
for k being Nat st k in X holds F1.k = F2.k
proof
let k be Nat;
assume
A7: k in X;
hence F1.k = (k-1)/(2|^n) by A3,A6
.= F2.k by A2,A4,A5,A6,A7;
end;
hence thesis by A2,A4,A6,FINSEQ_1:13;
end;
end;
theorem
for n being Nat holds
dom dyad(n) = Seg((2|^n)+1) & rng dyad(n) = dyadic(n)
proof
let n be Nat;
A1: dom dyad(n) = Seg((2|^n)+1) by Def4;
for x being object holds x in rng dyad(n) iff x in dyadic(n)
proof
let x be object;
A2: x in rng dyad(n) implies x in dyadic(n)
proof
assume x in rng dyad(n);
then consider y being object such that
A3: y in dom (dyad(n)) and
A4: x = (dyad(n)).y by FUNCT_1:def 3;
A5: y in Seg((2|^n)+1) by A3,Def4;
reconsider y as Nat by A3;
A6: 1 <= y by A5,FINSEQ_1:1;
y <= (2|^n) + 1 by A5,FINSEQ_1:1;
then
A7: y - 1 <= (2|^n) + 1 - 1 by XREAL_1:13;
consider i being Nat such that
A8: 1 + i = y by A6,NAT_1:10;
i in NAT & x = (y-1)/(2|^n) by A3,A4,Def4,ORDINAL1:def 12;
hence thesis by A7,A8,Def1;
end;
x in dyadic(n) implies x in rng (dyad(n))
proof
assume
A9: x in dyadic(n);
then reconsider x as Real;
consider i being Nat such that
A10: i <= 2|^n and
A11: x = i/(2|^n) by A9,Def1;
consider y being Nat such that
A12: y = i + 1;
0 + 1 <= i + 1 & i + 1 <= (2|^n) + 1 by A10,XREAL_1:6;
then
A13: y in Seg((2|^n)+1) by A12,FINSEQ_1:1;
then
A14: y in dom (dyad(n)) by Def4;
x = (y-1)/(2|^n) by A11,A12;
then x = (dyad(n)).y by A1,A13,Def4;
hence thesis by A14,FUNCT_1:def 3;
end;
hence thesis by A2;
end;
hence thesis by Def4,TARSKI:2;
end;
registration
cluster DYADIC -> non empty;
coherence
proof
ex x being object st x in dyadic(0) by XBOOLE_0:def 1;
hence thesis by Def2;
end;
end;
registration
cluster DOM -> non empty;
coherence;
end;
theorem Th5:
for n being Nat holds dyadic(n) c= dyadic(n+1)
proof
let n be Nat;
let x be object;
assume
A1: x in dyadic(n);
ex i being Nat st i <= 2|^(n+1) & x = i/(2|^(n+1))
proof
reconsider x as Real by A1;
consider i being Nat such that
A2: i <= 2|^n & x = i/(2|^n) by A1,Def1;
take i*2;
2|^(n+1) = (2|^n)*2 by NEWTON:6;
hence thesis by A2,XCMPLX_1:91,XREAL_1:64;
end;
hence thesis by Def1;
end;
theorem Th6:
for n being Nat holds 0 in dyadic(n) & 1 in dyadic(n)
proof
defpred P[Nat] means 0 in dyadic($1) & 1 in dyadic($1);
A1: for k being Nat st P[k] holds P[(k+1)]
proof
let k be Nat;
assume
A2: 0 in dyadic(k) & 1 in dyadic(k);
dyadic(k) c= dyadic(k+1) by Th5;
hence thesis by A2;
end;
A3: P[0] by Th2,TARSKI:def 2;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th7:
for n,i being Nat st 0 < i & i <= 2|^n holds (i*2-1)/
(2|^(n+1)) in dyadic(n+1) \ dyadic(n)
proof
let n,i be Nat;
assume that
A1: 0 < i and
A2: i <= 2|^n;
0*2 < i*2 by A1,XREAL_1:68;
then consider k being Nat such that
A3: i*2 = k + 1 by NAT_1:6;
A4: not (i*2-1)/(2|^(n+1)) in dyadic(n)
proof
assume (i*2-1)/(2|^(n+1)) in dyadic(n);
then consider s being Nat such that
s <= 2|^n and
A5: (i*2-1)/(2|^(n+1)) = s/(2|^n) by Def1;
A6: 2|^n <> 0 by NEWTON:83;
2|^(n+1) <> 0 by NEWTON:83;
then (i*2-1)*(2|^n) = s*(2|^(n+1)) by A5,A6,XCMPLX_1:95;
then (i*2-1)*(2|^n) = s*((2|^n)*2) by NEWTON:6;
then (i*2-1)*(2|^n) = s*2*(2|^n);
then (i*2-1)/(2|^n) = s*2/(2|^n) by A6,XCMPLX_1:94;
then i*2+(-1) = s*2 by A6,XCMPLX_1:53;
then 2*i + 0 = 2*s + 1;
then 0 = 1 by NAT_1:18;
hence thesis;
end;
i*2 <= (2|^n)*2 by A2,XREAL_1:64;
then i*2 <= 2|^(n+1) by NEWTON:6;
then
A7: k <= 2|^(n+1) by A3,NAT_1:13;
(i*2-1)/(2|^(n+1)) in dyadic(n+1) by A3,A7,Def1;
hence thesis by A4,XBOOLE_0:def 5;
end;
theorem Th8:
for n,i being Nat st 0 <= i & i < 2|^n holds (i*2+1)/
(2|^(n+1)) in dyadic(n+1) \ dyadic(n)
proof
let n,i be Nat;
assume that
0 <= i and
A1: i < 2|^n;
A2: 0 + 1 <= i + 1 by XREAL_1:6;
consider s being Nat such that
A3: s = i + 1;
A4: s*2 - 1 = i*2 + (1 + 0) by A3;
s <= 2|^n by A1,A3,NAT_1:13;
hence thesis by A2,A4,Th7;
end;
theorem Th9:
for n being Nat holds 1/(2|^(n+1)) in dyadic(n+1) \ dyadic(n)
proof
let n be Nat;
2*0 + 1 = 1 & 0 < 2|^n by NEWTON:83;
hence thesis by Th8;
end;
definition
let n be Nat;
let x be Element of dyadic(n);
func axis(x) -> Nat means
:Def5:
x = it/(2|^n);
existence
proof
consider i being Nat such that
i <= 2|^n and
A1: x = i/(2|^n) by Def1;
take i;
thus thesis by A1;
end;
uniqueness
proof
let i1,i2 be Nat;
assume
A2: x = i1/(2|^n) & x = i2/(2|^n);
A3: (2|^n) <> 0 by NEWTON:83;
then i1 = i1/(2|^n)*(2|^n) by XCMPLX_1:87
.= i2 by A2,A3,XCMPLX_1:87;
hence thesis;
end;
end;
theorem Th10:
for n being Nat holds for x being Element of dyadic(n) holds
x = axis(x)/(2|^n) & axis(x) <= (2|^n)
proof
let n be Nat;
let x be Element of dyadic(n);
ex i being Nat st i <= 2|^n & x = i/(2|^n) by Def1;
hence thesis by Def5;
end;
theorem
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)
proof
let n be Nat;
let x be Element of dyadic(n);
A1: 0 + axis(x) < 1 + axis(x) & 0 < 2|^n by NEWTON:83,XREAL_1:8;
x = axis(x)/(2|^n) & -1 + axis(x) < 0 + axis(x) by Def5,XREAL_1:8;
hence thesis by A1,XREAL_1:74;
end;
theorem Th12:
for n being Nat holds for x being Element of dyadic(n) holds
(axis(x)-1)/(2|^n) < (axis(x)+1)/(2|^n)
proof
let n be Nat;
let x be Element of dyadic(n);
-1 + axis(x) < 1 + axis(x) & 0 < 2|^n by NEWTON:83,XREAL_1:8;
hence thesis by XREAL_1:74;
end;
theorem Th13:
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) )
proof
let n be Nat;
let x be Element of dyadic(n+1);
assume
A1: not x in dyadic(n);
thus (axis(x)-1)/(2|^(n+1)) in dyadic(n)
proof
consider a being Real such that
A2: a = (axis(x)-1)/(2|^(n+1));
ex i being Nat st i <= 2|^n & a = i/(2|^n)
proof
consider s being Nat such that
A3: s <= (2|^(n+1)) and
A4: x = s/(2|^(n+1)) by Def1;
consider k being Element of NAT such that
A5: s = 2 * k or s = 2 * k + 1 by SCHEME1:1;
now
per cases by A5;
case
A6: s = k * 2;
then x = (k * 2)/((2|^n)* 2) by A4,NEWTON:6;
then
A7: x = k/(2|^n) by XCMPLX_1:91;
k * 2 <= (2|^n)* 2 by A3,A6,NEWTON:6;
then k <= ((2|^n)* 2)/2 by XREAL_1:77;
hence thesis by A1,A7,Def1;
end;
case
A8: s = k * 2 + 1;
A9: (2|^(n+1)) - 1 <= (2|^(n+1)) by XREAL_1:44;
k * 2 <= (2|^(n+1)) - 1 by A3,A8,XREAL_1:19;
then k * 2 <= (2|^(n+1)) by A9,XXREAL_0:2;
then k * 2 <= (2|^n)* 2 by NEWTON:6;
then
A10: k <= ((2|^n)* 2)/2 by XREAL_1:77;
take k;
a = (k * 2 + 1-1)/(2|^(n+1)) by A2,A4,A8,Def5
.= k * 2 /((2|^n)* 2) by NEWTON:6
.= (k/(2|^n))*(2/2) by XCMPLX_1:76
.= k/(2|^n);
hence thesis by A10;
end;
end;
hence thesis;
end;
hence thesis by A2,Def1;
end;
thus (axis(x)+1)/(2|^(n+1)) in dyadic(n)
proof
set a = (axis(x)+1)/(2|^(n+1));
ex i being Nat st i <= (2|^n) & a = i/(2|^n)
proof
consider s being Nat such that
A11: s <= (2|^(n+1)) and
A12: x = s/(2|^(n+1)) by Def1;
consider k being Element of NAT such that
A13: s = 2 * k or s = 2 * k + 1 by SCHEME1:1;
now
per cases by A13;
case
A14: s = k * 2;
then x = (k * 2)/((2|^n)* 2) by A12,NEWTON:6;
then
A15: x = k/(2|^n) by XCMPLX_1:91;
k * 2 <= (2|^n)* 2 by A11,A14,NEWTON:6;
then k <= ((2|^n)* 2)/2 by XREAL_1:77;
hence thesis by A1,A15,Def1;
end;
case
A16: s = k * 2 + 1;
consider l being Nat such that
A17: l = k + 1;
s <> (2|^(n+1))
proof
A18: 2|^(n+1) <> 0 by NEWTON:83;
assume s = (2|^(n+1));
then x = 1 by A12,A18,XCMPLX_1:60;
hence thesis by A1,Th6;
end;
then (k * 2 + 1 + 1) + (-1) < (2|^(n+1)) by A11,A16,XXREAL_0:1;
then l * 2 <= (2|^(n+1)) by A17,NAT_1:13;
then l * 2 <= (2|^n)* 2 by NEWTON:6;
then
A19: l <= ((2|^n)* 2)/2 by XREAL_1:77;
take l;
a = (k * 2 + 1 + 1)/(2|^(n+1)) by A12,A16,Def5
.= (k + 1) * 2 /((2|^n)* 2) by NEWTON:6
.= ((k + 1)/(2|^n))*(2/2) by XCMPLX_1:76
.= l/(2|^n) by A17;
hence thesis by A19;
end;
end;
hence thesis;
end;
hence thesis by Def1;
end;
end;
theorem Th14:
for n being Nat holds for x1,x2 being Element of dyadic(n) st
x1 < x2 holds axis(x1) < axis(x2)
proof
let n be Nat;
let x1,x2 be Element of dyadic(n);
x1 = axis(x1)/(2|^n) & x2 = axis(x2)/(2|^n) by Th10;
hence thesis by XREAL_1:72;
end;
theorem Th15:
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
proof
let n be Nat;
let x1,x2 be Element of dyadic(n);
assume
A1: x1 < x2;
then axis(x1) < axis(x2) by Th14;
then
A2: axis(x1) + 1 <= axis(x2) by NAT_1:13;
axis(x1) < axis(x2) by A1,Th14;
then axis(x1) + 1 <= axis(x2) by NAT_1:13;
then
A3: axis(x1) <= axis(x2) - 1 by XREAL_1:19;
A4: (axis(x1)+ 1)/(2|^n) <= axis(x2)/(2|^n) by A2,XREAL_1:72;
axis(x1)/(2|^n) <= (axis(x2) - 1)/(2|^n) by A3,XREAL_1:72;
hence thesis by A4,Th10;
end;
theorem Th16:
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))
proof
let n be Nat;
let x1,x2 be Element of dyadic(n+1);
assume that
A1: x1 < x2 and
A2: not x1 in dyadic(n) and
A3: not x2 in dyadic(n);
consider k2 being Element of NAT such that
A4: axis(x2) = 2 * k2 or axis(x2) = 2 * k2 + 1 by SCHEME1:1;
A5: axis(x2) <> k2 * 2
proof
assume
A6: axis(x2) = k2 * 2;
then x2 = (k2 * 2)/(2|^(n+1)) by Th10;
then
A7: x2 = (k2 * 2)/((2|^n) * 2) by NEWTON:6
.= (k2/(2|^n))*(2/2) by XCMPLX_1:76
.= k2/(2|^n);
k2 * 2 <= (2|^(n+1)) by A6,Th10;
then k2 * 2 <= (2|^n) * 2 by NEWTON:6;
then k2 <= ((2|^n)* 2)/2 by XREAL_1:77;
hence thesis by A3,A7,Def1;
end;
consider k1 being Element of NAT such that
A8: axis(x1) = 2 * k1 or axis(x1) = 2 * k1 + 1 by SCHEME1:1;
A9: not axis(x1) = k1 * 2
proof
assume
A10: axis(x1) = k1 * 2;
then x1 = (k1 * 2)/(2|^(n+1)) by Th10;
then
A11: x1 = (k1 * 2)/((2|^n) * 2) by NEWTON:6
.= (k1/(2|^n))*(2/2) by XCMPLX_1:76
.= k1/(2|^n);
k1 * 2 <= (2|^(n+1)) by A10,Th10;
then k1 * 2 <= (2|^n) * 2 by NEWTON:6;
then k1 <= ((2|^n)* 2)/2 by XREAL_1:77;
hence thesis by A2,A11,Def1;
end;
then k1 * 2 + 1 < k2 * 2 + 1 by A1,A8,A4,A5,Th14;
then k1 * 2 + 1 + (-1) < k2 * 2 + 1 + (-1) by XREAL_1:6;
then (k1 * 2)/2 < (k2 * 2)/2 by XREAL_1:74;
then k1 + 1 <= k2 by NAT_1:13;
then 0 < (2|^(n+1)) & (k1 + 1) * 2 <= k2 * 2 by NEWTON:83,XREAL_1:64;
hence thesis by A8,A4,A9,A5,XREAL_1:72;
end;
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 :: redefines Nbhd (URYSOHN1, synonym) → a_neighborhood (CONNSP_2, definition)
ex A being Subset of T st A is open & x in A & A c= it;
compatibility
proof
let S be Subset of T;
hereby
assume
A1: S is a_neighborhood of x;
take N = Int S;
thus N is open;
thus x in N by A1,CONNSP_2:def 1;
thus N c= S by TOPS_1:16;
end;
assume ex A being Subset of T st A is open & x in A & A c= S;
hence x in Int S by TOPS_1:22;
end;
end;
theorem Th17:
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
proof
let T be non empty TopSpace;
let A be Subset of T;
thus A is open implies for x being Point of T st x in A ex B being Nbhd of x
,T st B c= A
proof
assume
A1: A is open;
let x be Point of T;
assume x in A;
then ex B being Subset of T st B is a_neighborhood of x & B c= A by A1,
CONNSP_2:7;
hence thesis;
end;
assume
A2: for x being Point of T holds x in A implies ex B being Nbhd of x,T
st B c= A;
for x being Point of T st x in A ex B being Subset of T st B is
a_neighborhood of x & B c= A
proof
let x be Point of T;
assume x in A;
then ex B being Nbhd of x,T st B c= A by A2;
hence thesis;
end;
hence thesis by CONNSP_2:7;
end;
theorem
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
proof
let T be non empty TopSpace;
let A be Subset of T;
assume
A1: for x being Point of T st x in A holds A is Nbhd of x,T;
for x being Point of T holds x in A implies ex B being Nbhd of x,T st B c= A
proof
let x be Point of T;
assume
A2: x in A;
ex B being Nbhd of x,T st B c= A
proof
A is Nbhd of x,T by A1,A2;
then consider B being Nbhd of x,T such that
A3: B = A;
take B;
thus thesis by A3;
end;
hence thesis;
end;
hence thesis by Th17;
end;
definition
let T be TopSpace;
redefine attr T is T_1 means :: redefines T_1 (PRE_TOPC, definition)
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;
compatibility
proof
thus T is T_1 implies 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
proof
assume
A1: T is T_1;
let p,q being Point of T such that
A2: not p = q;
consider G1 being Subset of T such that
A3: G1 is open & p in G1 & q in G1` by A1,A2;
consider G2 being Subset of T such that
A4: G2 is open & q in G2 & p in G2` by A1,A2;
take G1,G2;
thus thesis by A3,A4,XBOOLE_0:def 5;
end;
assume
A5: 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;
let p,q being Point of T;
assume p <> q;
then consider W,V being Subset of T such that
A6: W is open and
V is open and
A7: p in W & not q in W and
q in V and
not p in V by A5;
take W;
thus thesis by A6,A7,XBOOLE_0:def 5;
end;
end;
theorem Th19:
for T being non empty TopSpace holds T is T_1 iff for p being
Point of T holds {p} is closed
proof
let T be non empty TopSpace;
thus T is T_1 implies for p being Point of T holds {p} is closed
proof
assume
A1: T is T_1;
for p being Point of T holds {p} is closed
proof
let p be Point of T;
consider B being Subset of T such that
A2: B = {p}`;
defpred Q[Subset of T] means ex q being Point of T st (q in B & for V
being Subset of T st $1 = V holds (V is open & q in V & not p in V ));
consider F being Subset-Family of T such that
A3: for C being Subset of T holds C in F iff Q[C] from SUBSET_1:sch
3;
A4: for C being Subset of T holds (C in F iff ex q being Point of T st
q in B & C is open & q in C & not p in C )
proof
let C be Subset of T;
A5: (ex q being Point of T st (q in B & C is open & q in C & not p in
C)) implies C in F
proof
assume
A6: ex q being Point of T st q in B & C is open & q in C & not p in C;
ex q being Point of T st (q in B & for V being Subset of T st C
= V holds V is open & q in V & not p in V )
proof
consider q being Point of T such that
A7: q in B & C is open & q in C & not p in C by A6;
take q;
thus thesis by A7;
end;
hence thesis by A3;
end;
C in F implies ex q being Point of T st q in B & C is open & q in
C & not p in C
proof
assume C in F;
then consider q being Point of T such that
A8: q in B & for V being Subset of T st C = V holds V is open &
q in V & not p in V by A3;
take q;
thus thesis by A8;
end;
hence thesis by A5;
end;
for x being object holds x in F implies x in the topology of T
proof
let x be object;
assume
A9: x in F;
then reconsider x as Subset of T;
ex q being Point of T st q in B & x is open & q in x & not p in x
by A4,A9;
hence thesis;
end;
then
A10: F c= the topology of T;
A11: for q being Point of T st q in B holds ex V being Subset of T st V
is open & q in V & not p in V
proof
let q be Point of T;
assume q in B;
then not q in {p} by A2,XBOOLE_0:def 5;
then not q = p by TARSKI:def 1;
then
ex V,W being Subset of T st V is open & W is open & q in V & not p
in V & p in W & not q in W by A1;
then consider V being Subset of T such that
A12: V is open & q in V & not p in V;
take V;
thus thesis by A12;
end;
for x being object holds x in B implies x in union F
proof
let x be object;
assume
A13: x in B;
then reconsider x as Point of T;
consider C being Subset of T such that
A14: C is open & x in C & not p in C by A11,A13;
ex C being set st x in C & C in F
by A4,A13,A14;
hence thesis by TARSKI:def 4;
end;
then
A15: B c= union F;
for x being object holds x in union F implies x in B
proof
let x be object;
assume x in union F;
then consider C being set such that
A16: x in C and
A17: C in F by TARSKI:def 4;
reconsider C as Subset of T by A17;
ex q being Point of T st q in B & C is open & q in C & not p in C
by A4,A17;
then C c= [#](T) \ {p} by ZFMISC_1:34;
hence thesis by A2,A16;
end;
then union F c= B;
then B = union F by A15;
then B in the topology of T by A10,PRE_TOPC:def 1;
then {p}` = [#](T) \ {p} & B is open;
hence thesis by A2;
end;
hence thesis;
end;
assume
A18: for p being Point of T holds {p} is closed;
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
proof
let p,q be Point of T;
consider V,W being Subset of T such that
A19: V = {p}` and
A20: W = {q}`;
p in {p} by TARSKI:def 1;
then
A21: not p in V by A19,XBOOLE_0:def 5;
assume
A22: not p = q;
then not p in {q} by TARSKI:def 1;
then
A23: p in W by A20,XBOOLE_0:def 5;
q in {q} by TARSKI:def 1;
then
A24: not q in W by A20,XBOOLE_0:def 5;
not q in {p} by A22,TARSKI:def 1;
then
A25: q in V by A19,XBOOLE_0:def 5;
{p} is closed & {q} is closed by A18;
hence thesis by A19,A20,A23,A24,A25,A21;
end;
hence thesis;
end;
theorem Th20:
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
proof
let T be non empty TopSpace;
assume
A1: T is normal;
let A,B be open Subset of T;
assume that
A2: A <> {} and
A3: Cl(A) c=B;
now
per cases;
case
A4: B <> [#](T);
reconsider W = Cl(A), V = [#](T) \ B as Subset of T;
A5: W <> {} & V <> {}
proof
A6: [#](T) \ B <> {}
proof
assume [#](T) \ B = {};
then B = [#](T) \ {} by PRE_TOPC:3;
hence thesis by A4;
end;
A c= Cl(A) by PRE_TOPC:18;
hence thesis by A2,A6;
end;
A7: W misses V
proof
assume W meets V;
then consider x being object such that
A8: x in W /\ V by XBOOLE_0:4;
x in Cl(A) & x in [#](T) \ B by A8,XBOOLE_0:def 4;
hence thesis by A3,XBOOLE_0:def 5;
end;
B = [#](T) \ V by PRE_TOPC:3;
then V is closed;
then consider C,Q being Subset of T such that
A9: C is open and
A10: Q is open and
A11: W c= C and
A12: V c= Q and
A13: C misses Q by A1,A7;
take C;
C <> {} & Cl(A) c= C & Cl(C) c= B
proof
consider Q0,C0 being Subset of [#](T) such that
A14: Q0 = Q & C0 = C;
C0 c= Q0` by A13,A14,SUBSET_1:23;
then Cl(C) c= Q` by A10,A14,TOPS_1:5;
then Cl(C) misses Q by SUBSET_1:23;
then
A15: V misses Cl(C) by A12,XBOOLE_1:63;
B`` = B;
hence thesis by A5,A11,A15,SUBSET_1:23;
end;
hence thesis by A9;
end;
case
A16: B = [#](T);
consider C being Subset of T such that
A17: C = [#](T);
take C;
Cl(C) c= B by A16;
hence thesis by A17;
end;
end;
hence thesis;
end;
theorem
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
proof
let T be non empty TopSpace;
thus T is regular implies 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
proof
assume
A1: T is regular;
thus 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
proof
let A be open Subset of T;
let p be Point of T;
assume
A2: p in A;
then
A3: p in A``;
thus ex B being open Subset of T st p in B & Cl(B) c= A
proof
reconsider P = A` as Subset of T;
now
per cases;
case
P <> {};
consider W,V being Subset of T such that
A4: W is open and
A5: V is open and
A6: p in W and
A7: P c= V and
A8: W misses V by A1,A3;
W /\ V = {} by A8;
then V /\ Cl(W) c= Cl({} T) by A5,TOPS_1:13;
then V /\ Cl(W) c= {} by PRE_TOPC:22;
then V /\ Cl(W) = {};
then V misses Cl(W);
then
A9: P misses Cl(W) by A7,XBOOLE_1:63;
take W;
A`` = A;
then Cl(W) c= A by A9,SUBSET_1:23;
hence thesis by A4,A6;
end;
case
A10: P = {};
take A;
A = [#](T) by A10,PRE_TOPC:4;
then Cl(A) c= A;
hence thesis by A2;
end;
end;
hence thesis;
end;
end;
end;
assume
A11: 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;
for p being Point of T for P being Subset of T st P <> {} & P is closed
& p in P` ex W,V being Subset of T st W is open & V is open & p in W & P c= V &
W misses V
proof
let p be Point of T;
let P be Subset of T;
assume that
P <> {} and
A12: P is closed & p in P`;
thus ex W,V being Subset of T st W is open & V is open & p in W & P c= V &
W misses V
proof
consider A being Subset of T such that
A13: A = P`;
consider B being open Subset of T such that
A14: p in B & Cl(B) c= A by A11,A12,A13;
consider C being Subset of T such that
A15: C = [#](T) \ Cl(B);
reconsider B,C as Subset of T;
Cl(B) misses C by A15,XBOOLE_1:79;
then
A16: B misses C by PRE_TOPC:18,XBOOLE_1:63;
take B;
take C;
(Cl(B))` is open & P`` = P;
hence thesis by A13,A14,A15,A16,XBOOLE_1:34;
end;
end;
hence T is regular by COMPTS_1:def 2;
end;
theorem
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
proof
let T be non empty TopSpace;
assume that
A1: T is normal and
A2: T is T_1;
let A be open Subset of T;
assume
A3: A <> {};
now
per cases;
case
A <> [#](T);
reconsider V = [#](T) \ A as Subset of T;
consider x being object such that
A4: x in A by A3,XBOOLE_0:def 1;
A = [#](T) \ V by PRE_TOPC:3;
then
A5: V is closed;
reconsider x as Point of T by A4;
consider W being set such that
A6: W = {x};
reconsider W as Subset of T by A6;
A7: W misses V
proof
assume W meets V;
then consider z being object such that
A8: z in W /\ V by XBOOLE_0:4;
z in W by A8,XBOOLE_0:def 4;
then
A9: z in A by A4,A6,TARSKI:def 1;
z in V by A8,XBOOLE_0:def 4;
hence thesis by A9,XBOOLE_0:def 5;
end;
W is closed by A2,A6,Th19;
then consider B,Q being Subset of T such that
B is open and
A10: Q is open and
A11: W c= B and
A12: V c= Q and
A13: B misses Q by A1,A5,A7;
take B;
B <> {} & Cl(B) c= A
proof
B c= Q` by A13,SUBSET_1:23;
then Cl(B) c= Q` by A10,TOPS_1:5;
then Cl(B) misses Q by SUBSET_1:23;
then
A14: V misses Cl(B) by A12,XBOOLE_1:63;
A`` = A;
hence thesis by A6,A11,A14,SUBSET_1:23;
end;
hence thesis;
end;
case
A15: A = [#](T);
consider B being Subset of T such that
A16: B = [#](T);
take B;
Cl(B) c= A by A15;
hence thesis by A16;
end;
end;
hence thesis;
end;
theorem
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
proof
let T be non empty TopSpace;
assume
A1: T is normal;
let A,B be Subset of T such that
A2: A is open and
A3: B is closed & B <> {} and
A4: B c= A;
per cases;
suppose
A <> [#](T);
reconsider V = [#](T) \ A as Subset of T;
A5: A = [#](T) \ V by PRE_TOPC:3;
A6: B misses V
proof
assume B /\ V <> {};
then consider z being object such that
A7: z in B /\ V by XBOOLE_0:def 1;
z in B & z in V by A7,XBOOLE_0:def 4;
hence thesis by A4,XBOOLE_0:def 5;
end;
V is closed by A2,A5;
then consider C,Q being Subset of T such that
A8: C is open and
A9: Q is open and
A10: B c= C and
A11: V c= Q and
A12: C misses Q by A1,A3,A6;
C c= Q` by A12,SUBSET_1:23;
then Cl(C) c= Q` by A9,TOPS_1:5;
then Q misses Cl(C) by SUBSET_1:23;
then
A13: V misses Cl(C) by A11,XBOOLE_1:63;
take C;
thus C is open & B c= C by A8,A10;
A`` = A;
hence thesis by A13,SUBSET_1:23;
end;
suppose
A14: A = [#](T);
take [#](T);
thus thesis by A14;
end;
end;
begin
::
:: Some increasing family of sets in normal space
::
definition
let T be non empty TopSpace;
let A,B be Subset of T;
assume
A1: T is normal & A <> {} & A is open & B is open & Cl(A) c= B;
mode Between of A,B -> Subset of T means
:Def8:
it <> {} & it is open & Cl( A) c= it & Cl(it) c= B;
existence by A1,Th20;
end;
theorem
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)
proof
let T be non empty TopSpace such that
A1: T is normal;
let A,B be closed Subset of T such that
A2: A <> {};
let n be Nat;
let G be Function of dyadic(n),bool the carrier of T such that
A3: A c= G.0 and
A4: B = [#](T) \ G.1 and
A5: 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;
A6: for r being Element of dyadic(n) holds G.r <> {}
proof
let r be Element of dyadic(n);
per cases by Th1;
suppose
0 = r;
hence thesis by A2,A3;
end;
suppose
A7: 0 < r;
reconsider q1 = 0 as Element of dyadic(n) by Th6;
G.q1 c= Cl(G.q1) & Cl(G.q1) c= G.r by A5,A7,PRE_TOPC:18;
hence thesis by A2,A3;
end;
end;
reconsider S = dyadic(n+1) \ dyadic(n) as non empty set by Th9;
A8: 0 in dyadic(n+1) & 1 in dyadic(n+1) by Th6;
defpred P[Element of S,Subset of T] means for r being Element of dyadic(n+1)
st r in S & $1 = r holds for r1,r2 being Element of dyadic(n) st
r1 = (axis(r)-1)/(2|^(n+1)) & r2 = (axis(r)+1)/(2|^(n+1)) holds
$2 is Between of G.r1,G.r2;
A9: for x being Element of S ex y being Subset of T st P[x,y]
proof
let x be Element of S;
A10: not x in dyadic(n) by XBOOLE_0:def 5;
reconsider x as Element of dyadic(n+1) by XBOOLE_0:def 5;
(axis(x)-1)/(2|^(n+1)) in dyadic(n) & (axis(x)+1)/(2|^(n+1))
in dyadic(n) by A10,Th13;
then consider q1,q2 being Element of dyadic(n) such that
A11: q1 = (axis(x)-1)/(2|^(n+1)) & q2 = (axis(x)+1)/(2|^(n+1));
take the Between of G.q1, G.q2;
thus thesis by A11;
end;
consider D being Function of S,bool the carrier of T such that
A12: for x being Element of S holds P[x,D.x] from FUNCT_2:sch 3(A9);
defpred W[Element of dyadic(n+1),Subset of T] means for r being Element of
dyadic(n+1) st $1 = r holds ((r in dyadic(n) implies $2 = G.r) & (not r in
dyadic(n) implies $2 = D.r));
A13: for x being Element of dyadic(n+1) ex y being Subset of T st W[x,y]
proof
let x be Element of dyadic(n+1);
per cases;
suppose
x in dyadic(n);
then reconsider x as Element of dyadic(n);
consider y being Subset of T such that
A14: y = G.x;
take y;
thus thesis by A14;
end;
suppose
A15: not x in dyadic(n);
then reconsider x as Element of S by XBOOLE_0:def 5;
consider y being Subset of T such that
A16: y = D.x;
take y;
thus thesis by A15,A16;
end;
end;
consider F being Function of dyadic(n+1),bool the carrier of T such that
A17: for x being Element of dyadic(n+1) holds W[x,F.x] from FUNCT_2:sch
3 (A13);
take F;
0 in dyadic(n) & 1 in dyadic(n) by Th6;
hence A c= F.0 & B = [#](T) \ F.1 by A3,A4,A17,A8;
let r1,r2,r be Element of dyadic(n+1) such that
A18: r1 < r2;
thus F.r1 is open & F.r2 is open & Cl(F.r1) c= F.r2
proof
now
per cases;
suppose
A19: r1 in dyadic(n) & r2 in dyadic(n);
then
A20: F.r1 = G.r1 & F.r2 = G.r2 by A17;
reconsider r1,r2 as Element of dyadic(n) by A19;
r1 < r2 by A18;
hence thesis by A5,A20;
end;
suppose
A21: r1 in dyadic(n) & not r2 in dyadic(n);
then
(axis(r2)-1)/(2|^(n+1)) in dyadic(n) & (axis(r2)+1)/(2|^(
n+1)) in dyadic(n) by Th13;
then consider q1,q2 being Element of dyadic(n) such that
A22: q1 = (axis(r2)-1)/(2|^(n+1)) and
A23: q2 = (axis(r2)+1)/(2|^(n+1));
A24: r1 <= q1 by A18,A22,Th15;
r2 in S by A21,XBOOLE_0:def 5;
then
A25: D.r2 is Between of (G.q1),(G.q2) by A12,A22,A23;
A26: q1 < q2 by A22,A23,Th12;
then
A27: G.q2 is open & Cl(G.q1) c= G. q2 by A5;
A28: F.r2 = D.r2 by A17,A21;
A29: G.q1 <> {} by A6;
A30: G.q1 is open by A5,A26;
then
A31: Cl(G.q1) c= F.r2 by A1,A28,A25,A29,A27,Def8;
now
per cases by A24,XXREAL_0:1;
suppose
r1 = q1;
hence thesis by A1,A17,A28,A25,A29,A30,A27,A31,Def8;
end;
suppose
A32: r1 < q1;
A33: G.q1 c= Cl(G.q1) by PRE_TOPC:18;
consider q0 being Element of dyadic(n) such that
A34: q0 = r1 by A21;
Cl(G.q0) c= G.q1 by A5,A32,A34;
then Cl(F.r1) c= G.q1 by A17,A34;
then
A35: Cl(F.r1) c= Cl(G.q1) by A33;
A36: G.q0 is open by A5,A32,A34;
A37: G.q1 is open by A5,A32,A34;
then Cl(G.q1) c= F.r2 by A1,A28,A25,A29,A27,Def8;
hence thesis by A1,A17,A28,A25,A29,A27,A34,A36,A37,A35,Def8;
end;
end;
hence thesis;
end;
suppose
A38: not r1 in dyadic(n) & r2 in dyadic(n);
then
(axis(r1)-1)/(2|^(n+1)) in dyadic(n) &
(axis(r1)+1)/(2|^(n+1)) in dyadic(n) by Th13;
then consider q1,q2 being Element of dyadic(n) such that
A39: q1 = (axis(r1)-1)/(2|^(n+1)) and
A40: q2 = (axis(r1)+1)/(2|^(n+1));
A41: q2 <= r2 by A18,A40,Th15;
r1 in S by A38,XBOOLE_0:def 5;
then
A42: D.r1 is Between of (G.q1),(G.q2) by A12,A39,A40;
A43: q1 < q2 by A39,A40,Th12;
then
A44: G.q1 is open & Cl(G.q1) c= G. q2 by A5;
A45: F.r1 = D.r1 by A17,A38;
A46: G.q1 <> {} by A6;
A47: G.q2 is open by A5,A43;
then
A48: Cl(F.r1) c= G.q2 by A1,A45,A42,A46,A44,Def8;
now
per cases by A41,XXREAL_0:1;
suppose
q2 = r2;
hence thesis by A1,A17,A45,A42,A46,A47,A44,A48,Def8;
end;
suppose
A49: q2 < r2;
A50: G.q2 c= Cl(G.q2) by PRE_TOPC:18;
consider q3 being Element of dyadic(n) such that
A51: q3 = r2 by A38;
A52: G.q2 is open by A5,A49,A51;
then Cl(F.r1) c= G.q2 by A1,A45,A42,A46,A44,Def8;
then
A53: Cl(F.r1) c= Cl(G.q2) by A50;
Cl(G.q2) c= G.q3 by A5,A49,A51;
then
A54: Cl(G.q2) c= F.r2 by A17,A51;
G.q3 is open by A5,A49,A51;
hence thesis by A1,A17,A45,A42,A46,A44,A51,A52,A53,A54,Def8;
end;
end;
hence thesis;
end;
suppose
A55: not r1 in dyadic(n) & not r2 in dyadic(n);
then
(axis(r1)-1)/(2|^(n+1)) in dyadic(n) &
(axis(r1)+1)/(2|^(n+1)) in dyadic(n) by Th13;
then consider q11,q21 being Element of dyadic(n) such that
A56: q11 = (axis(r1)-1)/(2|^(n+1)) and
A57: q21 = (axis(r1)+1)/(2|^(n+1));
r1 in S by A55,XBOOLE_0:def 5;
then
A58: D.r1 is Between of (G.q11),(G.q21) by A12,A56,A57;
A59: q11 < q21 by A56,A57,Th12;
then
A60: G.q21 is open by A5;
(axis(r2)-1)/(2|^(n+1)) in dyadic(n) &
(axis(r2)+1)/(2|^(n+1)) in dyadic(n) by A55,Th13;
then consider q12,q22 being Element of dyadic(n) such that
A61: q12 = (axis(r2)-1)/(2|^(n+1)) and
A62: q22 = (axis(r2)+1)/(2|^(n+1));
r2 in S by A55,XBOOLE_0:def 5;
then
A63: D.r2 is Between of (G.q12),(G.q22) by A12,A61,A62;
A64: q12 < q22 by A61,A62,Th12;
then
A65: G.q12 is open by A5;
A66: G.q22 is open & Cl(G.q12) c= G.q22 by A5,A64;
A67: G.q12 <> {} by A6;
A68: G.q11 <> {} by A6;
A69: F.r2 = D.r2 by A17,A55;
A70: F.r1 = D.r1 by A17,A55;
A71: G.q11 is open & Cl(G.q11) c= G.q21 by A5,A59;
hence F.r1 is open & F.r2 is open by A1,A70,A58,A68,A60,A69,A63,A67,A65
,A66,Def8;
A72: q21 <= q12 by A18,A55,A57,A61,Th16;
now
per cases by A72,XXREAL_0:1;
suppose
A73: q21 = q12;
Cl(F.r1) c= G.q21 & G.q21 c= Cl(G.q21) by A1,A70,A58,A68,A60,A71
,Def8,PRE_TOPC:18;
then
A74: Cl(F.r1) c= Cl(G.q21);
Cl(G.q21) c= F.r2 by A1,A60,A69,A63,A67,A66,A73,Def8;
hence Cl(F.r1) c= F.r2 by A74;
end;
suppose
A75: q21 < q12;
Cl(F.r1) c= G.q21 & G.q21 c= Cl(G.q21) by A1,A70,A58,A68,A60,A71
,Def8,PRE_TOPC:18;
then
A76: Cl(F.r1) c= Cl(G.q21);
Cl(G.q21) c= G.q12 by A5,A75;
then
A77: Cl(F.r1) c= G.q12 by A76;
G.q12 c= Cl(G.q12) & Cl(G.q12) c= F.r2 by A1,A69,A63,A67,A65,A66
,Def8,PRE_TOPC:18;
then G.q12 c= F.r2;
hence Cl(F.r1) c= F.r2 by A77;
end;
end;
hence Cl(F.r1) c= F.r2;
end;
end;
hence thesis;
end;
thus thesis by A17;
end;