:: TOPGEN_5 semantic presentation

theorem Th1: :: TOPGEN_5:1

for f, g being Function st f tolerates g holds
for A being set holds (f +* g) " A = (f " A) \/ (g " A)

proof end;

theorem :: TOPGEN_5:2

for f, g being Function st dom f misses dom g holds
for A being set holds (f +* g) " A = (f " A) \/ (g " A)

proof end;

registration

let X be set ;
let Y be real-membered set ;
cluster -> real-yielding Relation of X,Y;
coherence

proof end;

end;

theorem Th3: :: TOPGEN_5:3

for x, a being set
for f being Function st a in dom f holds
(commute (x .--> f)) . a = x .--> (f . a)

proof end;

theorem :: TOPGEN_5:4

for b being set
for f being Function holds
( b in dom (commute f) iff ex a being set ex g being Function st
( a in dom f & g = f . a & b in dom g ) )

proof end;

theorem Th5: :: TOPGEN_5:5

for a, b being set
for f being Function holds
( a in dom ((commute f) . b) iff ex g being Function st
( a in dom f & g = f . a & b in dom g ) )

proof end;

theorem Th6: :: TOPGEN_5:6

for a, b being set
for f, g being Function st a in dom f & g = f . a & b in dom g holds
((commute f) . b) . a = g . b

proof end;

theorem Th7: :: TOPGEN_5:7

for a being set
for f, g, h being Function st h = f \/ g holds
(commute h) . a = ((commute f) . a) \/ ((commute g) . a)

proof end;

registration

cluster finite -> finite bounded Element of bool REAL ;
coherence

proof end;

end;

theorem Th8: :: TOPGEN_5:8

for a, b, c, d being real number st a < b & c <= d holds
].a,c.[ /\ [.b,d.] = [.b,c.[

proof end;

theorem Th9: :: TOPGEN_5:9

for a, b, c, d being real number st a >= b & c > d holds
].a,c.[ /\ [.b,d.] = ].a,d.]

proof end;

theorem Th10: :: TOPGEN_5:10

for a, b, c, d being real number st a <= b & b < c & c <= d holds
[.a,c.[ \/ ].b,d.] = [.a,d.]

proof end;

theorem Th11: :: TOPGEN_5:11

for a, b, c, d being real number st a <= b & b < c & c <= d holds
[.a,c.[ /\ ].b,d.] = ].b,c.[

proof end;

theorem Th12: :: TOPGEN_5:12

for X, Y being set holds
( product <*X,Y*>,[:X,Y:] are_equipotent & Card (product <*X,Y*>) = (Card X) *` (Card Y) )

proof end;

scheme :: TOPGEN_5:sch 1
SCH1{ P₁[ set ], F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set ) -> set , F₅( set ) -> set } :

ex f being Function of F₃(),F₂() st
for a being Element of F₁() st a in F₃() holds
( ( P₁[a] implies f . a = F₄(a) ) & ( P₁[a] implies f . a = F₅(a) ) )

provided

A1: F₃() c= F₁() and
A2: for a being Element of F₁() st a in F₃() holds
( ( P₁[a] implies F₄(a) in F₂() ) & ( P₁[a] implies F₅(a) in F₂() ) )

proof end;

scheme :: TOPGEN_5:sch 2
SCH2{ P₁[ set ], P₂[ set ], F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set ) -> set , F₅( set ) -> set , F₆( set ) -> set } :

ex f being Function of F₃(),F₂() st
for a being Element of F₁() st a in F₃() holds
( ( P₁[a] implies f . a = F₄(a) ) & ( P₁[a] & P₂[a] implies f . a = F₅(a) ) & ( P₁[a] & P₂[a] implies f . a = F₆(a) ) )

provided

A1: F₃() c= F₁() and
A2: for a being Element of F₁() st a in F₃() holds
( ( P₁[a] implies F₄(a) in F₂() ) & ( P₁[a] & P₂[a] implies F₅(a) in F₂() ) & ( P₁[a] & P₂[a] implies F₆(a) in F₂() ) )

proof end;

theorem Th13: :: TOPGEN_5:13

for a, b being real number holds |.|[a,b]|.| ^2 = (a ^2 ) + (b ^2 )

proof end;

theorem Th14: :: TOPGEN_5:14

for X being TopSpace
for Y being non empty TopSpace
for A, B being closed Subset of X
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y st f tolerates g holds
f +* g is continuous Function of (X | (A \/ B)),Y

proof end;

theorem Th15: :: TOPGEN_5:15

for X being TopSpace
for Y being non empty TopSpace
for A, B being closed Subset of X st A misses B holds
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y holds f +* g is continuous Function of (X | (A \/ B)),Y

proof end;

theorem Th16: :: TOPGEN_5:16

for X being TopSpace
for Y being non empty TopSpace
for A being open closed Subset of X
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | (A ` )),Y holds f +* g is continuous Function of X,Y

