:: URYSOHN1 semantic presentation
begin
definition
let n be Nat;
func dyadic n -> Subset of REAL means :Def1: :: URYSOHN1:def 1
for x being Real holds
( x in it iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) );
existence
ex b1 being Subset of REAL st
for x being Real holds
( x in b1 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) )
proof
defpred S1[ set ] means ex i being Element of NAT st
( i <= 2 |^ n & $1 = i / (2 |^ n) );
ex X being Subset of REAL st
for x being Real holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
hence ex b1 being Subset of REAL st
for x being Real holds
( x in b1 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of REAL st ( for x being Real holds
( x in b1 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds
( x in b2 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) holds
b1 = b2
proof
let A1, A2 be Subset of REAL; ::_thesis: ( ( for x being Real holds
( x in A1 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds
( x in A2 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) implies A1 = A2 )
assume that
A1: for x being Real holds
( x in A1 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) and
A2: for x being Real holds
( x in A2 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ; ::_thesis: A1 = A2
for a being set holds
( a in A1 iff a in A2 )
proof
let a be set ; ::_thesis: ( a in A1 iff a in A2 )
thus ( a in A1 implies a in A2 ) ::_thesis: ( a in A2 implies a in A1 )
proof
assume A3: a in A1 ; ::_thesis: a in A2
then reconsider a = a as Real ;
ex i being Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) ) by A1, A3;
hence a in A2 by A2; ::_thesis: verum
end;
assume A4: a in A2 ; ::_thesis: a in A1
then reconsider a = a as Real ;
ex i being Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) ) by A2, A4;
hence a in A1 by A1; ::_thesis: verum
end;
hence A1 = A2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines dyadic URYSOHN1:def_1_:_
for n being Nat
for b2 being Subset of REAL holds
( b2 = dyadic n iff for x being Real holds
( x in b2 iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) );
definition
func DYADIC -> Subset of REAL means :Def2: :: URYSOHN1:def 2
for a being Real holds
( a in it iff ex n being Element of NAT st a in dyadic n );
existence
ex b1 being Subset of REAL st
for a being Real holds
( a in b1 iff ex n being Element of NAT st a in dyadic n )
proof
defpred S1[ set ] means ex i being Element of NAT st $1 in dyadic i;
ex X being Subset of REAL st
for x being Real holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
hence ex b1 being Subset of REAL st
for a being Real holds
( a in b1 iff ex n being Element of NAT st a in dyadic n ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of REAL st ( for a being Real holds
( a in b1 iff ex n being Element of NAT st a in dyadic n ) ) & ( for a being Real holds
( a in b2 iff ex n being Element of NAT st a in dyadic n ) ) holds
b1 = b2
proof
let A1, A2 be Subset of REAL; ::_thesis: ( ( for a being Real holds
( a in A1 iff ex n being Element of NAT st a in dyadic n ) ) & ( for a being Real holds
( a in A2 iff ex n being Element of NAT st a in dyadic n ) ) implies A1 = A2 )
assume that
A1: for x being Real holds
( x in A1 iff ex n being Element of NAT st x in dyadic n ) and
A2: for x being Real holds
( x in A2 iff ex n being Element of NAT st x in dyadic n ) ; ::_thesis: A1 = A2
for a being set holds
( a in A1 iff a in A2 )
proof
let a be set ; ::_thesis: ( a in A1 iff a in A2 )
thus ( a in A1 implies a in A2 ) ::_thesis: ( a in A2 implies a in A1 )
proof
assume A3: a in A1 ; ::_thesis: a in A2
then reconsider a = a as Real ;
ex n being Element of NAT st a in dyadic n by A1, A3;
hence a in A2 by A2; ::_thesis: verum
end;
thus ( a in A2 implies a in A1 ) ::_thesis: verum
proof
assume A4: a in A2 ; ::_thesis: a in A1
then reconsider a = a as Real ;
ex n being Element of NAT st a in dyadic n by A2, A4;
hence a in A1 by A1; ::_thesis: verum
end;
end;
hence A1 = A2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines DYADIC URYSOHN1:def_2_:_
for b1 being Subset of REAL holds
( b1 = DYADIC iff for a being Real holds
( a in b1 iff ex n being Element of NAT st a in dyadic n ) );
definition
func DOM -> Subset of REAL equals :: URYSOHN1:def 3
((halfline 0) \/ DYADIC) \/ (right_open_halfline 1);
coherence
((halfline 0) \/ DYADIC) \/ (right_open_halfline 1) is Subset of REAL ;
end;
:: deftheorem defines DOM URYSOHN1:def_3_:_
DOM = ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1);
definition
let T be TopSpace;
let A be non empty Subset of REAL;
let F be Function of A,(bool the carrier of T);
let r be Element of A;
:: original: .
redefine funcF . r -> Subset of T;
coherence
F . r is Subset of T
proof
F . r is Subset of T ;
hence F . r is Subset of T ; ::_thesis: verum
end;
end;
theorem Th1: :: URYSOHN1:1
for n being Element of NAT
for x being Real st x in dyadic n holds
( 0 <= x & x <= 1 )
proof
let n be Element of NAT ; ::_thesis: for x being Real st x in dyadic n holds
( 0 <= x & x <= 1 )
let x be Real; ::_thesis: ( x in dyadic n implies ( 0 <= x & x <= 1 ) )
assume x in dyadic n ; ::_thesis: ( 0 <= x & x <= 1 )
then consider i being Element of NAT such that
A1: i <= 2 |^ n and
A2: x = i / (2 |^ n) by Def1;
0 <= i by NAT_1:2;
then ( 0 / (2 |^ n) <= i / (2 |^ n) & i / (2 |^ n) <= (2 |^ n) / (2 |^ n) ) by A1, XREAL_1:72;
hence ( 0 <= x & x <= 1 ) by A2, XCMPLX_1:60; ::_thesis: verum
end;
theorem Th2: :: URYSOHN1:2
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 Element of NAT st
( i <= 1 & x = i ) )
proof
let x be Real; ::_thesis: ( x in dyadic 0 iff ex i being Element of NAT st
( i <= 1 & x = i ) )
A3: ( ex i being Element of NAT st
( i <= 1 & x = i ) implies x in dyadic 0 )
proof
given i being Element of NAT such that A4: i <= 1 and
A5: x = i ; ::_thesis: x in dyadic 0
x = i / 1 by A5;
hence x in dyadic 0 by A1, A4, Def1; ::_thesis: verum
end;
( x in dyadic 0 implies ex i being Element of NAT st
( i <= 1 & x = i ) )
proof
assume x in dyadic 0 ; ::_thesis: ex i being Element of NAT st
( i <= 1 & x = i )
then ex i being Element of NAT st
( i <= 1 & x = i / 1 ) by A1, Def1;
hence ex i being Element of NAT st
( i <= 1 & x = i ) ; ::_thesis: verum
end;
hence ( x in dyadic 0 iff ex i being Element of NAT st
( i <= 1 & x = i ) ) by A3; ::_thesis: verum
end;
for x being set holds
( x in dyadic 0 iff x in {0,1} )
proof
let x be set ; ::_thesis: ( x in dyadic 0 iff x in {0,1} )
A6: ( x in dyadic 0 implies x in {0,1} )
proof
assume A7: x in dyadic 0 ; ::_thesis: x in {0,1}
then reconsider x = x as Real ;
consider i being Element of NAT such that
A8: i <= 1 and
A9: x = i by A2, A7;
A10: 0 <= i by NAT_1:2;
i <= 0 + 1 by A8;
then ( x = 0 or x = 1 ) by A10, A9, NAT_1:9;
hence x in {0,1} by TARSKI:def_2; ::_thesis: verum
end;
( x in {0,1} implies x in dyadic 0 )
proof
assume x in {0,1} ; ::_thesis: x in dyadic 0
then ( x = 0 or x = 1 ) by TARSKI:def_2;
hence x in dyadic 0 by A2; ::_thesis: verum
end;
hence ( x in dyadic 0 iff x in {0,1} ) by A6; ::_thesis: verum
end;
hence dyadic 0 = {0,1} by TARSKI:1; ::_thesis: verum
end;
theorem :: URYSOHN1:3
dyadic 1 = {0,(1 / 2),1}
proof
A1: 2 |^ 1 = 2 by NEWTON:5;
for x being set holds
( x in dyadic 1 iff x in {0,(1 / 2),1} )
proof
let x be set ; ::_thesis: ( x in dyadic 1 iff x in {0,(1 / 2),1} )
A2: ( x in {0,(1 / 2),1} implies x in dyadic 1 )
proof
assume A3: x in {0,(1 / 2),1} ; ::_thesis: x in dyadic 1
percases ( x = 0 or x = 1 / 2 or x = 1 ) by A3, ENUMSET1:def_1;
suppose x = 0 ; ::_thesis: x in dyadic 1
then x = 0 / 2 ;
hence x in dyadic 1 by A1, Def1; ::_thesis: verum
end;
suppose x = 1 / 2 ; ::_thesis: x in dyadic 1
hence x in dyadic 1 by A1, Def1; ::_thesis: verum
end;
supposeA4: x = 1 ; ::_thesis: x in dyadic 1
then reconsider x = x as Real ;
x = 2 / 2 by A4;
hence x in dyadic 1 by A1, Def1; ::_thesis: verum
end;
end;
end;
( x in dyadic 1 implies x in {0,(1 / 2),1} )
proof
assume A5: x in dyadic 1 ; ::_thesis: x in {0,(1 / 2),1}
then reconsider x = x as Real ;
consider i being Element of NAT such that
A6: i <= 2 and
A7: x = i / 2 by A1, A5, Def1;
A8: 0 <= i by NAT_1:2;
( i <= 1 or i = 1 + 1 ) by A6, NAT_1:8;
then ( i = 0 or i = 0 + 1 or i = 2 ) by A8, NAT_1:9;
hence x in {0,(1 / 2),1} by A7, ENUMSET1:def_1; ::_thesis: verum
end;
hence ( x in dyadic 1 iff x in {0,(1 / 2),1} ) by A2; ::_thesis: verum
end;
hence dyadic 1 = {0,(1 / 2),1} by TARSKI:1; ::_thesis: verum
end;
registration
let n be Nat;
cluster dyadic n -> non empty ;
coherence
not dyadic n is empty
proof
set x = 0 / (2 |^ n);
ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & 0 / (2 |^ n) = i / (2 |^ n) )
proof
take 0 ; ::_thesis: ( 0 <= 0 & 0 <= 2 |^ n & 0 / (2 |^ n) = 0 / (2 |^ n) )
thus ( 0 <= 0 & 0 <= 2 |^ n & 0 / (2 |^ n) = 0 / (2 |^ n) ) by NEWTON:83; ::_thesis: verum
end;
hence not dyadic n is empty by Def1; ::_thesis: verum
end;
end;
definition
let n be Nat;
func dyad n -> FinSequence means :Def4: :: URYSOHN1:def 4
( dom it = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom it holds
it . i = (i - 1) / (2 |^ n) ) );
existence
ex b1 being FinSequence st
( dom b1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b1 holds
b1 . i = (i - 1) / (2 |^ n) ) )
proof
deffunc H1( Nat) -> Element of REAL = ($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 = H1(i) ) ) from FINSEQ_1:sch_2();
take FS ; ::_thesis: ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom FS holds
FS . i = (i - 1) / (2 |^ n) ) )
thus ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom FS holds
FS . i = (i - 1) / (2 |^ n) ) ) by A1, FINSEQ_1:def_3; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence st dom b1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b1 holds
b1 . i = (i - 1) / (2 |^ n) ) & dom b2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b2 holds
b2 . i = (i - 1) / (2 |^ n) ) holds
b1 = b2
proof
let F1, F2 be FinSequence; ::_thesis: ( dom F1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom F1 holds
F1 . i = (i - 1) / (2 |^ n) ) & dom F2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom F2 holds
F2 . i = (i - 1) / (2 |^ n) ) implies F1 = F2 )
assume that
A2: dom F1 = Seg ((2 |^ n) + 1) and
A3: for i being Element of 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 Element of NAT st i in dom F2 holds
F2 . i = (i - 1) / (2 |^ n) ; ::_thesis: F1 = F2
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; ::_thesis: ( k in X implies F1 . k = F2 . k )
assume A7: k in X ; ::_thesis: F1 . k = F2 . k
hence F1 . k = (k - 1) / (2 |^ n) by A3, A6
.= F2 . k by A2, A4, A5, A6, A7 ;
::_thesis: verum
end;
hence F1 = F2 by A2, A4, A6, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines dyad URYSOHN1:def_4_:_
for n being Nat
for b2 being FinSequence holds
( b2 = dyad n iff ( dom b2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b2 holds
b2 . i = (i - 1) / (2 |^ n) ) ) );
theorem :: URYSOHN1:4
for n being Element of NAT holds
( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n )
proof
let n be Element of NAT ; ::_thesis: ( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n )
A1: dom (dyad n) = Seg ((2 |^ n) + 1) by Def4;
for x being set holds
( x in rng (dyad n) iff x in dyadic n )
proof
let x be set ; ::_thesis: ( x in rng (dyad n) iff x in dyadic n )
A2: ( x in rng (dyad n) implies x in dyadic n )
proof
assume x in rng (dyad n) ; ::_thesis: x in dyadic n
then consider y being set 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 = y as Element of 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 x in dyadic n by A7, A8, Def1; ::_thesis: verum
end;
( x in dyadic n implies x in rng (dyad n) )
proof
assume A9: x in dyadic n ; ::_thesis: x in rng (dyad n)
then reconsider x = x as Real ;
consider i being Element of NAT such that
A10: i <= 2 |^ n and
A11: x = i / (2 |^ n) by A9, Def1;
consider y being Element of NAT such that
A12: y = i + 1 ;
0 <= i by NAT_1:2;
then ( 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 x in rng (dyad n) by A14, FUNCT_1:def_3; ::_thesis: verum
end;
hence ( x in rng (dyad n) iff x in dyadic n ) by A2; ::_thesis: verum
end;
hence ( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n ) by Def4, TARSKI:1; ::_thesis: verum
end;
registration
cluster DYADIC -> non empty ;
coherence
not DYADIC is empty
proof
ex x being set st x in dyadic 0 by XBOOLE_0:def_1;
hence not DYADIC is empty by Def2; ::_thesis: verum
end;
end;
registration
cluster DOM -> non empty ;
coherence
not DOM is empty ;
end;
theorem Th5: :: URYSOHN1:5
for n being Element of NAT holds dyadic n c= dyadic (n + 1)
proof
let n be Element of NAT ; ::_thesis: dyadic n c= dyadic (n + 1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dyadic n or x in dyadic (n + 1) )
assume A1: x in dyadic n ; ::_thesis: x in dyadic (n + 1)
ex i being Element of NAT st
( i <= 2 |^ (n + 1) & x = i / (2 |^ (n + 1)) )
proof
reconsider x = x as Real by A1;
consider i being Element of NAT such that
A2: ( i <= 2 |^ n & x = i / (2 |^ n) ) by A1, Def1;
take i * 2 ; ::_thesis: ( i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) )
2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:6;
hence ( i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) ) by A2, XCMPLX_1:91, XREAL_1:64; ::_thesis: verum
end;
hence x in dyadic (n + 1) by Def1; ::_thesis: verum
end;
theorem Th6: :: URYSOHN1:6
for n being Element of NAT holds
( 0 in dyadic n & 1 in dyadic n )
proof
defpred S1[ Element of NAT ] means ( 0 in dyadic $1 & 1 in dyadic $1 );
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: ( 0 in dyadic k & 1 in dyadic k ) ; ::_thesis: S1[k + 1]
dyadic k c= dyadic (k + 1) by Th5;
hence S1[k + 1] by A2; ::_thesis: verum
end;
A3: S1[ 0 ] by Th2, TARSKI:def_2;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1);
hence for n being Element of NAT holds
( 0 in dyadic n & 1 in dyadic n ) ; ::_thesis: verum
end;
theorem Th7: :: URYSOHN1:7
for n, i being Element of 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 Element of NAT ; ::_thesis: ( 0 < i & i <= 2 |^ n implies ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) )
assume that
A1: 0 < i and
A2: i <= 2 |^ n ; ::_thesis: ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
A3: 0 * 2 < i * 2 by A1, XREAL_1:68;
then consider k being Nat such that
A4: i * 2 = k + 1 by NAT_1:6;
A5: not ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic n
proof
assume ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic n ; ::_thesis: contradiction
then consider s being Element of NAT such that
s <= 2 |^ n and
A6: ((i * 2) - 1) / (2 |^ (n + 1)) = s / (2 |^ n) by Def1;
A7: 2 |^ n <> 0 by NEWTON:83;
2 |^ (n + 1) <> 0 by NEWTON:83;
then ((i * 2) - 1) * (2 |^ n) = s * (2 |^ (n + 1)) by A6, A7, 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 A7, XCMPLX_1:94;
then (i * 2) + (- 1) = s * 2 by A7, XCMPLX_1:53;
then (2 * i) + 0 = (2 * s) + 1 ;
hence contradiction by NAT_1:18; ::_thesis: verum
end;
i * 2 <= (2 |^ n) * 2 by A2, XREAL_1:64;
then i * 2 <= 2 |^ (n + 1) by NEWTON:6;
then A8: k <= 2 |^ (n + 1) by A4, NAT_1:13;
( k in NAT & 0 <= k ) by A3, A4, NAT_1:13, ORDINAL1:def_12;
then ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic (n + 1) by A4, A8, Def1;
hence ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th8: :: URYSOHN1:8
for n, i being Element of 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 Element of NAT ; ::_thesis: ( 0 <= i & i < 2 |^ n implies ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) )
assume that
A1: 0 <= i and
A2: i < 2 |^ n ; ::_thesis: ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
A3: 0 + 1 <= i + 1 by A1, XREAL_1:6;
consider s being Element of NAT such that
A4: s = i + 1 ;
A5: (s * 2) - 1 = (i * 2) + (1 + 0) by A4;
s <= 2 |^ n by A2, A4, NAT_1:13;
hence ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by A3, A5, Th7; ::_thesis: verum
end;
theorem Th9: :: URYSOHN1:9
for n being Element of NAT holds 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
proof
let n be Element of NAT ; ::_thesis: 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
( (2 * 0) + 1 = 1 & 0 < 2 |^ n ) by NEWTON:83;
hence 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by Th8; ::_thesis: verum
end;
definition
let n be Nat;
let x be Element of dyadic n;
func axis x -> Element of NAT means :Def5: :: URYSOHN1:def 5
x = it / (2 |^ n);
existence
ex b1 being Element of NAT st x = b1 / (2 |^ n)
proof
consider i being Element of NAT such that
i <= 2 |^ n and
A1: x = i / (2 |^ n) by Def1;
take i ; ::_thesis: x = i / (2 |^ n)
thus x = i / (2 |^ n) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of NAT st x = b1 / (2 |^ n) & x = b2 / (2 |^ n) holds
b1 = b2
proof
let i1, i2 be Element of NAT ; ::_thesis: ( x = i1 / (2 |^ n) & x = i2 / (2 |^ n) implies i1 = i2 )
assume A2: ( x = i1 / (2 |^ n) & x = i2 / (2 |^ n) ) ; ::_thesis: i1 = i2
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 i1 = i2 ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines axis URYSOHN1:def_5_:_
for n being Nat
for x being Element of dyadic n
for b3 being Element of NAT holds
( b3 = axis x iff x = b3 / (2 |^ n) );
theorem Th10: :: URYSOHN1:10
for n being Element of NAT
for x being Element of dyadic n holds
( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )
proof
let n be Element of NAT ; ::_thesis: for x being Element of dyadic n holds
( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )
let x be Element of dyadic n; ::_thesis: ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )
ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) by Def1;
hence ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) by Def5; ::_thesis: verum
end;
theorem :: URYSOHN1:11
for n being Element of NAT
for x being Element of dyadic n holds
( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) )
proof
let n be Element of NAT ; ::_thesis: for x being Element of dyadic n holds
( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) )
let x be Element of dyadic n; ::_thesis: ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ 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 ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) ) by A1, XREAL_1:74; ::_thesis: verum
end;
theorem Th12: :: URYSOHN1:12
for n being Element of NAT
for x being Element of dyadic n holds ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n)
proof
let n be Element of NAT ; ::_thesis: for x being Element of dyadic n holds ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n)
let x be Element of dyadic n; ::_thesis: ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n)
( (- 1) + (axis x) < 1 + (axis x) & 0 < 2 |^ n ) by NEWTON:83, XREAL_1:8;
hence ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n) by XREAL_1:74; ::_thesis: verum
end;
theorem Th13: :: URYSOHN1:13
for n being Element of NAT
for x being Element of dyadic (n + 1) st not x in dyadic n holds
( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n )
proof
let n be Element of NAT ; ::_thesis: for x being Element of dyadic (n + 1) st not x in dyadic n holds
( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n )
let x be Element of dyadic (n + 1); ::_thesis: ( not x in dyadic n implies ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) )
assume A1: not x in dyadic n ; ::_thesis: ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n )
thus ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n ::_thesis: ((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 Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) )
proof
consider s being Element of 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__::_thesis:_(_(_s_=_k_*_2_&_ex_i_being_Element_of_NAT_st_
(_i_<=_2_|^_n_&_a_=_i_/_(2_|^_n)_)_)_or_(_s_=_(k_*_2)_+_1_&_ex_k,_i_being_Element_of_NAT_st_
(_i_<=_2_|^_n_&_a_=_i_/_(2_|^_n)_)_)_)
percases ( s = k * 2 or s = (k * 2) + 1 ) by A5;
caseA6: s = k * 2 ; ::_thesis: ex i being Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) )
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 ex i being Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) ) by A1, A7, Def1; ::_thesis: verum
end;
caseA8: s = (k * 2) + 1 ; ::_thesis: ex k, i being Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) )
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 = k; ::_thesis: ex i being Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) )
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 ex i being Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) ) by A10; ::_thesis: verum
end;
end;
end;
hence ex i being Element of NAT st
( i <= 2 |^ n & a = i / (2 |^ n) ) ; ::_thesis: verum
end;
hence ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n by A2, Def1; ::_thesis: verum
end;
thus ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ::_thesis: verum
proof
set a = ((axis x) + 1) / (2 |^ (n + 1));
ex i being Element of NAT st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )
proof
consider s being Element of 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__::_thesis:_(_(_s_=_k_*_2_&_ex_i_being_Element_of_NAT_st_
(_i_<=_2_|^_n_&_((axis_x)_+_1)_/_(2_|^_(n_+_1))_=_i_/_(2_|^_n)_)_)_or_(_s_=_(k_*_2)_+_1_&_ex_l,_i_being_Element_of_NAT_st_
(_i_<=_2_|^_n_&_((axis_x)_+_1)_/_(2_|^_(n_+_1))_=_i_/_(2_|^_n)_)_)_)
percases ( s = k * 2 or s = (k * 2) + 1 ) by A13;
caseA14: s = k * 2 ; ::_thesis: ex i being Element of NAT st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )
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 ex i being Element of NAT st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) by A1, A15, Def1; ::_thesis: verum
end;
caseA16: s = (k * 2) + 1 ; ::_thesis: ex l, i being Element of NAT st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )
consider l being Element of 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) ; ::_thesis: contradiction
then x = 1 by A12, A18, XCMPLX_1:60;
hence contradiction by A1, Th6; ::_thesis: verum
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 = l; ::_thesis: ex i being Element of NAT st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )
((axis x) + 1) / (2 |^ (n + 1)) = (((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 ex i being Element of NAT st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) by A19; ::_thesis: verum
end;
end;
end;
hence ex i being Element of NAT st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) ; ::_thesis: verum
end;
hence ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n by Def1; ::_thesis: verum
end;
end;
theorem Th14: :: URYSOHN1:14
for n being Element of NAT
for x1, x2 being Element of dyadic n st x1 < x2 holds
axis x1 < axis x2
proof
let n be Element of NAT ; ::_thesis: for x1, x2 being Element of dyadic n st x1 < x2 holds
axis x1 < axis x2
let x1, x2 be Element of dyadic n; ::_thesis: ( x1 < x2 implies axis x1 < axis x2 )
A1: 0 < 2 |^ n by NEWTON:83;
( x1 = (axis x1) / (2 |^ n) & x2 = (axis x2) / (2 |^ n) ) by Th10;
hence ( x1 < x2 implies axis x1 < axis x2 ) by A1, XREAL_1:72; ::_thesis: verum
end;
theorem Th15: :: URYSOHN1:15
for n being Element of NAT
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 Element of NAT ; ::_thesis: for x1, x2 being Element of dyadic n st x1 < x2 holds
( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 )
let x1, x2 be Element of dyadic n; ::_thesis: ( x1 < x2 implies ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) )
assume A1: x1 < x2 ; ::_thesis: ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= 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;
0 < 2 |^ n by NEWTON:83;
then A4: ((axis x1) + 1) / (2 |^ n) <= (axis x2) / (2 |^ n) by A2, XREAL_1:72;
0 < 2 |^ n by NEWTON:83;
then (axis x1) / (2 |^ n) <= ((axis x2) - 1) / (2 |^ n) by A3, XREAL_1:72;
hence ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) by A4, Th10; ::_thesis: verum
end;
theorem Th16: :: URYSOHN1:16
for n being Element of NAT
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 Element of NAT ; ::_thesis: 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))
let x1, x2 be Element of dyadic (n + 1); ::_thesis: ( x1 < x2 & not x1 in dyadic n & not x2 in dyadic n implies ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) )
assume that
A1: x1 < x2 and
A2: not x1 in dyadic n and
A3: not x2 in dyadic n ; ::_thesis: ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1))
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 ; ::_thesis: contradiction
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 contradiction by A3, A7, Def1; ::_thesis: verum
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 ; ::_thesis: contradiction
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 contradiction by A2, A11, Def1; ::_thesis: verum
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 ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) by A8, A4, A9, A5, XREAL_1:72; ::_thesis: verum
end;
begin
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 a_neighborhood of x means :: URYSOHN1:def 6
ex A being Subset of T st
( A is open & x in A & A c= it );
compatibility
for b1 being Element of bool the carrier of T holds
( b1 is Nbhd of x,T iff ex A being Subset of T st
( A is open & x in A & A c= b1 ) )
proof
let S be Subset of T; ::_thesis: ( S is Nbhd of x,T iff ex A being Subset of T st
( A is open & x in A & A c= S ) )
hereby ::_thesis: ( ex A being Subset of T st
( A is open & x in A & A c= S ) implies S is Nbhd of x,T )
assume A1: S is a_neighborhood of x ; ::_thesis: ex N being Element of bool the carrier of T st
( N is open & x in N & N c= S )
take N = Int S; ::_thesis: ( N is open & x in N & N c= S )
thus N is open ; ::_thesis: ( x in N & N c= S )
thus x in N by A1, CONNSP_2:def_1; ::_thesis: N c= S
thus N c= S by TOPS_1:16; ::_thesis: verum
end;
assume ex A being Subset of T st
( A is open & x in A & A c= S ) ; ::_thesis: S is Nbhd of x,T
hence x in Int S by TOPS_1:22; :: according to CONNSP_2:def_1 ::_thesis: verum
end;
end;
:: deftheorem defines Nbhd URYSOHN1:def_6_:_
for T being non empty TopSpace
for x being Point of T
for b3 being Element of bool the carrier of T holds
( b3 is Nbhd of x,T iff ex A being Subset of T st
( A is open & x in A & A c= b3 ) );
theorem Th17: :: 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 st x in A holds
ex B being Nbhd of x,T st B c= A )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds
( A is open iff for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A )
let A be Subset of T; ::_thesis: ( A is open iff for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A )
thus ( A is open implies for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A ) ::_thesis: ( ( for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A ) implies A is open )
proof
assume A1: A is open ; ::_thesis: for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A
let x be Point of T; ::_thesis: ( x in A implies ex B being Nbhd of x,T st B c= A )
assume x in A ; ::_thesis: ex B being Nbhd of x,T st B c= A
then ex B being Subset of T st
( B is a_neighborhood of x & B c= A ) by A1, CONNSP_2:7;
hence ex B being Nbhd of x,T st B c= A ; ::_thesis: verum
end;
assume A2: for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A ; ::_thesis: A is open
for x being Point of T st x in A holds
ex B being Subset of T st
( B is a_neighborhood of x & B c= A )
proof
let x be Point of T; ::_thesis: ( x in A implies ex B being Subset of T st
( B is a_neighborhood of x & B c= A ) )
assume x in A ; ::_thesis: ex B being Subset of T st
( B is a_neighborhood of x & B c= A )
then ex B being Nbhd of x,T st B c= A by A2;
hence ex B being Subset of T st
( B is a_neighborhood of x & B c= A ) ; ::_thesis: verum
end;
hence A is open by CONNSP_2:7; ::_thesis: verum
end;
theorem :: URYSOHN1:18
for T being non empty TopSpace
for A being Subset of T st ( for x being Point of T st x in A holds
A is Nbhd of x,T ) holds
A is open
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st ( for x being Point of T st x in A holds
A is Nbhd of x,T ) holds
A is open
let A be Subset of T; ::_thesis: ( ( for x being Point of T st x in A holds
A is Nbhd of x,T ) implies A is open )
assume A1: for x being Point of T st x in A holds
A is Nbhd of x,T ; ::_thesis: A is open
for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A
proof
let x be Point of T; ::_thesis: ( x in A implies ex B being Nbhd of x,T st B c= A )
assume A2: x in A ; ::_thesis: ex B being Nbhd of x,T st B c= 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 ; ::_thesis: B c= A
thus B c= A by A3; ::_thesis: verum
end;
hence ex B being Nbhd of x,T st B c= A ; ::_thesis: verum
end;
hence A is open by Th17; ::_thesis: verum
end;
definition
let T be TopSpace;
redefine attr T is T_1 means :Def7: :: URYSOHN1:def 7
for p, q being Point of T st not p = q holds
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
( T is T_1 iff for p, q being Point of T st not p = q holds
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
thus ( T is T_1 implies for p, q being Point of T st not p = q holds
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 ) ) ::_thesis: ( ( for p, q being Point of T st not p = q holds
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 ) ) implies T is T_1 )
proof
assume A1: T is T_1 ; ::_thesis: for p, q being Point of T st not p = q holds
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 be Point of T; ::_thesis: ( not p = q implies 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 ) )
assume A2: not p = q ; ::_thesis: 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 )
consider G1 being Subset of T such that
A3: ( G1 is open & p in G1 & q in G1 ` ) by A1, A2, PRE_TOPC:def_9;
consider G2 being Subset of T such that
A4: ( G2 is open & q in G2 & p in G2 ` ) by A1, A2, PRE_TOPC:def_9;
take G1 ; ::_thesis: ex V being Subset of T st
( G1 is open & V is open & p in G1 & not q in G1 & q in V & not p in V )
take G2 ; ::_thesis: ( G1 is open & G2 is open & p in G1 & not q in G1 & q in G2 & not p in G2 )
thus ( G1 is open & G2 is open & p in G1 & not q in G1 & q in G2 & not p in G2 ) by A3, A4, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A5: for p, q being Point of T st not p = q holds
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 ) ; ::_thesis: T is T_1
let p, q be Point of T; :: according to PRE_TOPC:def_9 ::_thesis: ( p = q or ex b1 being Element of bool the carrier of T st
( b1 is open & p in b1 & q in b1 ` ) )
assume p <> q ; ::_thesis: ex b1 being Element of bool the carrier of T st
( b1 is open & p in b1 & q in b1 ` )
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 ; ::_thesis: ( W is open & p in W & q in W ` )
thus ( W is open & p in W & q in W ` ) by A6, A7, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines T_1 URYSOHN1:def_7_:_
for T being TopSpace holds
( T is T_1 iff for p, q being Point of T st not p = q holds
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 ) );
theorem Th19: :: URYSOHN1:19
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; ::_thesis: ( T is T_1 iff for p being Point of T holds {p} is closed )
thus ( T is T_1 implies for p being Point of T holds {p} is closed ) ::_thesis: ( ( for p being Point of T holds {p} is closed ) implies T is T_1 )
proof
assume A1: T is T_1 ; ::_thesis: for p being Point of T holds {p} is closed
for p being Point of T holds {p} is closed
proof
let p be Point of T; ::_thesis: {p} is closed
consider B being Subset of T such that
A2: B = {p} ` ;
defpred S1[ 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 S1[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; ::_thesis: ( C in F iff ex q being Point of T st
( q in B & C is open & q in C & not p in C ) )
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 ) ; ::_thesis: C in F
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 ; ::_thesis: ( q in B & ( for V being Subset of T st C = V holds
( V is open & q in V & not p in V ) ) )
thus ( q in B & ( for V being Subset of T st C = V holds
( V is open & q in V & not p in V ) ) ) by A7; ::_thesis: verum
end;
hence C in F by A3; ::_thesis: verum
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 ; ::_thesis: ex q being Point of T st
( q in B & C is open & q in C & not p in C )
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 ; ::_thesis: ( q in B & C is open & q in C & not p in C )
thus ( q in B & C is open & q in C & not p in C ) by A8; ::_thesis: verum
end;
hence ( C in F iff ex q being Point of T st
( q in B & C is open & q in C & not p in C ) ) by A5; ::_thesis: verum
end;
for x being set st x in F holds
x in the topology of T
proof
let x be set ; ::_thesis: ( x in F implies x in the topology of T )
assume A9: x in F ; ::_thesis: x in the topology of T
then reconsider x = 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 x in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
then A10: F c= the topology of T by TARSKI:def_3;
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; ::_thesis: ( q in B implies ex V being Subset of T st
( V is open & q in V & not p in V ) )
assume q in B ; ::_thesis: ex V being Subset of T st
( V is open & q in V & not p in V )
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, Def7;
then consider V being Subset of T such that
A12: ( V is open & q in V & not p in V ) ;
take V ; ::_thesis: ( V is open & q in V & not p in V )
thus ( V is open & q in V & not p in V ) by A12; ::_thesis: verum
end;
for x being set st x in B holds
x in union F
proof
let x be set ; ::_thesis: ( x in B implies x in union F )
assume A13: x in B ; ::_thesis: x in union F
then reconsider x = 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 )
proof
take C ; ::_thesis: ( x in C & C in F )
thus ( x in C & C in F ) by A4, A13, A14; ::_thesis: verum
end;
hence x in union F by TARSKI:def_4; ::_thesis: verum
end;
then A15: B c= union F by TARSKI:def_3;
for x being set st x in union F holds
x in B
proof
let x be set ; ::_thesis: ( x in union F implies x in B )
assume x in union F ; ::_thesis: x in B
then consider C being set such that
A16: x in C and
A17: C in F by TARSKI:def_4;
reconsider C = 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 x in B by A2, A16; ::_thesis: verum
end;
then union F c= B by TARSKI:def_3;
then B = union F by A15, XBOOLE_0:def_10;
then B in the topology of T by A10, PRE_TOPC:def_1;
then ( {p} ` = ([#] T) \ {p} & B is open ) by PRE_TOPC:def_2;
hence {p} is closed by A2, PRE_TOPC:def_3; ::_thesis: verum
end;
hence for p being Point of T holds {p} is closed ; ::_thesis: verum
end;
assume A18: for p being Point of T holds {p} is closed ; ::_thesis: T is T_1
for p, q being Point of T st not p = q holds
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; ::_thesis: ( not p = q implies 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 ) )
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 ; ::_thesis: 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 )
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 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 ) by A19, A20, A23, A24, A25, A21; ::_thesis: verum
end;
hence T is T_1 by Def7; ::_thesis: verum
end;
theorem Th20: :: 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 )
proof
let T be non empty TopSpace; ::_thesis: ( T is normal implies 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 ) )
assume A1: T is normal ; ::_thesis: 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 )
let A, B be open Subset of T; ::_thesis: ( A <> {} & Cl A c= B implies ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) )
assume that
A2: A <> {} and
A3: Cl A c= B ; ::_thesis: ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )
now__::_thesis:_(_(_B_<>_[#]_T_&_ex_C,_C_being_Subset_of_T_st_
(_C_<>_{}_&_C_is_open_&_Cl_A_c=_C_&_Cl_C_c=_B_)_)_or_(_B_=_[#]_T_&_ex_C,_C_being_Subset_of_T_st_
(_C_<>_{}_&_C_is_open_&_Cl_A_c=_C_&_Cl_C_c=_B_)_)_)
percases ( B <> [#] T or B = [#] T ) ;
caseA4: B <> [#] T ; ::_thesis: ex C, C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )
reconsider W = Cl A, V = ([#] T) \ B as Subset of T ;
A5: ( W <> {} & V <> {} )
proof
A6: ([#] T) \ B <> {}
proof
assume ([#] T) \ B = {} ; ::_thesis: contradiction
then B = ([#] T) \ {} by PRE_TOPC:3;
hence contradiction by A4; ::_thesis: verum
end;
A c= Cl A by PRE_TOPC:18;
hence ( W <> {} & V <> {} ) by A2, A6; ::_thesis: verum
end;
A7: W misses V
proof
assume W meets V ; ::_thesis: contradiction
then consider x being set 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 contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
B = ([#] T) \ V by PRE_TOPC:3;
then V is closed by PRE_TOPC:def_3;
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, A5, A7, COMPTS_1:def_3;
take C = C; ::_thesis: ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )
( 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 ( C <> {} & Cl A c= C & Cl C c= B ) by A5, A11, A15, SUBSET_1:23; ::_thesis: verum
end;
hence ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A9; ::_thesis: verum
end;
caseA16: B = [#] T ; ::_thesis: ex C, C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )
consider C being Subset of T such that
A17: C = [#] T ;
take C = C; ::_thesis: ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )
Cl C c= B by A16;
hence ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A17; ::_thesis: verum
end;
end;
end;
hence ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) ; ::_thesis: verum
end;
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 ) )
proof
let T be non empty TopSpace; ::_thesis: ( 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 ) )
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 ) ) ::_thesis: ( ( 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 ) ) implies T is regular )
proof
assume A1: T is regular ; ::_thesis: 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 )
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 ) ::_thesis: verum
proof
let A be open Subset of T; ::_thesis: 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 )
let p be Point of T; ::_thesis: ( p in A implies ex B being open Subset of T st
( p in B & Cl B c= A ) )
assume A2: p in A ; ::_thesis: ex B being open Subset of T st
( p in B & Cl B c= A )
then A3: p in (A `) ` ;
thus ex B being open Subset of T st
( p in B & Cl B c= A ) ::_thesis: verum
proof
reconsider P = A ` as Subset of T ;
now__::_thesis:_(_(_P_<>_{}_&_ex_W_being_Subset_of_T_ex_B_being_open_Subset_of_T_st_
(_p_in_B_&_Cl_B_c=_A_)_)_or_(_P_=_{}_&_ex_A,_B_being_open_Subset_of_T_st_
(_p_in_B_&_Cl_B_c=_A_)_)_)
percases ( P <> {} or P = {} ) ;
case P <> {} ; ::_thesis: ex W being Subset of T ex B being open Subset of T st
( p in B & Cl B c= A )
then 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, COMPTS_1:def_2;
W /\ V = {} by A8, XBOOLE_0:def_7;
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 by XBOOLE_0:def_7;
then A9: P misses Cl W by A7, XBOOLE_1:63;
take W = W; ::_thesis: ex B being open Subset of T st
( p in B & Cl B c= A )
(A `) ` = A ;
then Cl W c= A by A9, SUBSET_1:23;
hence ex B being open Subset of T st
( p in B & Cl B c= A ) by A4, A6; ::_thesis: verum
end;
caseA10: P = {} ; ::_thesis: ex A, B being open Subset of T st
( p in B & Cl B c= A )
take A = A; ::_thesis: ex B being open Subset of T st
( p in B & Cl B c= A )
A = [#] T by A10, PRE_TOPC:4;
then Cl A c= A ;
hence ex B being open Subset of T st
( p in B & Cl B c= A ) by A2; ::_thesis: verum
end;
end;
end;
hence ex B being open Subset of T st
( p in B & Cl B c= A ) ; ::_thesis: verum
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 ) ; ::_thesis: T is regular
for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
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; ::_thesis: for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V )
let P be Subset of T; ::_thesis: ( P <> {} & P is closed & p in P ` implies ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) )
assume that
P <> {} and
A12: ( P is closed & p in P ` ) ; ::_thesis: ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V )
thus ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) ::_thesis: verum
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 = B, C = 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 ; ::_thesis: ex V being Subset of T st
( B is open & V is open & p in B & P c= V & B misses V )
take C ; ::_thesis: ( B is open & C is open & p in B & P c= C & B misses C )
( (Cl B) ` is open & (P `) ` = P ) ;
hence ( B is open & C is open & p in B & P c= C & B misses C ) by A13, A14, A15, A16, XBOOLE_1:34; ::_thesis: verum
end;
end;
hence T is regular by COMPTS_1:def_2; ::_thesis: verum
end;
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 )
proof
let T be non empty TopSpace; ::_thesis: ( T is normal & T is T_1 implies for A being open Subset of T st A <> {} holds
ex B being Subset of T st
( B <> {} & Cl B c= A ) )
assume that
A1: T is normal and
A2: T is T_1 ; ::_thesis: for A being open Subset of T st A <> {} holds
ex B being Subset of T st
( B <> {} & Cl B c= A )
let A be open Subset of T; ::_thesis: ( A <> {} implies ex B being Subset of T st
( B <> {} & Cl B c= A ) )
assume A3: A <> {} ; ::_thesis: ex B being Subset of T st
( B <> {} & Cl B c= A )
now__::_thesis:_(_(_A_<>_[#]_T_&_ex_B,_B_being_Subset_of_T_st_
(_B_<>_{}_&_Cl_B_c=_A_)_)_or_(_A_=_[#]_T_&_ex_B,_B_being_Subset_of_T_st_
(_B_<>_{}_&_Cl_B_c=_A_)_)_)
percases ( A <> [#] T or A = [#] T ) ;
caseA4: A <> [#] T ; ::_thesis: ex B, B being Subset of T st
( B <> {} & Cl B c= A )
A5: ([#] T) \ A <> {}
proof
assume ([#] T) \ A = {} ; ::_thesis: contradiction
then A = ([#] T) \ {} by PRE_TOPC:3;
hence contradiction by A4; ::_thesis: verum
end;
reconsider V = ([#] T) \ A as Subset of T ;
consider x being set such that
A6: x in A by A3, XBOOLE_0:def_1;
A = ([#] T) \ V by PRE_TOPC:3;
then A7: V is closed by PRE_TOPC:def_3;
reconsider x = x as Point of T by A6;
consider W being set such that
A8: W = {x} ;
reconsider W = W as Subset of T by A8;
A9: W misses V
proof
assume W meets V ; ::_thesis: contradiction
then consider z being set such that
A10: z in W /\ V by XBOOLE_0:4;
z in W by A10, XBOOLE_0:def_4;
then A11: z in A by A6, A8, TARSKI:def_1;
z in V by A10, XBOOLE_0:def_4;
hence contradiction by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
W is closed by A2, A8, Th19;
then consider B, Q being Subset of T such that
B is open and
A12: Q is open and
A13: W c= B and
A14: V c= Q and
A15: B misses Q by A1, A8, A7, A5, A9, COMPTS_1:def_3;
take B = B; ::_thesis: ex B being Subset of T st
( B <> {} & Cl B c= A )
( B <> {} & Cl B c= A )
proof
B c= Q ` by A15, SUBSET_1:23;
then Cl B c= Q ` by A12, TOPS_1:5;
then Cl B misses Q by SUBSET_1:23;
then A16: V misses Cl B by A14, XBOOLE_1:63;
(A `) ` = A ;
hence ( B <> {} & Cl B c= A ) by A8, A13, A16, SUBSET_1:23; ::_thesis: verum
end;
hence ex B being Subset of T st
( B <> {} & Cl B c= A ) ; ::_thesis: verum
end;
caseA17: A = [#] T ; ::_thesis: ex B, B being Subset of T st
( B <> {} & Cl B c= A )
consider B being Subset of T such that
A18: B = [#] T ;
take B = B; ::_thesis: ex B being Subset of T st
( B <> {} & Cl B c= A )
Cl B c= A by A17;
hence ex B being Subset of T st
( B <> {} & Cl B c= A ) by A18; ::_thesis: verum
end;
end;
end;
hence ex B being Subset of T st
( B <> {} & Cl B c= A ) ; ::_thesis: verum
end;
theorem :: URYSOHN1:23
for T being non empty TopSpace st T is normal holds
for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds
ex C being Subset of T st
( C is open & B c= C & Cl C c= A )
proof
let T be non empty TopSpace; ::_thesis: ( T is normal implies for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds
ex C being Subset of T st
( C is open & B c= C & Cl C c= A ) )
assume A1: T is normal ; ::_thesis: for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds
ex C being Subset of T st
( C is open & B c= C & Cl C c= A )
let A, B be Subset of T; ::_thesis: ( A is open & B is closed & B <> {} & B c= A implies ex C being Subset of T st
( C is open & B c= C & Cl C c= A ) )
assume that
A2: A is open and
A3: ( B is closed & B <> {} ) and
A4: B c= A ; ::_thesis: ex C being Subset of T st
( C is open & B c= C & Cl C c= A )
percases ( A <> [#] T or A = [#] T ) ;
supposeA5: A <> [#] T ; ::_thesis: ex C being Subset of T st
( C is open & B c= C & Cl C c= A )
reconsider V = ([#] T) \ A as Subset of T ;
A6: A = ([#] T) \ V by PRE_TOPC:3;
then A7: ([#] T) \ A <> {} by A5;
A8: B misses V
proof
assume B /\ V <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider z being set such that
A9: z in B /\ V by XBOOLE_0:def_1;
( z in B & z in V ) by A9, XBOOLE_0:def_4;
hence contradiction by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
V is closed by A2, A6, PRE_TOPC:def_3;
then consider C, Q being Subset of T such that
A10: C is open and
A11: Q is open and
A12: B c= C and
A13: V c= Q and
A14: C misses Q by A1, A3, A7, A8, COMPTS_1:def_3;
C c= Q ` by A14, SUBSET_1:23;
then Cl C c= Q ` by A11, TOPS_1:5;
then Q misses Cl C by SUBSET_1:23;
then A15: V misses Cl C by A13, XBOOLE_1:63;
take C ; ::_thesis: ( C is open & B c= C & Cl C c= A )
thus ( C is open & B c= C ) by A10, A12; ::_thesis: Cl C c= A
(A `) ` = A ;
hence Cl C c= A by A15, SUBSET_1:23; ::_thesis: verum
end;
supposeA16: A = [#] T ; ::_thesis: ex C being Subset of T st
( C is open & B c= C & Cl C c= A )
take [#] T ; ::_thesis: ( [#] T is open & B c= [#] T & Cl ([#] T) c= A )
thus ( [#] T is open & B c= [#] T & Cl ([#] T) c= A ) by A16; ::_thesis: verum
end;
end;
end;
begin
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: :: URYSOHN1:def 8
( it <> {} & it is open & Cl A c= it & Cl it c= B );
existence
ex b1 being Subset of T st
( b1 <> {} & b1 is open & Cl A c= b1 & Cl b1 c= B ) by A1, Th20;
end;
:: deftheorem Def8 defines Between URYSOHN1:def_8_:_
for T being non empty TopSpace
for A, B being Subset of T st T is normal & A <> {} & A is open & B is open & Cl A c= B holds
for b4 being Subset of T holds
( b4 is Between of A,B iff ( b4 <> {} & b4 is open & Cl A c= b4 & Cl b4 c= B ) );
theorem :: URYSOHN1:24
for T being non empty TopSpace st T is normal holds
for A, B being closed Subset of T st A <> {} holds
for n being Element of 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 ) ) holds
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; ::_thesis: ( T is normal implies for A, B being closed Subset of T st A <> {} holds
for n being Element of 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 ) ) holds
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 ) ) ) ) )
assume A1: T is normal ; ::_thesis: for A, B being closed Subset of T st A <> {} holds
for n being Element of 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 ) ) holds
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 ) ) ) )
let A, B be closed Subset of T; ::_thesis: ( A <> {} implies for n being Element of 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 ) ) holds
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 ) ) ) ) )
assume A2: A <> {} ; ::_thesis: for n being Element of 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 ) ) holds
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 ) ) ) )
let n be Element of NAT ; ::_thesis: 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 ) ) holds
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 ) ) ) )
let G be Function of (dyadic n),(bool the carrier of T); ::_thesis: ( 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 ) ) implies 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 ) ) ) ) )
assume 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 ) ; ::_thesis: 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 ) ) ) )
A6: for r being Element of dyadic n holds G . r <> {}
proof
let r be Element of dyadic n; ::_thesis: G . r <> {}
percases ( 0 = r or 0 < r ) by Th1;
suppose 0 = r ; ::_thesis: G . r <> {}
hence G . r <> {} by A2, A3; ::_thesis: verum
end;
supposeA7: 0 < r ; ::_thesis: G . 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 G . r <> {} by A2, A3; ::_thesis: verum
end;
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 S1[ 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 S1[x,y]
proof
let x be Element of S; ::_thesis: ex y being Subset of T st S1[x,y]
A10: not x in dyadic n by XBOOLE_0:def_5;
reconsider x = 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 ; ::_thesis: S1[x, the Between of G . q1,G . q2]
thus S1[x, the Between of G . q1,G . q2] by A11; ::_thesis: verum
end;
consider D being Function of S,(bool the carrier of T) such that
A12: for x being Element of S holds S1[x,D . x] from FUNCT_2:sch_3(A9);
defpred S2[ 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 S2[x,y]
proof
let x be Element of dyadic (n + 1); ::_thesis: ex y being Subset of T st S2[x,y]
percases ( x in dyadic n or not x in dyadic n ) ;
suppose x in dyadic n ; ::_thesis: ex y being Subset of T st S2[x,y]
then reconsider x = x as Element of dyadic n ;
consider y being Subset of T such that
A14: y = G . x ;
take y ; ::_thesis: S2[x,y]
thus S2[x,y] by A14; ::_thesis: verum
end;
supposeA15: not x in dyadic n ; ::_thesis: ex y being Subset of T st S2[x,y]
then reconsider x = x as Element of S by XBOOLE_0:def_5;
consider y being Subset of T such that
A16: y = D . x ;
take y ; ::_thesis: S2[x,y]
thus S2[x,y] by A15, A16; ::_thesis: verum
end;
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 S2[x,F . x] from FUNCT_2:sch_3(A13);
take F ; ::_thesis: ( 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 ) ) ) )
( 0 in dyadic n & 1 in dyadic n ) by Th6;
hence ( A c= F . 0 & B = ([#] T) \ (F . 1) ) by A3, A4, A17, A8; ::_thesis: 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 ) )
let r1, r2, r be Element of dyadic (n + 1); ::_thesis: ( r1 < r2 implies ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) )
assume A18: r1 < r2 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) )
thus ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ::_thesis: ( r in dyadic n implies F . r = G . r )
proof
now__::_thesis:_(_F_._r1_is_open_&_F_._r2_is_open_&_Cl_(F_._r1)_c=_F_._r2_)
percases ( ( r1 in dyadic n & r2 in dyadic n ) or ( r1 in dyadic n & not r2 in dyadic n ) or ( not r1 in dyadic n & r2 in dyadic n ) or ( not r1 in dyadic n & not r2 in dyadic n ) ) ;
supposeA19: ( r1 in dyadic n & r2 in dyadic n ) ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
then A20: ( F . r1 = G . r1 & F . r2 = G . r2 ) by A17;
reconsider r1 = r1, r2 = r2 as Element of dyadic n by A19;
r1 < r2 by A18;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A5, A20; ::_thesis: verum
end;
supposeA21: ( r1 in dyadic n & not r2 in dyadic n ) ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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__::_thesis:_(_F_._r1_is_open_&_F_._r2_is_open_&_Cl_(F_._r1)_c=_F_._r2_)
percases ( r1 = q1 or r1 < q1 ) by A24, XXREAL_0:1;
suppose r1 = q1 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A28, A25, A29, A30, A27, A31, Def8; ::_thesis: verum
end;
supposeA32: r1 < q1 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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, XBOOLE_1:1;
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 ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A28, A25, A29, A27, A34, A36, A37, A35, Def8, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; ::_thesis: verum
end;
supposeA38: ( not r1 in dyadic n & r2 in dyadic n ) ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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__::_thesis:_(_F_._r1_is_open_&_F_._r2_is_open_&_Cl_(F_._r1)_c=_F_._r2_)
percases ( q2 = r2 or q2 < r2 ) by A41, XXREAL_0:1;
suppose q2 = r2 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A45, A42, A46, A47, A44, A48, Def8; ::_thesis: verum
end;
supposeA49: q2 < r2 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . 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, XBOOLE_1:1;
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 ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A45, A42, A46, A44, A51, A52, A53, A54, Def8, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; ::_thesis: verum
end;
supposeA55: ( not r1 in dyadic n & not r2 in dyadic n ) ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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; ::_thesis: Cl (F . r1) c= F . r2
A72: q21 <= q12 by A18, A55, A57, A61, Th16;
now__::_thesis:_Cl_(F_._r1)_c=_F_._r2
percases ( q21 = q12 or q21 < q12 ) by A72, XXREAL_0:1;
supposeA73: q21 = q12 ; ::_thesis: Cl (F . r1) c= F . r2
( 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) by XBOOLE_1:1;
Cl (G . q21) c= F . r2 by A1, A60, A69, A63, A67, A66, A73, Def8;
hence Cl (F . r1) c= F . r2 by A74, XBOOLE_1:1; ::_thesis: verum
end;
supposeA75: q21 < q12 ; ::_thesis: Cl (F . r1) c= F . r2
( 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) by XBOOLE_1:1;
Cl (G . q21) c= G . q12 by A5, A75;
then A77: Cl (F . r1) c= G . q12 by A76, XBOOLE_1:1;
( 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 by XBOOLE_1:1;
hence Cl (F . r1) c= F . r2 by A77, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence Cl (F . r1) c= F . r2 ; ::_thesis: verum
end;
end;
end;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; ::_thesis: verum
end;
thus ( r in dyadic n implies F . r = G . r ) by A17; ::_thesis: verum
end;