:: by J\'ozef Bia\las and Yatsuka Nakamura

::

:: Received July 29, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

definition

let n be Nat;

ex b_{1} being Subset of REAL st

for x being Real holds

( x in b_{1} iff ex i being Element of NAT st

( i <= 2 |^ n & x = i / (2 |^ n) ) )

for b_{1}, b_{2} being Subset of REAL st ( for x being Real holds

( x in b_{1} iff ex i being Element of NAT st

( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds

( x in b_{2} iff ex i being Element of NAT st

( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) holds

b_{1} = b_{2}

end;
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 for x being Real holds

( x in it iff ex i being Element of NAT st

( i <= 2 |^ n & x = i / (2 |^ n) ) );

ex b

for x being Real holds

( x in b

( i <= 2 |^ n & x = i / (2 |^ n) ) )

proof end;

uniqueness for b

( x in b

( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds

( x in b

( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) holds

b

proof end;

:: deftheorem Def1 defines dyadic URYSOHN1:def 1 :

for n being Nat

for b_{2} being Subset of REAL holds

( b_{2} = dyadic n iff for x being Real holds

( x in b_{2} iff ex i being Element of NAT st

( i <= 2 |^ n & x = i / (2 |^ n) ) ) );

for n being Nat

for b

( b

( x in b

( i <= 2 |^ n & x = i / (2 |^ n) ) ) );

definition

ex b_{1} being Subset of REAL st

for a being Real holds

( a in b_{1} iff ex n being Element of NAT st a in dyadic n )

for b_{1}, b_{2} being Subset of REAL st ( for a being Real holds

( a in b_{1} iff ex n being Element of NAT st a in dyadic n ) ) & ( for a being Real holds

( a in b_{2} iff ex n being Element of NAT st a in dyadic n ) ) holds

b_{1} = b_{2}
end;

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 for a being Real holds

( a in it iff ex n being Element of NAT st a in dyadic n );

ex b

for a being Real holds

( a in b

proof end;

uniqueness for b

( a in b

( a in b

b

proof end;

:: deftheorem Def2 defines DYADIC URYSOHN1:def 2 :

for b_{1} being Subset of REAL holds

( b_{1} = DYADIC iff for a being Real holds

( a in b_{1} iff ex n being Element of NAT st a in dyadic n ) );

for b

( b

( a in b

definition

((halfline 0) \/ DYADIC) \/ (right_open_halfline 1) is Subset of REAL ;

end;

func DOM -> Subset of REAL equals :: URYSOHN1:def 3

((halfline 0) \/ DYADIC) \/ (right_open_halfline 1);

coherence ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1);

((halfline 0) \/ DYADIC) \/ (right_open_halfline 1) is Subset of REAL ;

:: deftheorem defines DOM URYSOHN1:def 3 :

DOM = ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1);

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 func F . r -> Subset of T;

coherence

F . r is Subset of T

end;
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 func F . r -> Subset of T;

coherence

F . r is Subset of T

proof end;

registration
end;

definition

let n be Nat;

ex b_{1} being FinSequence st

( dom b_{1} = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b_{1} holds

b_{1} . i = (i - 1) / (2 |^ n) ) )

for b_{1}, b_{2} being FinSequence st dom b_{1} = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b_{1} holds

b_{1} . i = (i - 1) / (2 |^ n) ) & dom b_{2} = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b_{2} holds

b_{2} . i = (i - 1) / (2 |^ n) ) holds

b_{1} = b_{2}

end;
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 ( dom it = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom it holds

it . i = (i - 1) / (2 |^ n) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines dyad URYSOHN1:def 4 :

for n being Nat

for b_{2} being FinSequence holds

( b_{2} = dyad n iff ( dom b_{2} = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b_{2} holds

b_{2} . i = (i - 1) / (2 |^ n) ) ) );

for n being Nat

for b

( b

b

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)

((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)

proof 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)

((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)

proof end;

definition

let n be Nat;

let x be Element of dyadic n;

existence

ex b_{1} being Element of NAT st x = b_{1} / (2 |^ n)

for b_{1}, b_{2} being Element of NAT st x = b_{1} / (2 |^ n) & x = b_{2} / (2 |^ n) holds

b_{1} = b_{2}

end;
let x be Element of dyadic n;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines axis URYSOHN1:def 5 :

for n being Nat

for x being Element of dyadic n

for b_{3} being Element of NAT holds

( b_{3} = axis x iff x = b_{3} / (2 |^ n) );

for n being Nat

for x being Element of dyadic n

for b

( b

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 )

for x being Element of dyadic n holds

( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )

proof 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) )

for x being Element of dyadic n holds

( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) )

proof 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)

for x being Element of dyadic n holds ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n)

proof 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 )

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 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 )

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 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))

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 end;

begin

notation
end;

definition

let T be non empty TopSpace;

let x be Point of T;

for b_{1} being Element of bool the carrier of T holds

( b_{1} is Nbhd of x,T iff ex A being Subset of T st

( A is open & x in A & A c= b_{1} ) )

end;
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 ex A being Subset of T st

( A is open & x in A & A c= it );

for b

( b

( A is open & x in A & A c= b

proof end;

:: deftheorem defines Nbhd URYSOHN1:def 6 :

for T being non empty TopSpace

for x being Point of T

for b_{3} being Element of bool the carrier of T holds

( b_{3} is Nbhd of x,T iff ex A being Subset of T st

( A is open & x in A & A c= b_{3} ) );

for T being non empty TopSpace

for x being Point of T

for b

( b

( A is open & x in A & A c= b

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 )

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 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

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 end;

definition

let T be TopSpace;

( 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 ) )

end;
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 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 );

( 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 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 ) );

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 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 )

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 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 ) )

( 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 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 )

for A being open Subset of T st A <> {} holds

ex B being Subset of T st

( B <> {} & Cl B c= A )

proof 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 )

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 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 ) ;

ex b_{1} being Subset of T st

( b_{1} <> {} & b_{1} is open & Cl A c= b_{1} & Cl b_{1} c= B )
by A1, Th20;

end;
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 ( it <> {} & it is open & Cl A c= it & Cl it c= B );

ex b

( b

:: 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 b_{4} being Subset of T holds

( b_{4} is Between of A,B iff ( b_{4} <> {} & b_{4} is open & Cl A c= b_{4} & Cl b_{4} c= B ) );

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 b

( 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 ) ) ) )

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 end;

:: Some increasing family of sets in normal space

::