proof end;

theorem Th17: :: TOPGEN_5:17

for n being Nat
for a being Point of (TOP-REAL n)
for r being real positive number holds a in Ball a,r

proof end;

definition

func y=0-line -> Subset of (TOP-REAL 2) equals :: TOPGEN_5:def 1
{ |[x,0]| where x is Element of REAL : verum } ;
coherence

proof end;

func y>=0-plane -> Subset of (TOP-REAL 2) equals :: TOPGEN_5:def 2
{ |[x,y]| where x, y is Element of REAL : y >= 0 } ;
coherence

proof end;

end;

:: deftheorem defines y=0-line TOPGEN_5:def 1 :

:: deftheorem defines y>=0-plane TOPGEN_5:def 2 :

theorem :: TOPGEN_5:18

for a, b being set holds
( <*a,b*> in y=0-line iff ( a in REAL & b = 0 ) )

proof end;

theorem Th19: :: TOPGEN_5:19

for a, b being real number holds
( |[a,b]| in y=0-line iff b = 0 )

proof end;

theorem Th20: :: TOPGEN_5:20

Card y=0-line = continuum

proof end;

theorem :: TOPGEN_5:21

for a, b being set holds
( <*a,b*> in y>=0-plane iff ( a in REAL & ex y being Element of REAL st
( b = y & y >= 0 ) ) )

proof end;

theorem Th22: :: TOPGEN_5:22

for a, b being real number holds
( |[a,b]| in y>=0-plane iff b >= 0 )

proof end;

registration

cluster y=0-line -> non empty ;
coherence by Th19;
cluster y>=0-plane -> non empty ;
coherence by Th22;

end;

theorem Th23: :: TOPGEN_5:23

y=0-line c= y>=0-plane

proof end;

theorem Th24: :: TOPGEN_5:24

for a, b, r being real number st r > 0 holds
( Ball |[a,b]|,r c= y>=0-plane iff r <= b )

proof end;

theorem Th25: :: TOPGEN_5:25

for a, b, r being real number st r > 0 & b >= 0 holds
( Ball |[a,b]|,r misses y=0-line iff r <= b )

proof end;

theorem Th26: :: TOPGEN_5:26

for n being Nat
for a, b being Element of (TOP-REAL n)
for r1, r2 being real positive number st |.(a - b).| <= r1 - r2 holds
Ball b,r2 c= Ball a,r1

proof end;

theorem Th27: :: TOPGEN_5:27

for a being real number
for r1, r2 being real positive number st r1 <= r2 holds
Ball |[a,r1]|,r1 c= Ball |[a,r2]|,r2

proof end;

theorem Th28: :: TOPGEN_5:28

for T1, T2 being non empty TopSpace
for B1 being Neighborhood_System of T1
for B2 being Neighborhood_System of T2 st B1 = B2 holds
TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #)

proof end;

definition

