:: Urysohn Lemma
:: by J\'ozef Bia{\l}as and Yatsuka Nakamura
::
:: Received February 16, 2001
:: Copyright (c) 2001 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 ) ) )
theorem Th1: :: URYSOHN3:1
:: deftheorem Def1 defines Drizzle URYSOHN3:def 1 :
theorem :: URYSOHN3:2
canceled;
theorem Th3: :: URYSOHN3:3
theorem Th4: :: URYSOHN3:4
theorem Th5: :: URYSOHN3:5
:: deftheorem Def2 defines Rain URYSOHN3:def 2 :
:: deftheorem Def3 defines inf_number_dyadic URYSOHN3:def 3 :
theorem Th6: :: URYSOHN3:6
theorem Th7: :: URYSOHN3:7
theorem Th8: :: URYSOHN3:8
theorem Th9: :: URYSOHN3:9
theorem Th10: :: URYSOHN3:10
theorem Th11: :: URYSOHN3:11
:: deftheorem Def4 defines Tempest URYSOHN3:def 4 :
theorem Th12: :: URYSOHN3:12
theorem Th13: :: URYSOHN3:13
theorem Th14: :: URYSOHN3:14
:: deftheorem Def5 defines Rainbow URYSOHN3:def 5 :
theorem Th15: :: URYSOHN3:15
theorem Th16: :: URYSOHN3:16
definition
let T be non
empty TopSpace;
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
ex b1 being Function of T,R^1 st
for p being Point of T holds
( ( Rainbow p,R = {} implies b1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow p,R holds
b1 . p = sup S ) )
by Th16;
uniqueness
for b1, b2 being Function of T,R^1 st ( for p being Point of T holds
( ( Rainbow p,R = {} implies b1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow p,R holds
b1 . p = sup S ) ) ) & ( for p being Point of T holds
( ( Rainbow p,R = {} implies b2 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow p,R holds
b2 . p = sup S ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines Thunder URYSOHN3:def 6 :
theorem Th17: :: URYSOHN3:17
theorem Th18: :: URYSOHN3:18
theorem Th19: :: URYSOHN3:19
theorem Th20: :: URYSOHN3:20
theorem Th21: :: URYSOHN3:21
theorem Th22: :: URYSOHN3:22
theorem Th23: :: URYSOHN3:23
theorem :: URYSOHN3:24