begin
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:
:: deftheorem Def1 defines Drizzle URYSOHN3:def 1 :
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
:: deftheorem Def2 defines Rain URYSOHN3:def 2 :
:: deftheorem Def3 defines inf_number_dyadic URYSOHN3:def 3 :
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
:: deftheorem Def4 defines Tempest URYSOHN3:def 4 :
theorem Th12:
theorem Th13:
theorem Th14:
:: deftheorem Def5 defines Rainbow URYSOHN3:def 5 :
theorem Th15:
theorem Th16:
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:
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:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem