:: URYSOHN3 semantic presentation

registration

let c₁ be non empty Subset of REAL ;
cluster -> real Element of a₁;
coherence ;

end;

Lemma1: for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
ex b₄ being Function of dyadic 0, bool the carrier of b₁ st
( b₂ c= b₄ . 0 & b₃ = ([#] b₁) \ (b₄ . 1) & ( for b₅, b₆ being Element of dyadic 0 st b₅ < b₆ holds
( b₄ . b₅ is open & b₄ . b₆ is open & Cl (b₄ . b₅) c= b₄ . b₆ ) ) )

proof end;

theorem Th1: :: URYSOHN3:1

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Nat ex b₅ being Function of dyadic b₄, bool the carrier of b₁ st
( b₂ c= b₅ . 0 & b₃ = ([#] b₁) \ (b₅ . 1) & ( for b₆, b₇ being Element of dyadic b₄ st b₆ < b₇ holds
( b₅ . b₆ is open & b₅ . b₇ is open & Cl (b₅ . b₆) c= b₅ . b₇ ) ) )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Subset of c₁;
let c₄ be Nat;
assume E3: ( c₁ is_T4 & c₂ <> {} & c₂ is closed & c₃ is closed & c₂ misses c₃ ) ;
mode Drizzle of c₂,c₃,c₄ -> Function of dyadic a₄, bool the carrier of a₁ means :Def1: :: URYSOHN3:def 1
( a₂ c= a₅ . 0 & a₃ = ([#] a₁) \ (a₅ . 1) & ( for b₁, b₂ being Element of dyadic a₄ st b₁ < b₂ holds
( a₅ . b₁ is open & a₅ . b₂ is open & Cl (a₅ . b₁) c= a₅ . b₂ ) ) );
existence by E3, Th1;

end;

:: deftheorem Def1 defines Drizzle URYSOHN3:def 1 :

theorem Th2: :: URYSOHN3:2

canceled;

theorem Th3: :: URYSOHN3:3

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Nat
for b₅ being Drizzle of b₂,b₃,b₄ ex b₆ being Drizzle of b₂,b₃,b₄ + 1 st
for b₇ being Element of dyadic (b₄ + 1) st b₇ in dyadic b₄ holds
b₆ . b₇ = b₅ . b₇

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of NAT , PFuncs c₁,c₂;
let c₄ be Nat;
redefine func . as c₃ . c₄ -> PartFunc of a₁,a₂;
correctness

proof end;

end;

theorem Th4: :: URYSOHN3:4

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Nat
for b₅ being Drizzle of b₂,b₃,b₄ holds b₅ is Element of PFuncs DYADIC ,(bool the carrier of b₁)

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of NAT , PFuncs c₁,c₂;
let c₄ be Nat;
redefine func . as c₃ . c₄ -> Element of PFuncs a₁,a₂;
coherence by FUNCT_2:7;

end;

theorem Th5: :: URYSOHN3:5

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
ex b₄ being Functional_Sequence of DYADIC , bool the carrier of b₁ st
for b₅ being Nat holds
( b₄ . b₅ is Drizzle of b₂,b₃,b₅ & ( for b₆ being Element of dom (b₄ . b₅) holds (b₄ . b₅) . b₆ = (b₄ . (b₅ + 1)) . b₆ ) )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Subset of c₁;
assume E7: ( c₁ is_T4 & c₂ <> {} & c₂ is closed & c₃ is closed & c₂ misses c₃ ) ;
mode Rain of c₂,c₃ -> Functional_Sequence of DYADIC , bool the carrier of a₁ means :Def2: :: URYSOHN3:def 2
for b₁ being Nat holds
( a₄ . b₁ is Drizzle of a₂,a₃,b₁ & ( for b₂ being Element of dom (a₄ . b₁) holds (a₄ . b₁) . b₂ = (a₄ . (b₁ + 1)) . b₂ ) );
existence by E7, Th5;

end;

:: deftheorem Def2 defines Rain URYSOHN3:def 2 :

definition

let c₁ be Real;
assume E8: c₁ in DYADIC ;
func inf_number_dyadic c₁ -> Nat means :Def3: :: URYSOHN3:def 3
( ( a₁ in dyadic 0 implies a₂ = 0 ) & ( a₂ = 0 implies a₁ in dyadic 0 ) & ( for b₁ being Nat st a₁ in dyadic (b₁ + 1) & not a₁ in dyadic b₁ holds
a₂ = b₁ + 1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines inf_number_dyadic URYSOHN3:def 3 :

theorem Th6: :: URYSOHN3:6

for b₁ being Real st b₁ in DYADIC holds
b₁ in dyadic (inf_number_dyadic b₁)

proof end;

theorem Th7: :: URYSOHN3:7

for b₁ being Real st b₁ in DYADIC holds
for b₂ being Nat st inf_number_dyadic b₁ <= b₂ holds
b₁ in dyadic b₂

proof end;

theorem Th8: :: URYSOHN3:8

for b₁ being Real
for b₂ being Nat st b₁ in dyadic b₂ holds
inf_number_dyadic b₁ <= b₂

proof end;

theorem Th9: :: URYSOHN3:9

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃
for b₅ being Real st b₅ in DYADIC holds
for b₆ being Nat holds (b₄ . (inf_number_dyadic b₅)) . b₅ = (b₄ . ((inf_number_dyadic b₅) + b₆)) . b₅

proof end;

theorem Th10: :: URYSOHN3:10

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃
for b₅ being Real st b₅ in DYADIC holds
ex b₆ being Subset of b₁ st
for b₇ being Nat st b₅ in dyadic b₇ holds
b₆ = (b₄ . b₇) . b₅

proof end;

theorem Th11: :: URYSOHN3:11

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃ ex b₅ being Function of DOM , bool the carrier of b₁ st
for b₆ being Real st b₆ in DOM holds
( ( b₆ in R<0 implies b₅ . b₆ = {} ) & ( b₆ in R>1 implies b₅ . b₆ = the carrier of b₁ ) & ( b₆ in DYADIC implies for b₇ being Nat st b₆ in dyadic b₇ holds
b₅ . b₆ = (b₄ . b₇) . b₆ ) )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Subset of c₁;
assume E15: ( c₁ is_T4 & c₂ <> {} & c₂ is closed & c₃ is closed & c₂ misses c₃ ) ;
let c₄ be Rain of c₂,c₃;
func Tempest c₄ -> Function of DOM , bool the carrier of a₁ means :Def4: :: URYSOHN3:def 4
for b₁ being Real st b₁ in DOM holds
( ( b₁ in R<0 implies a₅ . b₁ = {} ) & ( b₁ in R>1 implies a₅ . b₁ = the carrier of a₁ ) & ( b₁ in DYADIC implies for b₂ being Nat st b₁ in dyadic b₂ holds
a₅ . b₁ = (a₄ . b₂) . b₁ ) );
existence by E15, Th11;
uniqueness

proof end;

end;

:: deftheorem Def4 defines Tempest URYSOHN3:def 4 :

definition

let c₁ be non empty set ;
let c₂ be TopSpace;
let c₃ be Function of c₁, bool the carrier of c₂;
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Subset of a₂;
correctness

proof end;

end;

theorem Th12: :: URYSOHN3:12

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃
for b₅ being Real
for b₆ being Subset of b₁ st b₆ = (Tempest b₄) . b₅ & b₅ in DOM holds
b₆ is open

proof end;

theorem Th13: :: URYSOHN3:13

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃
for b₅, b₆ being Real st b₅ in DOM & b₆ in DOM & b₅ < b₆ holds
for b₇ being Subset of b₁ st b₇ = (Tempest b₄) . b₅ holds
Cl b₇ c= (Tempest b₄) . b₆

proof end;

theorem Th14: :: URYSOHN3:14

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Rain of b₂,b₃
for b₅ being Point of b₁ ex b₆ being Subset of ExtREAL st
for b₇ being set holds
( b₇ in b₆ iff ( b₇ in DYADIC & ( for b₈ being Real st b₈ = b₇ holds
not b₅ in (Tempest b₄) . b₈ ) ) )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Subset of c₁;
let c₄ be Rain of c₂,c₃;
let c₅ be Point of c₁;
func Rainbow c₅,c₄ -> Subset of ExtREAL means :Def5: :: URYSOHN3:def 5
for b₁ being set holds
( b₁ in a₆ iff ( b₁ in DYADIC & ( for b₂ being Real st b₂ = b₁ holds
not a₅ in (Tempest a₄) . b₂ ) ) );
existence by Th14;
uniqueness

proof end;

end;

:: deftheorem Def5 defines Rainbow URYSOHN3:def 5 :

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Function of c₁,c₂;
let c₄ be Point of c₁;
redefine func . as c₃ . c₄ -> Point of a₂;
correctness

proof end;

end;

theorem Th15: :: URYSOHN3:15

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Rain of b₂,b₃
for b₅ being Point of b₁ holds Rainbow b₅,b₄ c= DYADIC

proof end;

theorem Th16: :: URYSOHN3:16

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Rain of b₂,b₃ ex b₅ being Function of b₁,R^1 st
for b₆ being Point of b₁ holds
( ( Rainbow b₆,b₄ = {} implies b₅ . b₆ = 0 ) & ( for b₇ being non empty Subset of ExtREAL st b₇ = Rainbow b₆,b₄ holds
b₅ . b₆ = sup b₇ ) )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Subset of c₁;
let c₄ be Rain of c₂,c₃;
func Thunder c₄ -> Function of a₁,R^1 means :Def6: :: URYSOHN3:def 6
for b₁ being Point of a₁ holds
( ( Rainbow b₁,a₄ = {} implies a₅ . b₁ = 0 ) & ( for b₂ being non empty Subset of ExtREAL st b₂ = Rainbow b₁,a₄ holds
a₅ . b₁ = sup b₂ ) );
existence by Th16;
uniqueness

proof end;

end;

:: deftheorem Def6 defines Thunder URYSOHN3:def 6 :

definition

let c₁ be non empty TopSpace;
let c₂ be Function of c₁,R^1 ;
let c₃ be Point of c₁;
redefine func . as c₂ . c₃ -> Real;
correctness

proof end;

end;

theorem Th17: :: URYSOHN3:17

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Rain of b₂,b₃
for b₅ being Point of b₁
for b₆ being non empty Subset of ExtREAL st b₆ = Rainbow b₅,b₄ holds
for b₇ being R_eal st b₇ = 1 holds
( 0. <=' sup b₆ & sup b₆ <=' b₇ )

proof end;

theorem Th18: :: URYSOHN3:18

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃
for b₅ being Element of DOM
for b₆ being Point of b₁ st (Thunder b₄) . b₆ < b₅ holds
b₆ in (Tempest b₄) . b₅

proof end;

theorem Th19: :: URYSOHN3:19

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃
for b₅ being Real st b₅ in DYADIC \/ R>1 & 0 < b₅ holds
for b₆ being Point of b₁ st b₆ in (Tempest b₄) . b₅ holds
(Thunder b₄) . b₆ <= b₅

proof end;

theorem Th20: :: URYSOHN3:20

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃
for b₅ being Element of DOM st 0 < b₅ holds
for b₆ being Point of b₁ st b₅ < (Thunder b₄) . b₆ holds
not b₆ in (Tempest b₄) . b₅

proof end;

theorem Th21: :: URYSOHN3:21

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Rain of b₂,b₃ holds
( Thunder b₄ is continuous & ( for b₅ being Point of b₁ holds
( 0 <= (Thunder b₄) . b₅ & (Thunder b₄) . b₅ <= 1 & ( b₅ in b₂ implies (Thunder b₄) . b₅ = 0 ) & ( b₅ in b₃ implies (Thunder b₄) . b₅ = 1 ) ) ) )

proof end;

theorem Th22: :: URYSOHN3:22

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
ex b₄ being Function of b₁,R^1 st
( b₄ is continuous & ( for b₅ being Point of b₁ holds
( 0 <= b₄ . b₅ & b₄ . b₅ <= 1 & ( b₅ in b₂ implies b₄ . b₅ = 0 ) & ( b₅ in b₃ implies b₄ . b₅ = 1 ) ) ) )

proof end;

theorem Th23: :: URYSOHN3:23

for b₁ being non empty being_T4 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ misses b₃ holds
ex b₄ being Function of b₁,R^1 st
( b₄ is continuous & ( for b₅ being Point of b₁ holds
( 0 <= b₄ . b₅ & b₄ . b₅ <= 1 & ( b₅ in b₂ implies b₄ . b₅ = 0 ) & ( b₅ in b₃ implies b₄ . b₅ = 1 ) ) ) )

proof end;

theorem Th24: :: URYSOHN3:24

for b₁ being non empty compact being_T2 TopSpace
for b₂, b₃ being closed Subset of b₁ st b₂ misses b₃ holds
ex b₄ being Function of b₁,R^1 st
( b₄ is continuous & ( for b₅ being Point of b₁ holds
( 0 <= b₄ . b₅ & b₄ . b₅ <= 1 & ( b₅ in b₂ implies b₄ . b₅ = 0 ) & ( b₅ in b₃ implies b₄ . b₅ = 1 ) ) ) ) by Th23;