:: URYSOHN3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let D be non empty Subset of REAL ;
cluster -> real Element of D;
coherence
for b1 being Element of D holds b1 is real
;
end;

Lm1: for T being non empty being_T4 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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 ) ) )
proof end;

definition
let T be non empty TopSpace;
let A, B be Subset of T;
let n be Nat;
assume A1: ( T is_T4 & 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
ex b1 being Function of dyadic n, bool the carrier of T st
( A c= b1 . 0 & B = ([#] T) \ (b1 . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds
( b1 . r1 is open & b1 . r2 is open & Cl (b1 . r1) c= b1 . r2 ) ) )
by A1, Th1;
end;

:: 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_T4 & A <> {} & A is closed & B is closed & A misses B holds
for b5 being Function of dyadic n, bool the carrier of T holds
( b5 is Drizzle of A,B,n iff ( A c= b5 . 0 & B = ([#] T) \ (b5 . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds
( b5 . r1 is open & b5 . r2 is open & Cl (b5 . r1) c= b5 . r2 ) ) ) );

theorem :: URYSOHN3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: URYSOHN3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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
proof end;

definition
let A, B be non empty set ;
let F be Function of NAT , PFuncs A,B;
let n be Nat;
:: original: .
redefine func F . n -> PartFunc of A,B;
correctness
coherence
F . n is PartFunc of A,B
;
proof end;
end;

theorem Th4: :: URYSOHN3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

definition
let A, B be non empty set ;
let F be Function of NAT , PFuncs A,B;
let n be Nat;
:: original: .
redefine func F . n -> Element of PFuncs A,B;
coherence
F . n is Element of PFuncs A,B
by FUNCT_2:7;
end;

theorem Th5: :: URYSOHN3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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 ) )
proof end;

definition
let T be non empty TopSpace;
let A, B be Subset of T;
assume A1: ( T is_T4 & 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
ex b1 being Functional_Sequence of DYADIC , bool the carrier of T st
for n being Nat holds
( b1 . n is Drizzle of A,B,n & ( for r being Element of dom (b1 . n) holds (b1 . n) . r = (b1 . (n + 1)) . r ) )
by A1, Th5;
end;

:: deftheorem Def2 defines Rain URYSOHN3:def 2 :
for T being non empty TopSpace
for A, B being Subset of T st T is_T4 & A <> {} & A is closed & B is closed & A misses B holds
for b4 being Functional_Sequence of DYADIC , bool the carrier of T holds
( b4 is Rain of A,B iff for n being Nat holds
( b4 . n is Drizzle of A,B,n & ( for r being Element of dom (b4 . n) holds (b4 . n) . r = (b4 . (n + 1)) . r ) ) );

definition
let x be Real;
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
ex b1 being Nat st
( ( x in dyadic 0 implies b1 = 0 ) & ( b1 = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
b1 = n + 1 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
not ( ( x in dyadic 0 implies b1 = 0 ) & ( b1 = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
b1 = n + 1 ) & ( x in dyadic 0 implies b2 = 0 ) & ( b2 = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
b2 = n + 1 ) & not b1 = b2 )
proof end;
end;

:: deftheorem Def3 defines inf_number_dyadic URYSOHN3:def 3 :
for x being Real st x in DYADIC holds
for b2 being Nat holds
( b2 = inf_number_dyadic x iff ( ( x in dyadic 0 implies b2 = 0 ) & ( b2 = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
b2 = n + 1 ) ) );

theorem Th6: :: URYSOHN3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real st x in DYADIC holds
x in dyadic (inf_number_dyadic x)
proof end;

theorem Th7: :: URYSOHN3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real st x in DYADIC holds
for n being Nat st inf_number_dyadic x <= n holds
x in dyadic n
proof end;

theorem Th8: :: URYSOHN3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real
for n being Nat st x in dyadic n holds
inf_number_dyadic x <= n
proof end;

theorem Th9: :: URYSOHN3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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
proof end;

theorem Th10: :: URYSOHN3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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
proof end;

theorem Th11: :: URYSOHN3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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 R<0 implies F . x = {} ) & ( x in R>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_T4 & 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 R<0 implies it . x = {} ) & ( x in R>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
ex b1 being Function of DOM , bool the carrier of T st
for x being Real st x in DOM holds
( ( x in R<0 implies b1 . x = {} ) & ( x in R>1 implies b1 . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
b1 . x = (R . n) . x ) )
by A1, Th11;
uniqueness
for b1, b2 being Function of DOM , bool the carrier of T st ( for x being Real st x in DOM holds
( ( x in R<0 implies b1 . x = {} ) & ( x in R>1 implies b1 . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
b1 . x = (R . n) . x ) ) ) & ( for x being Real st x in DOM holds
( ( x in R<0 implies b2 . x = {} ) & ( x in R>1 implies b2 . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
b2 . x = (R . n) . x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Tempest URYSOHN3:def 4 :
for T being non empty TopSpace
for A, B being Subset of T st T is_T4 & A <> {} & A is closed & B is closed & A misses B holds
for R being Rain of A,B
for b5 being Function of DOM , bool the carrier of T holds
( b5 = Tempest R iff for x being Real st x in DOM holds
( ( x in R<0 implies b5 . x = {} ) & ( x in R>1 implies b5 . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
b5 . x = (R . n) . x ) ) );

definition
let X be non empty set ;
let T be TopSpace;
let F be Function of X, bool the carrier of T;
let x be Element of X;
:: original: .
redefine func F . x -> Subset of T;
correctness
coherence
F . x is Subset of T
;
proof end;
end;

theorem Th12: :: URYSOHN3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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
proof end;

theorem Th13: :: URYSOHN3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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
proof end;

theorem Th14: :: URYSOHN3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ex R being Subset of ExtREAL st
for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) )
proof end;

definition
let T be non empty TopSpace;
let A, B be Subset of T;
let R be Rain of A,B;
let p be Point of T;
func Rainbow p,R -> 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 R) . s ) ) );
existence
ex b1 being Subset of ExtREAL st
for x being set holds
( x in b1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest R) . s ) ) )
by Th14;
uniqueness
for b1, b2 being Subset of ExtREAL st ( for x being set holds
( x in b1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest R) . s ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest R) . s ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Rainbow URYSOHN3:def 5 :
for T being non empty TopSpace
for A, B being Subset of T
for R being Rain of A,B
for p being Point of T
for b6 being Subset of ExtREAL holds
( b6 = Rainbow p,R iff for x being set holds
( x in b6 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest R) . s ) ) ) );

