:: by J\'ozef Bia{\l}as and Yatsuka Nakamura

::

:: Received February 16, 2001

:: Copyright (c) 2001-2019 Association of Mizar Users

Lm1: for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

ex G being Function of (dyadic 0),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic 0 st r1 < r2 holds

( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) )

proof end;

theorem Th1: :: URYSOHN3:1

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for n being Nat ex 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 ) ) )

for A, B being closed Subset of T st A <> {} & A misses B holds

for n being Nat ex 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 ) ) )

proof end;

definition

let T be non empty TopSpace;

let A, B be Subset of T;

let n be Nat;

assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;

ex b_{1} being Function of (dyadic n),(bool the carrier of T) st

( A c= b_{1} . 0 & B = ([#] T) \ (b_{1} . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds

( b_{1} . r1 is open & b_{1} . r2 is open & Cl (b_{1} . r1) c= b_{1} . r2 ) ) )
by A1, Th1;

end;
let A, B be Subset of T;

let n be Nat;

assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;

mode Drizzle of A,B,n -> Function of (dyadic n),(bool the carrier of T) means :Def1: :: URYSOHN3:def 1

( A c= it . 0 & B = ([#] T) \ (it . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds

( it . r1 is open & it . r2 is open & Cl (it . r1) c= it . r2 ) ) );

existence ( A c= it . 0 & B = ([#] T) \ (it . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds

( it . r1 is open & it . r2 is open & Cl (it . r1) c= it . r2 ) ) );

ex b

( A c= b

( b

:: deftheorem Def1 defines Drizzle URYSOHN3:def 1 :

for T being non empty TopSpace

for A, B being Subset of T

for n being Nat st T is normal & A <> {} & A is closed & B is closed & A misses B holds

for b_{5} being Function of (dyadic n),(bool the carrier of T) holds

( b_{5} is Drizzle of A,B,n iff ( A c= b_{5} . 0 & B = ([#] T) \ (b_{5} . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds

( b_{5} . r1 is open & b_{5} . r2 is open & Cl (b_{5} . r1) c= b_{5} . r2 ) ) ) );

for T being non empty TopSpace

for A, B being Subset of T

for n being Nat st T is normal & A <> {} & A is closed & B is closed & A misses B holds

for b

( b

( b

theorem Th2: :: URYSOHN3:2

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for n being Nat

for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

for A, B being closed Subset of T st A <> {} & A misses B holds

for n being Nat

for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

proof end;

theorem Th3: :: URYSOHN3:3

for T being non empty TopSpace

for A, B being Subset of T

for n being Nat

for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))

for A, B being Subset of T

for n being Nat

for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))

proof end;

theorem Th4: :: URYSOHN3:4

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st

for n being Nat holds

( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) )

for A, B being closed Subset of T st A <> {} & A misses B holds

ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st

for n being Nat holds

( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) )

proof end;

definition

let T be non empty TopSpace;

let A, B be Subset of T;

assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;

ex b_{1} being Functional_Sequence of DYADIC,(bool the carrier of T) st

for n being Nat holds

( b_{1} . n is Drizzle of A,B,n & ( for r being Element of dom (b_{1} . n) holds (b_{1} . n) . r = (b_{1} . (n + 1)) . r ) )
by A1, Th4;

end;
let A, B be Subset of T;

assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;

mode Rain of A,B -> Functional_Sequence of DYADIC,(bool the carrier of T) means :Def2: :: URYSOHN3:def 2

for n being Nat holds

( it . n is Drizzle of A,B,n & ( for r being Element of dom (it . n) holds (it . n) . r = (it . (n + 1)) . r ) );

existence for n being Nat holds

( it . n is Drizzle of A,B,n & ( for r being Element of dom (it . n) holds (it . n) . r = (it . (n + 1)) . r ) );

ex b

for n being Nat holds

( b

:: deftheorem Def2 defines Rain URYSOHN3:def 2 :

for T being non empty TopSpace

for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds

for b_{4} being Functional_Sequence of DYADIC,(bool the carrier of T) holds

( b_{4} is Rain of A,B iff for n being Nat holds

( b_{4} . n is Drizzle of A,B,n & ( for r being Element of dom (b_{4} . n) holds (b_{4} . n) . r = (b_{4} . (n + 1)) . r ) ) );

for T being non empty TopSpace

for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds

for b

( b

( b

definition

let x be Real;

assume A1: x in DYADIC ;

ex b_{1} being Nat st

( ( x in dyadic 0 implies b_{1} = 0 ) & ( b_{1} = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

b_{1} = n + 1 ) )

for b_{1}, b_{2} being Nat holds

not ( ( x in dyadic 0 implies b_{1} = 0 ) & ( b_{1} = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

b_{1} = n + 1 ) & ( x in dyadic 0 implies b_{2} = 0 ) & ( b_{2} = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

b_{2} = n + 1 ) & not b_{1} = b_{2} )

end;
assume A1: x in DYADIC ;

func inf_number_dyadic x -> Nat means :Def3: :: URYSOHN3:def 3

( ( x in dyadic 0 implies it = 0 ) & ( it = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

it = n + 1 ) );

existence ( ( x in dyadic 0 implies it = 0 ) & ( it = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

it = n + 1 ) );

ex b

( ( x in dyadic 0 implies b

b

proof end;

uniqueness for b

not ( ( x in dyadic 0 implies b

b

b

proof end;

:: deftheorem Def3 defines inf_number_dyadic URYSOHN3:def 3 :

for x being Real st x in DYADIC holds

for b_{2} being Nat holds

( b_{2} = inf_number_dyadic x iff ( ( x in dyadic 0 implies b_{2} = 0 ) & ( b_{2} = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

b_{2} = n + 1 ) ) );

for x being Real st x in DYADIC holds

for b

( b

b

theorem Th6: :: URYSOHN3:6

for x being Real st x in DYADIC holds

for n being Nat st inf_number_dyadic x <= n holds

x in dyadic n

for n being Nat st inf_number_dyadic x <= n holds

x in dyadic n

proof end;

theorem Th8: :: URYSOHN3:8

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

proof end;

theorem Th9: :: URYSOHN3:9

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for x being Real st x in DYADIC holds

ex y being Subset of T st

for n being Nat st x in dyadic n holds

y = (G . n) . x

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for x being Real st x in DYADIC holds

ex y being Subset of T st

for n being Nat st x in dyadic n holds

y = (G . n) . x

proof end;

theorem Th10: :: URYSOHN3:10

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st

for x being Real st x in DOM holds

( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds

F . x = (G . n) . x ) )

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st

for x being Real st x in DOM holds

( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds

F . x = (G . n) . x ) )

proof end;

definition

let T be non empty TopSpace;

let A, B be Subset of T;

assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;

let R be Rain of A,B;

ex b_{1} being Function of DOM,(bool the carrier of T) st

for x being Real st x in DOM holds

( ( x in halfline 0 implies b_{1} . x = {} ) & ( x in right_open_halfline 1 implies b_{1} . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds

b_{1} . x = (R . n) . x ) )
by A1, Th10;

uniqueness

for b_{1}, b_{2} being Function of DOM,(bool the carrier of T) st ( for x being Real st x in DOM holds

( ( x in halfline 0 implies b_{1} . x = {} ) & ( x in right_open_halfline 1 implies b_{1} . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds

b_{1} . x = (R . n) . x ) ) ) & ( for x being Real st x in DOM holds

( ( x in halfline 0 implies b_{2} . x = {} ) & ( x in right_open_halfline 1 implies b_{2} . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds

b_{2} . x = (R . n) . x ) ) ) holds

b_{1} = b_{2}

end;
let A, B be Subset of T;

assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;

let R be Rain of A,B;

func Tempest R -> Function of DOM,(bool the carrier of T) means :Def4: :: URYSOHN3:def 4

for x being Real st x in DOM holds

( ( x in halfline 0 implies it . x = {} ) & ( x in right_open_halfline 1 implies it . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds

it . x = (R . n) . x ) );

existence for x being Real st x in DOM holds

( ( x in halfline 0 implies it . x = {} ) & ( x in right_open_halfline 1 implies it . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds

it . x = (R . n) . x ) );

ex b

for x being Real st x in DOM holds

( ( x in halfline 0 implies b

b

uniqueness

for b

( ( x in halfline 0 implies b

b

( ( x in halfline 0 implies b

b

b

proof end;

:: deftheorem Def4 defines Tempest URYSOHN3:def 4 :

for T being non empty TopSpace

for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds

for R being Rain of A,B

for b_{5} being Function of DOM,(bool the carrier of T) holds

( b_{5} = Tempest R iff for x being Real st x in DOM holds

( ( x in halfline 0 implies b_{5} . x = {} ) & ( x in right_open_halfline 1 implies b_{5} . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds

b_{5} . x = (R . n) . x ) ) );

for T being non empty TopSpace

for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds

for R being Rain of A,B

for b

( b

( ( x in halfline 0 implies b

b

theorem Th11: :: URYSOHN3:11

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r being Real

for C being Subset of T st C = (Tempest G) . r & r in DOM holds

C is open

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r being Real

for C being Subset of T st C = (Tempest G) . r & r in DOM holds

C is open

proof end;

theorem Th12: :: URYSOHN3:12

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds

for C being Subset of T st C = (Tempest G) . r1 holds

Cl C c= (Tempest G) . r2

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds

for C being Subset of T st C = (Tempest G) . r1 holds

Cl C c= (Tempest G) . r2

proof end;

definition

let T be non empty TopSpace;

let A, B be Subset of T;

let G be Rain of A,B;

let p be Point of T;

ex b_{1} being Subset of ExtREAL st

for x being set holds

( x in b_{1} iff ( x in DYADIC & ( for s being Real st s = x holds

not p in (Tempest G) . s ) ) )

for b_{1}, b_{2} being Subset of ExtREAL st ( for x being set holds

( x in b_{1} iff ( x in DYADIC & ( for s being Real st s = x holds

not p in (Tempest G) . s ) ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in DYADIC & ( for s being Real st s = x holds

not p in (Tempest G) . s ) ) ) ) holds

b_{1} = b_{2}

end;
let A, B be Subset of T;

let G be Rain of A,B;

let p be Point of T;

func Rainbow (p,G) -> Subset of ExtREAL means :Def5: :: URYSOHN3:def 5

for x being set holds

( x in it iff ( x in DYADIC & ( for s being Real st s = x holds

not p in (Tempest G) . s ) ) );

existence for x being set holds

( x in it iff ( x in DYADIC & ( for s being Real st s = x holds

not p in (Tempest G) . s ) ) );

ex b

for x being set holds

( x in b

not p in (Tempest G) . s ) ) )

proof end;

uniqueness for b

( x in b

not p in (Tempest G) . s ) ) ) ) & ( for x being set holds

( x in b

not p in (Tempest G) . s ) ) ) ) holds

b

proof end;

:: deftheorem Def5 defines Rainbow URYSOHN3:def 5 :

for T being non empty TopSpace

for A, B being Subset of T

for G being Rain of A,B

for p being Point of T

for b_{6} being Subset of ExtREAL holds

( b_{6} = Rainbow (p,G) iff for x being set holds

( x in b_{6} iff ( x in DYADIC & ( for s being Real st s = x holds

not p in (Tempest G) . s ) ) ) );

for T being non empty TopSpace

for A, B being Subset of T

for G being Rain of A,B

for p being Point of T

for b

( b

( x in b

not p in (Tempest G) . s ) ) ) );

definition

let T be non empty TopSpace;

let A, B be Subset of T;

let R be Rain of A,B;

ex b_{1} being Function of T,R^1 st

for p being Point of T holds

( ( Rainbow (p,R) = {} implies b_{1} . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds

b_{1} . p = sup S ) )

for b_{1}, b_{2} being Function of T,R^1 st ( for p being Point of T holds

( ( Rainbow (p,R) = {} implies b_{1} . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds

b_{1} . p = sup S ) ) ) & ( for p being Point of T holds

( ( Rainbow (p,R) = {} implies b_{2} . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds

b_{2} . p = sup S ) ) ) holds

b_{1} = b_{2}

end;
let A, B be Subset of T;

let R be Rain of A,B;

func Thunder R -> Function of T,R^1 means :Def6: :: URYSOHN3:def 6

for p being Point of T holds

( ( Rainbow (p,R) = {} implies it . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds

it . p = sup S ) );

existence for p being Point of T holds

( ( Rainbow (p,R) = {} implies it . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds

it . p = sup S ) );

ex b

for p being Point of T holds

( ( Rainbow (p,R) = {} implies b

b

proof end;

uniqueness for b

( ( Rainbow (p,R) = {} implies b

b

( ( Rainbow (p,R) = {} implies b

b

b

proof end;

:: deftheorem Def6 defines Thunder URYSOHN3:def 6 :

for T being non empty TopSpace

for A, B being Subset of T

for R being Rain of A,B

for b_{5} being Function of T,R^1 holds

( b_{5} = Thunder R iff for p being Point of T holds

( ( Rainbow (p,R) = {} implies b_{5} . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds

b_{5} . p = sup S ) ) );

for T being non empty TopSpace

for A, B being Subset of T

for R being Rain of A,B

for b

( b

( ( Rainbow (p,R) = {} implies b

b

theorem Th14: :: URYSOHN3:14

for T being non empty TopSpace

for A, B being Subset of T

for G being Rain of A,B

for p being Point of T

for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

for A, B being Subset of T

for G being Rain of A,B

for p being Point of T

for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

proof end;

theorem Th15: :: URYSOHN3:15

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

proof end;

theorem Th16: :: URYSOHN3:16

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds

for p being Point of T st p in (Tempest G) . r holds

(Thunder G) . p <= r

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds

for p being Point of T st p in (Tempest G) . r holds

(Thunder G) . p <= r

proof end;

theorem Th17: :: URYSOHN3:17

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

proof end;

theorem Th18: :: URYSOHN3:18

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B holds

( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )

for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B holds

( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )

proof end;

theorem Th19: :: URYSOHN3:19

for T being non empty normal TopSpace

for A, B being closed Subset of T st A <> {} & A misses B holds

ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

for A, B being closed Subset of T st A <> {} & A misses B holds

ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

proof end;

:: Urysohn's lemma

theorem Th20: :: URYSOHN3:20

for T being non empty normal TopSpace

for A, B being closed Subset of T st A misses B holds

ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

for A, B being closed Subset of T st A misses B holds

ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

proof end;

theorem :: URYSOHN3:21