:: URYSOHN1 semantic presentation

definition

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

proof end;

uniqueness

proof end;

end;

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

definition

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

proof end;

uniqueness

proof end;

end;

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

definition

let n be Nat;
func dyadic n -> Subset of REAL means :Def3: :: URYSOHN1:def 3
for x being Real holds
( x in it iff ex i being Nat st
( 0 <= i & i <= 2 |^ n & x = i / (2 |^ n) ) );
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 a being Real holds
( a in it iff ex n being Nat st a in dyadic n );
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 defines DOM URYSOHN1:def 5 :

definition

let T be TopSpace;
let A be non empty Subset of REAL ;
let F be Function of A, bool the carrier of T;
let r be Element of A;
:: original: .
redefine func F . r -> Subset of T;
coherence

proof end;

end;

theorem :: URYSOHN1:1

canceled;

theorem :: URYSOHN1:2

canceled;

theorem :: URYSOHN1:3

canceled;

theorem :: URYSOHN1:4

canceled;

theorem Th5: :: URYSOHN1:5

for n being Nat
for x being Real st x in dyadic n holds
( 0 <= x & x <= 1 )

proof end;

theorem Th6: :: URYSOHN1:6

dyadic 0 = {0,1}

proof end;

theorem :: URYSOHN1:7

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

proof end;

registration

let n be Nat;
cluster dyadic n -> non empty ;
coherence

proof end;

end;

theorem :: URYSOHN1:8

canceled;

theorem Th9: :: URYSOHN1:9

for n being Nat ex FS being FinSequence st
( dom FS = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom FS holds
FS . i = (i - 1) / (2 |^ n) ) )

proof end;

definition

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

proof end;

end;

:: deftheorem Def6 defines dyad URYSOHN1:def 6 :

theorem :: URYSOHN1:10

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

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 n being Nat holds dyadic n c= dyadic (n + 1)

proof end;

theorem Th12: :: URYSOHN1:12

for n being Nat holds
( 0 in dyadic n & 1 in dyadic n )

proof end;

theorem Th13: :: URYSOHN1:13

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

proof end;

theorem Th14: :: URYSOHN1:14

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

proof end;

theorem Th15: :: URYSOHN1:15

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

proof end;

definition

let n be Nat;
let x be Element of dyadic n;
func axis x,n -> Nat means :Def7: :: URYSOHN1:def 7
x = it / (2 |^ n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines axis URYSOHN1:def 7 :

theorem Th16: :: URYSOHN1:16

for n being Nat
for x being Element of dyadic n holds
( x = (axis x,n) / (2 |^ n) & 0 <= axis x,n & axis x,n <= 2 |^ n )

proof end;

theorem :: URYSOHN1:17

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

proof end;

theorem Th18: :: URYSOHN1:18

for n being Nat
for x being Element of dyadic n holds ((axis x,n) - 1) / (2 |^ n) < ((axis x,n) + 1) / (2 |^ n)

proof end;

theorem :: URYSOHN1:19

canceled;

theorem Th20: :: URYSOHN1:20

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

proof end;

theorem Th21: :: URYSOHN1:21

for n being Nat
for x1, x2 being Element of dyadic n st x1 < x2 holds
axis x1,n < axis x2,n

proof end;

theorem Th22: :: URYSOHN1:22

for n being Nat
for x1, x2 being Element of dyadic n st x1 < x2 holds
( x1 <= ((axis x2,n) - 1) / (2 |^ n) & ((axis x1,n) + 1) / (2 |^ n) <= x2 )

proof end;

theorem Th23: :: URYSOHN1:23

for n being Nat
for x1, x2 being Element of dyadic (n + 1) st x1 < x2 & not x1 in dyadic n & not x2 in dyadic n holds
((axis x1,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 1) / (2 |^ (n + 1))

proof end;

notation

let T be non empty TopSpace;
let x be Point of T;
synonym Nbhd of x,T for a_neighborhood of x;

end;

definition

let T be non empty TopSpace;
let x be Point of T;
redefine mode a_neighborhood of x means :: URYSOHN1:def 8
ex A being Subset of T st
( A is open & x in A & A c= it );
compatibility

proof end;

end;

:: deftheorem defines Nbhd URYSOHN1:def 8 :

theorem Th24: :: URYSOHN1:24

for T being non empty TopSpace
for A being Subset of T holds
( A is open iff for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A )

proof end;

theorem :: URYSOHN1:25

canceled;

theorem :: URYSOHN1:26

for T being non empty TopSpace
for A being Subset of T st ( for x being Point of T st x in A holds
A is Nbhd of x,T ) holds
A is open

proof end;

definition

let T be TopStruct ;
attr T is being_T1 means :Def9: :: URYSOHN1:def 9
for p, q being Point of T st not p = q holds
ex W, V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V );

end;

:: deftheorem Def9 defines being_T1 URYSOHN1:def 9 :

notation

let T be TopStruct ;
synonym T is_T1 for being_T1 T;

end;

theorem Th27: :: URYSOHN1:27

for T being non empty TopSpace holds
( T is_T1 iff for p being Point of T holds {p} is closed )

proof end;

definition

let T be non empty TopSpace;
let F be Function of T,R^1 ;
let x be Point of T;
:: original: .
redefine func F . x -> Real;
coherence by FUNCT_2:7, TOPMETR:24;

end;

theorem Th28: :: URYSOHN1:28

for T being non empty TopSpace st T is_T4 holds
for A, B being open Subset of T st A <> {} & Cl A c= B holds
ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )

proof end;

theorem :: URYSOHN1:29

for T being TopSpace holds
( T is_T3 iff for A being open Subset of T
for p being Point of T st p in A holds
ex B being open Subset of T st
( p in B & Cl B c= A ) )

proof end;

theorem :: URYSOHN1:30

for T being non empty TopSpace st T is_T4 & T is_T1 holds
for A being open Subset of T st A <> {} holds
ex B being Subset of T st
( B <> {} & Cl B c= A )

proof end;

theorem :: URYSOHN1:31

for T being non empty TopSpace st T is_T4 holds
for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds
ex C being Subset of T st
( C is open & B c= C & Cl C c= A )

proof end;

definition

let T be non empty TopSpace;
let A, B be Subset of T;
assume A1: ( T is_T4 & A <> {} & A is open & B is open & Cl A c= B ) ;
mode Between of A,B -> Subset of T means :Def10: :: URYSOHN1:def 10
( it <> {} & it is open & Cl A c= it & Cl it c= B );
existence by A1, Th28;

end;

:: deftheorem Def10 defines Between URYSOHN1:def 10 :

theorem :: URYSOHN1:32

for T being non empty TopSpace st T is_T4 holds
for A, B being closed Subset of T st A <> {} & A misses B holds
for n being Nat
for 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 ) ) holds
ex F being Function of dyadic (n + 1), bool the carrier of T st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) )

proof end;