definition
let T, S be non empty TopSpace;
let F be Function of T,S;
let p be Point of T;
:: original: .
redefine func F . p -> Point of S;
correctness
coherence
F . p is Point of S
;
proof end;
end;

theorem Th15: :: URYSOHN3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 holds Rainbow p,G c= DYADIC
proof end;

theorem Th16: :: URYSOHN3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T
for R being Rain of A,B ex F being Function of T,R^1 st
for p being Point of T holds
( ( Rainbow p,R = {} implies F . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow p,R holds
F . p = sup S ) )
proof end;

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
proof end;
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 b5 being Function of T,R^1 holds
( b5 = Thunder R iff for p being Point of T holds
( ( Rainbow p,R = {} implies b5 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow p,R holds
b5 . p = sup S ) ) );

definition
let T be non empty TopSpace;
let F be Function of T,R^1 ;
let p be Point of T;
:: original: .
redefine func F . p -> Real;
correctness
coherence
F . p is Real
;
proof end;
end;

theorem Th17: :: URYSOHN3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th18: :: URYSOHN3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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
proof end;

theorem Th19: :: URYSOHN3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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 \/ R>1 & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
proof end;

theorem Th20: :: URYSOHN3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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
proof end;

theorem Th21: :: URYSOHN3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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 ) ) ) )
proof end;

theorem Th22: :: URYSOHN3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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 ) ) ) )
proof end;

theorem Th23: :: URYSOHN3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty being_T4 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 ) ) ) )
proof end;

theorem :: URYSOHN3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty compact being_T2 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 ) ) ) ) by Th23;