:: URYSOHN1 semantic presentation

definition

func R<0 -> Subset of REAL means :: URYSOHN1:def 1
for b₁ being Real holds
( b₁ in a₁ iff b₁ < 0 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines R<0 URYSOHN1:def 1 :

definition

func R>1 -> Subset of REAL means :: URYSOHN1:def 2
for b₁ being Real holds
( b₁ in a₁ iff 1 < b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines R>1 URYSOHN1:def 2 :

definition

let c₁ be Nat;
func dyadic c₁ -> Subset of REAL means :Def3: :: URYSOHN1:def 3
for b₁ being Real holds
( b₁ in a₂ iff ex b₂ being Nat st
( 0 <= b₂ & b₂ <= 2 |^ a₁ & b₁ = b₂ / (2 |^ a₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines dyadic URYSOHN1:def 3 :

definition

func DYADIC -> Subset of REAL means :Def4: :: URYSOHN1:def 4
for b₁ being Real holds
( b₁ in a₁ iff ex b₂ being Nat st b₁ in dyadic b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines DYADIC URYSOHN1:def 4 :

definition

func DOM -> Subset of REAL equals :: URYSOHN1:def 5
(R<0 \/ DYADIC ) \/ R>1 ;
coherence ;

end;

:: deftheorem Def5 defines DOM URYSOHN1:def 5 :

definition

let c₁ be TopSpace;
let c₂ be non empty Subset of REAL ;
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₁;
coherence

proof end;

end;

theorem Th1: :: URYSOHN1:1

canceled;

theorem Th2: :: URYSOHN1:2

canceled;

theorem Th3: :: URYSOHN1:3

canceled;

theorem Th4: :: URYSOHN1:4

canceled;

theorem Th5: :: URYSOHN1:5

for b₁ being Nat
for b₂ being Real st b₂ in dyadic b₁ holds
( 0 <= b₂ & b₂ <= 1 )

proof end;

theorem Th6: :: URYSOHN1:6

dyadic 0 = {0,1}

proof end;

theorem Th7: :: URYSOHN1:7

dyadic 1 = {0,(1 / 2),1}

proof end;

registration

let c₁ be Nat;
cluster dyadic a₁ -> non empty ;
coherence

proof end;

end;

theorem Th8: :: URYSOHN1:8

canceled;

theorem Th9: :: URYSOHN1:9

for b₁ being Nat ex b₂ being FinSequence st
( dom b₂ = Seg ((2 |^ b₁) + 1) & ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = (b₃ - 1) / (2 |^ b₁) ) )

proof end;

definition

let c₁ be Nat;
func dyad c₁ -> FinSequence means :Def6: :: URYSOHN1:def 6
( dom a₂ = Seg ((2 |^ a₁) + 1) & ( for b₁ being Nat st b₁ in dom a₂ holds
a₂ . b₁ = (b₁ - 1) / (2 |^ a₁) ) );
existence by Th9;
uniqueness

proof end;

end;

:: deftheorem Def6 defines dyad URYSOHN1:def 6 :

theorem Th10: :: URYSOHN1:10

for b₁ being Nat holds
( dom (dyad b₁) = Seg ((2 |^ b₁) + 1) & rng (dyad b₁) = dyadic b₁ )

proof end;

registration

cluster DYADIC -> non empty ;
coherence

proof end;

end;

registration

cluster DOM -> non empty ;
coherence

proof end;

end;

theorem Th11: :: URYSOHN1:11

for b₁ being Nat holds dyadic b₁ c= dyadic (b₁ + 1)

proof end;

theorem Th12: :: URYSOHN1:12

for b₁ being Nat holds
( 0 in dyadic b₁ & 1 in dyadic b₁ )

proof end;

theorem Th13: :: URYSOHN1:13

for b₁, b₂ being Nat st 0 < b₂ & b₂ <= 2 |^ b₁ holds
((b₂ * 2) - 1) / (2 |^ (b₁ + 1)) in (dyadic (b₁ + 1)) \ (dyadic b₁)

proof end;

theorem Th14: :: URYSOHN1:14

for b₁, b₂ being Nat st 0 <= b₂ & b₂ < 2 |^ b₁ holds
((b₂ * 2) + 1) / (2 |^ (b₁ + 1)) in (dyadic (b₁ + 1)) \ (dyadic b₁)

proof end;

theorem Th15: :: URYSOHN1:15

for b₁ being Nat holds 1 / (2 |^ (b₁ + 1)) in (dyadic (b₁ + 1)) \ (dyadic b₁)

proof end;

definition

let c₁ be Nat;
let c₂ be Element of dyadic c₁;
func axis c₂,c₁ -> Nat means :Def7: :: URYSOHN1:def 7
a₂ = a₃ / (2 |^ a₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines axis URYSOHN1:def 7 :

theorem Th16: :: URYSOHN1:16

for b₁ being Nat
for b₂ being Element of dyadic b₁ holds
( b₂ = (axis b₂,b₁) / (2 |^ b₁) & 0 <= axis b₂,b₁ & axis b₂,b₁ <= 2 |^ b₁ )

proof end;

theorem Th17: :: URYSOHN1:17

for b₁ being Nat
for b₂ being Element of dyadic b₁ holds
( ((axis b₂,b₁) - 1) / (2 |^ b₁) < b₂ & b₂ < ((axis b₂,b₁) + 1) / (2 |^ b₁) )

proof end;

theorem Th18: :: URYSOHN1:18

for b₁ being Nat
for b₂ being Element of dyadic b₁ holds ((axis b₂,b₁) - 1) / (2 |^ b₁) < ((axis b₂,b₁) + 1) / (2 |^ b₁)

proof end;

theorem Th19: :: URYSOHN1:19

canceled;

theorem Th20: :: URYSOHN1:20

for b₁ being Nat
for b₂ being Element of dyadic (b₁ + 1) st not b₂ in dyadic b₁ holds
( ((axis b₂,(b₁ + 1)) - 1) / (2 |^ (b₁ + 1)) in dyadic b₁ & ((axis b₂,(b₁ + 1)) + 1) / (2 |^ (b₁ + 1)) in dyadic b₁ )

proof end;

theorem Th21: :: URYSOHN1:21

for b₁ being Nat
for b₂, b₃ being Element of dyadic b₁ st b₂ < b₃ holds
axis b₂,b₁ < axis b₃,b₁

proof end;

theorem Th22: :: URYSOHN1:22

for b₁ being Nat
for b₂, b₃ being Element of dyadic b₁ st b₂ < b₃ holds
( b₂ <= ((axis b₃,b₁) - 1) / (2 |^ b₁) & ((axis b₂,b₁) + 1) / (2 |^ b₁) <= b₃ )

proof end;

theorem Th23: :: URYSOHN1:23

for b₁ being Nat
for b₂, b₃ being Element of dyadic (b₁ + 1) st b₂ < b₃ & not b₂ in dyadic b₁ & not b₃ in dyadic b₁ holds
((axis b₂,(b₁ + 1)) + 1) / (2 |^ (b₁ + 1)) <= ((axis b₃,(b₁ + 1)) - 1) / (2 |^ (b₁ + 1))

proof end;

notation

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
synonym Nbhd of c₂,c₁ for a_neighborhood of c₂;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
redefine mode a_neighborhood of c₂ -> Element of bool the carrier of a₁ means :: URYSOHN1:def 8
ex b₁ being Subset of a₁ st
( b₁ is open & a₂ in b₁ & b₁ c= a₃ );
compatibility

proof end;

end;

:: deftheorem Def8 defines Nbhd URYSOHN1:def 8 :

theorem Th24: :: URYSOHN1:24

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is open iff for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being Nbhd of b₃,b₁ st b₄ c= b₂ )

proof end;

theorem Th25: :: URYSOHN1:25

canceled;

theorem Th26: :: URYSOHN1:26

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st ( for b₃ being Point of b₁ st b₃ in b₂ holds
b₂ is Nbhd of b₃,b₁ ) holds
b₂ is open

proof end;

definition

let c₁ be TopStruct ;
attr a₁ is being_T1 means :Def9: :: URYSOHN1:def 9
for b₁, b₂ being Point of a₁ st not b₁ = b₂ holds
ex b₃, b₄ being Subset of a₁ st
( b₃ is open & b₄ is open & b₁ in b₃ & not b₂ in b₃ & b₂ in b₄ & not b₁ in b₄ );

end;

:: deftheorem Def9 defines being_T1 URYSOHN1:def 9 :

notation

let c₁ be TopStruct ;
synonym c₁ is_T1 for being_T1 c₁;

end;

theorem Th27: :: URYSOHN1:27

for b₁ being non empty TopSpace holds
( b₁ is_T1 iff for b₂ being Point of b₁ holds {b₂} is closed )

proof end;

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;
coherence by FUNCT_2:7, TOPMETR:24;

end;

theorem Th28: :: URYSOHN1:28

for b₁ being non empty TopSpace st b₁ is_T4 holds
for b₂, b₃ being open Subset of b₁ st b₂ <> {} & Cl b₂ c= b₃ holds
ex b₄ being Subset of b₁ st
( b₄ <> {} & b₄ is open & Cl b₂ c= b₄ & Cl b₄ c= b₃ )

proof end;

theorem Th29: :: URYSOHN1:29

for b₁ being TopSpace holds
( b₁ is_T3 iff for b₂ being open Subset of b₁
for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being open Subset of b₁ st
( b₃ in b₄ & Cl b₄ c= b₂ ) )

proof end;

theorem Th30: :: URYSOHN1:30

for b₁ being non empty TopSpace st b₁ is_T4 & b₁ is_T1 holds
for b₂ being open Subset of b₁ st b₂ <> {} holds
ex b₃ being Subset of b₁ st
( b₃ <> {} & Cl b₃ c= b₂ )

proof end;

theorem Th31: :: URYSOHN1:31

for b₁ being non empty TopSpace st b₁ is_T4 holds
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is closed & b₃ <> {} & b₃ c= b₂ holds
ex b₄ being Subset of b₁ st
( b₄ is open & b₃ c= b₄ & Cl b₄ c= b₂ )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Subset of c₁;
assume E23: ( c₁ is_T4 & c₂ <> {} & c₂ is open & c₃ is open & Cl c₂ c= c₃ ) ;
mode Between of c₂,c₃ -> Subset of a₁ means :Def10: :: URYSOHN1:def 10
( a₄ <> {} & a₄ is open & Cl a₂ c= a₄ & Cl a₄ c= a₃ );
existence by E23, Th28;

end;

:: deftheorem Def10 defines Between URYSOHN1:def 10 :

theorem Th32: :: URYSOHN1:32

for b₁ being non empty TopSpace st b₁ is_T4 holds
for b₂, b₃ being closed Subset of b₁ st b₂ <> {} & b₂ misses b₃ holds
for b₄ being Nat
for 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₇ ) ) holds
ex b₆ being Function of dyadic (b₄ + 1), bool the carrier of b₁ st
( b₂ c= b₆ . 0 & b₃ = ([#] b₁) \ (b₆ . 1) & ( for b₇, b₈, b₉ being Element of dyadic (b₄ + 1) st b₇ < b₈ holds
( b₆ . b₇ is open & b₆ . b₈ is open & Cl (b₆ . b₇) c= b₆ . b₈ & ( b₉ in dyadic b₄ implies b₆ . b₉ = b₅ . b₉ ) ) ) )

proof end;