func Niemytzki-plane -> non empty strict TopSpace means :Def3: :: TOPGEN_5:def 3
( the carrier of it = y>=0-plane & ex B being Neighborhood_System of it st
( ( for x being Element of REAL holds B . |[x,0]| = { ((Ball |[x,r]|,r) \/ {|[x,0]|}) where r is Element of REAL : r > 0 } ) & ( for x, y being Element of REAL st y > 0 holds
B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Niemytzki-plane TOPGEN_5:def 3 :

theorem Th29: :: TOPGEN_5:29

y>=0-plane \ y=0-line is open Subset of Niemytzki-plane

proof end;

Lm1: the carrier of Niemytzki-plane = y>=0-plane
by Def3;

theorem Th30: :: TOPGEN_5:30

y=0-line is closed Subset of Niemytzki-plane

proof end;

theorem Th31: :: TOPGEN_5:31

for x being real number
for r being real positive number holds (Ball |[x,r]|,r) \/ {|[x,0]|} is open Subset of Niemytzki-plane

proof end;

theorem Th32: :: TOPGEN_5:32

for x being real number
for y, r being real positive number holds (Ball |[x,y]|,r) /\ y>=0-plane is open Subset of Niemytzki-plane

proof end;

theorem Th33: :: TOPGEN_5:33

for x, y being real number
for r being real positive number st r <= y holds
Ball |[x,y]|,r is open Subset of Niemytzki-plane

proof end;

theorem Th34: :: TOPGEN_5:34

for p being Point of Niemytzki-plane
for r being real positive number ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )

proof end;

theorem Th35: :: TOPGEN_5:35

for x, y being real number
for r being real positive number ex w, v being rational number st
( |[w,v]| in Ball |[x,y]|,r & |[w,v]| <> |[x,y]| )

proof end;

theorem Th36: :: TOPGEN_5:36

for A being Subset of Niemytzki-plane st A = (y>=0-plane \ y=0-line ) /\ (product <*RAT ,RAT *>) holds
for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane

proof end;

theorem Th37: :: TOPGEN_5:37

for A being Subset of Niemytzki-plane st A = y>=0-plane \ y=0-line holds
for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane

proof end;

theorem Th38: :: TOPGEN_5:38

for A being Subset of Niemytzki-plane st A = y>=0-plane \ y=0-line holds
Cl A = [#] Niemytzki-plane

proof end;

theorem Th39: :: TOPGEN_5:39

for A being Subset of Niemytzki-plane st A = y=0-line holds
( Cl A = A & Int A = {} )

proof end;

theorem Th40: :: TOPGEN_5:40

(y>=0-plane \ y=0-line ) /\ (product <*RAT ,RAT *>) is dense Subset of Niemytzki-plane

proof end;

theorem :: TOPGEN_5:41

(y>=0-plane \ y=0-line ) /\ (product <*RAT ,RAT *>) is dense-in-itself Subset of Niemytzki-plane

proof end;

theorem :: TOPGEN_5:42

y>=0-plane \ y=0-line is dense Subset of Niemytzki-plane

proof end;

theorem :: TOPGEN_5:43

y>=0-plane \ y=0-line is dense-in-itself Subset of Niemytzki-plane

proof end;

theorem :: TOPGEN_5:44

y=0-line is nowhere_dense Subset of Niemytzki-plane

proof end;

theorem Th45: :: TOPGEN_5:45

for A being Subset of Niemytzki-plane st A = y=0-line holds
Der A is empty

proof end;

theorem Th46: :: TOPGEN_5:46

for A being Subset of y=0-line holds A is closed Subset of Niemytzki-plane

proof end;

theorem Th47: :: TOPGEN_5:47

RAT is dense Subset of Sorgenfrey-line

proof end;

theorem :: TOPGEN_5:48

Sorgenfrey-line is separable

proof end;

theorem :: TOPGEN_5:49

Niemytzki-plane is separable

proof end;

theorem :: TOPGEN_5:50

Niemytzki-plane is_T1

proof end;

theorem :: TOPGEN_5:51

not Niemytzki-plane is being_T4

proof end;

definition

let T be TopSpace;
attr T is Tychonoff means :Def4: :: TOPGEN_5:def 4
( T is_T1 & ( for A being closed Subset of T
for a being Point of T st a in A ` holds
ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} ) ) );

end;

:: deftheorem Def4 defines Tychonoff TOPGEN_5:def 4 :

registration

cluster Tychonoff -> being_T1 being_T3 TopStruct ;
coherence

proof end;

cluster non empty being_T1 being_T4 -> non empty Tychonoff TopStruct ;
coherence

proof end;

end;

theorem :: TOPGEN_5:52

for X being being_T1 TopSpace st X is Tychonoff holds
for B being prebasis of X
for x being Point of X
for V being Subset of X st x in V & V in B holds
ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} )

proof end;

registration

let X be set ;
let Y be non empty real-membered set ;
cluster -> real-yielding Relation of X,Y;
coherence ;

end;

theorem Th53: :: TOPGEN_5:53

for X being TopSpace
for R being non empty SubSpace of R^1
for f, g being continuous Function of X,R
for A being Subset of X st ( for x being Point of X holds
( x in A iff f . x <= g . x ) ) holds
A is closed

proof end;

theorem Th54: :: TOPGEN_5:54

for X being TopSpace
for R being non empty SubSpace of R^1
for f, g being continuous Function of X,R ex h being continuous Function of X,R st
for x being Point of X holds h . x = max (f . x),(g . x)

proof end;

theorem Th55: :: TOPGEN_5:55

for X being non empty TopSpace
for R being non empty SubSpace of R^1
for A being non empty finite set
for F being ManySortedFunction of A st ( for a being set st a in A holds
F . a is continuous Function of X,R ) holds
ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds
f . x = max S

proof end;

theorem Th56: :: TOPGEN_5:56

for X being non empty being_T1 TopSpace
for B being prebasis of X st ( for x being Point of X
for V being Subset of X st x in V & V in B holds
ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} ) ) holds
X is Tychonoff

proof end;

theorem Th57: :: TOPGEN_5:57

Sorgenfrey-line is_T1

proof end;

theorem Th58: :: TOPGEN_5:58

for x being real number holds left_open_halfline x is closed Subset of Sorgenfrey-line

proof end;

theorem :: TOPGEN_5:59

for x being real number holds left_closed_halfline x is closed Subset of Sorgenfrey-line

proof end;

theorem Th60: :: TOPGEN_5:60

for x being real number holds right_closed_halfline x is closed Subset of Sorgenfrey-line

proof end;

theorem Th61: :: TOPGEN_5:61

for x, y being real number holds [.x,y.[ is closed Subset of Sorgenfrey-line

proof end;

theorem Th62: :: TOPGEN_5:62

for x being real number
for w being rational number st x < w holds
ex f being continuous Function of Sorgenfrey-line ,I[01] st
for a being Point of Sorgenfrey-line holds
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )

proof end;

theorem :: TOPGEN_5:63

Sorgenfrey-line is Tychonoff

proof end;

definition

let x be real number ;
let r be real positive number ;
func + x,r -> Function of Niemytzki-plane ,I[01] means :Def5: :: TOPGEN_5:def 5
( it . |[x,0]| = 0 & ( for a being real number
for b being real non negative number holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball |[x,r]|,r implies it . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,r]|,r implies it . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + TOPGEN_5:def 5 :

theorem Th64: :: TOPGEN_5:64

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds
for x being real number
for r being real positive number st (+ x,r) . p = 0 holds
p = |[x,0]|

proof end;

theorem Th65: :: TOPGEN_5:65

for x, y being real number
for r being real positive number st x <> y holds
(+ x,r) . |[y,0]| = 1

proof end;

theorem Th66: :: TOPGEN_5:66

for p being Point of (TOP-REAL 2)
for x being real number
for a, r being real positive number st a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 holds
(+ x,r) . p = a

proof end;

theorem Th67: :: TOPGEN_5:67

for p being Point of (TOP-REAL 2)
for x, a being real number
for r being real positive number st 0 <= a & a <= 1 & |.(p - |[x,(r * a)]|).| < r * a holds
(+ x,r) . p < a

proof end;

theorem Th68: :: TOPGEN_5:68

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds
for x, a being real number
for r being real positive number st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ x,r) . p > a

proof end;

theorem Th69: :: TOPGEN_5:69

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds
for x, a, b being real number
for r being real positive number st 0 <= a & b <= 1 & (+ x,r) . p in ].a,b.[ holds
ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,b.[ )

proof end;

theorem Th70: :: TOPGEN_5:70

for x being real number
for a, r being real positive number holds Ball |[x,(r * a)]|,(r * a) c= (+ x,r) " ].0,a.[

proof end;

theorem Th71: :: TOPGEN_5:71

for x being real number
for a, r being real positive number holds (Ball |[x,(r * a)]|,(r * a)) \/ {|[x,0]|} c= (+ x,r) " [.0,a.[

proof end;

theorem Th72: :: TOPGEN_5:72

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds
for x, a being real number
for r being real positive number st 0 < (+ x,r) . p & (+ x,r) . p < a & a <= 1 holds
p in Ball |[x,(r * a)]|,(r * a)

proof end;

theorem Th73: :: TOPGEN_5:73

for p being Point of (TOP-REAL 2) st p `2 > 0 holds
for x, a being real number
for r being real positive number st 0 <= a & a < (+ x,r) . p holds
ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] )

proof end;

theorem Th74: :: TOPGEN_5:74

for p being Point of (TOP-REAL 2) st p `2 = 0 holds
for x being real number
for r being real positive number st (+ x,r) . p = 1 holds
ex r1 being real positive number st (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,r) " {1}

proof end;

theorem Th75: :: TOPGEN_5:75

for T being non empty TopSpace
for S being SubSpace of T
for B being Basis of T holds { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } is Basis of S

proof end;

theorem Th76: :: TOPGEN_5:76

{ ].a,b.[ where a, b is Real : a < b } is Basis of R^1

proof end;

theorem Th77: :: TOPGEN_5:77

for T being TopSpace
for U, V being Subset of T
for B being set st U in B & V in B & B \/ {(U \/ V)} is Basis of T holds
B is Basis of T

proof end;

theorem Th78: :: TOPGEN_5:78

({ [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } is Basis of I[01]

proof end;

theorem Th79: :: TOPGEN_5:79

for T being non empty TopSpace
for f being Function of T,I[01] holds
( f is continuous iff for a, b being real number st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0,b.[ is open & f " ].a,1.] is open ) )

proof end;

registration

let x be real number ;
let r be real positive number ;
cluster + x,r -> continuous real-yielding ;
coherence

proof end;

end;

theorem Th80: :: TOPGEN_5:80

for U being Subset of Niemytzki-plane
for x being Element of REAL
for r being real positive number st U = (Ball |[x,r]|,r) \/ {|[x,0]|} holds
ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,0]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0]|} implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) )

proof end;

definition

let x, y be real number ;
let r be real positive number ;
func + x,y,r -> Function of Niemytzki-plane ,I[01] means :Def6: :: TOPGEN_5:def 6
for a being real number
for b being real non negative number holds
( ( not |[a,b]| in Ball |[x,y]|,r implies it . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,y]|,r implies it . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines + TOPGEN_5:def 6 :

theorem Th81: :: TOPGEN_5:81

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds
for x being real number
for y being real non negative number
for r being real positive number holds
( (+ x,y,r) . p = 0 iff p = |[x,y]| )

proof end;

theorem Th82: :: TOPGEN_5:82

for x being real number
for y being real non negative number
for r, a being real positive number st a <= 1 holds
(+ x,y,r) " [.0,a.[ = (Ball |[x,y]|,(r * a)) /\ y>=0-plane

proof end;

theorem Th83: :: TOPGEN_5:83

for p being Point of (TOP-REAL 2) st p `2 > 0 holds
for x being real number
for a being real non negative number
for y, r being real positive number st (+ x,y,r) . p > a holds
( |.(|[x,y]| - p).| > r * a & (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane c= (+ x,y,r) " ].a,1.] )

proof end;

theorem Th84: :: TOPGEN_5:84

for p being Point of (TOP-REAL 2) st p `2 = 0 holds
for x being real number
for a being real non negative number
for y, r being real positive number st (+ x,y,r) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,y,r) " ].a,1.] ) )

proof end;

registration

let x be real number ;
let y, r be real positive number ;
cluster + x,y,r -> continuous real-yielding ;
coherence

proof end;

end;

theorem Th85: :: TOPGEN_5:85

for U being Subset of Niemytzki-plane
for x, y being Element of REAL
for r being real positive number st y > 0 & U = (Ball |[x,y]|,r) /\ y>=0-plane holds
ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,y]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) )

proof end;

theorem Th86: :: TOPGEN_5:86

Niemytzki-plane is_T1

proof end;

theorem :: TOPGEN_5:87

Niemytzki-plane is Tychonoff

proof end;