:: Niemytzki Plane -- an Example of {T}ychonoff Space Which Is Not $T_4$
:: by Grzegorz Bancerek
::
:: Received November 7, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

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)
proofend;

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) by Th1, PARTFUN1:56;

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)
proofend;

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 ) )
proofend;

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 ) )
proofend;

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
proofend;

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)
proofend;

theorem Th8: :: TOPGEN_5:8
for X, Y being set holds
( product <*X,Y*>,[:X,Y:] are_equipotent &amp; card (product <*X,Y*>) = (card X) *` (card Y) )
proofend;

scheme :: TOPGEN_5:sch 1
SCH1{ P1[ set ], F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( set ) ->  set , F5( set ) ->  set } :
 ex f being Function of F3(),F2() st
for a being Element of F1() st a in F3() holds
( ( P1[a] implies f . a = F4(a) ) &amp; ( P1[a] implies f . a = F5(a) ) )
provided
A1: F3() c= F1() and
A2: for a being Element of F1() st a in F3() holds
( ( P1[a] implies F4(a) in F2() ) &amp; ( P1[a] implies F5(a) in F2() ) )
proofend;

scheme :: TOPGEN_5:sch 2
SCH2{ P1[ set ], P2[ set ], F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( set ) ->  set , F5( set ) ->  set , F6( set ) ->  set } :
 ex f being Function of F3(),F2() st
for a being Element of F1() st a in F3() holds
( ( P1[a] implies f . a = F4(a) ) &amp; ( P1[a] &amp; P2[a] implies f . a = F5(a) ) &amp; ( P1[a] &amp; P2[a] implies f . a = F6(a) ) )
provided
A1: F3() c= F1() and
A2: for a being Element of F1() st a in F3() holds
( ( P1[a] implies F4(a) in F2() ) &amp; ( P1[a] &amp; P2[a] implies F5(a) in F2() ) &amp; ( P1[a] &amp; P2[a] implies F6(a) in F2() ) )
proofend;

theorem Th9: :: TOPGEN_5:9
for a, b being real number holds |.|[a,b]|.| ^2 = (a ^2) + (b ^2)
proofend;

theorem Th10: :: TOPGEN_5:10
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
proofend;

theorem Th11: :: TOPGEN_5:11
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
proofend;

theorem Th12: :: TOPGEN_5:12
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
proofend;

begin

theorem Th13: :: TOPGEN_5:13
for n being Element of NAT
for a being Point of (TOP-REAL n)
for r being real positive number holds a in Ball (a,r)
proofend;

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
  {  |[x,0]| where x is Element of REAL : verum  }  is Subset of (TOP-REAL 2)
proofend;
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
  {  |[x,y]| where x, y is Element of REAL : y >= 0  }  is Subset of (TOP-REAL 2)
proofend;
end;

:: deftheorem  defines y=0-line TOPGEN_5:def_1_:_
 y=0-line =  {  |[x,0]| where x is Element of REAL : verum  }  ;

:: deftheorem  defines y>=0-plane TOPGEN_5:def_2_:_
 y>=0-plane =  {  |[x,y]| where x, y is Element of REAL : y >= 0  }  ;

theorem :: TOPGEN_5:14
for a, b being set holds
( <*a,b*> in y=0-line iff ( a in REAL &amp; b = 0 ) )
proofend;

theorem Th15: :: TOPGEN_5:15
for a, b being real number holds
( |[a,b]| in y=0-line iff b = 0 )
proofend;

theorem Th16: :: TOPGEN_5:16
card y=0-line = continuum
proofend;

theorem :: TOPGEN_5:17
for a, b being set holds
( <*a,b*> in y>=0-plane iff ( a in REAL &amp; ex y being Element of REAL st
( b = y &amp; y >= 0 ) ) )
proofend;

theorem Th18: :: TOPGEN_5:18
for a, b being real number holds
( |[a,b]| in y>=0-plane iff b >= 0 )
proofend;

registration
cluster y=0-line  ->  non empty ;
coherence
 not y=0-line is empty by Th15;
cluster y>=0-plane  ->  non empty ;
coherence
 not y>=0-plane is empty by Th18;
end;

theorem Th19: :: TOPGEN_5:19
y=0-line c= y>=0-plane
proofend;

theorem Th20: :: TOPGEN_5:20
for a, b, r being real number st r > 0 holds
( Ball (|[a,b]|,r) c= y>=0-plane iff r <= b )
proofend;

theorem Th21: :: TOPGEN_5:21
for a, b, r being real number st r > 0 &amp; b >= 0 holds
( Ball (|[a,b]|,r) misses y=0-line iff r <= b )
proofend;

theorem Th22: :: TOPGEN_5:22
for n being Element of 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)
proofend;

theorem Th23: :: TOPGEN_5:23
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)
proofend;

theorem Th24: :: TOPGEN_5:24
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 #)
proofend;

definition
func Niemytzki-plane  ->  non empty strict TopSpace means :Def3: :: TOPGEN_5:def 3
( the carrier of it = y>=0-plane &amp; 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  }  ) &amp; ( 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
 ex b1 being non empty strict TopSpace st
( the carrier of b1 = y>=0-plane &amp; ex B being Neighborhood_System of b1 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  }  ) &amp; ( 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  }  ) ) )
proofend;
uniqueness
 for b1, b2 being non empty strict TopSpace st the carrier of b1 = y>=0-plane &amp; ex B being Neighborhood_System of b1 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  }  ) &amp; ( 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  }  ) ) &amp; the carrier of b2 = y>=0-plane &amp; ex B being Neighborhood_System of b2 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  }  ) &amp; ( 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  }  ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Niemytzki-plane TOPGEN_5:def_3_:_
 for b1 being non empty strict TopSpace holds
( b1 = Niemytzki-plane iff ( the carrier of b1 = y>=0-plane &amp; ex B being Neighborhood_System of b1 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  }  ) &amp; ( 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  }  ) ) ) );

theorem Th25: :: TOPGEN_5:25
y>=0-plane \ y=0-line is open Subset of Niemytzki-plane
proofend;

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

theorem Th26: :: TOPGEN_5:26
y=0-line is closed Subset of Niemytzki-plane
proofend;

theorem Th27: :: TOPGEN_5:27
for x being real number
for r being real positive number holds (Ball (|[x,r]|,r)) \/ {|[x,0]|} is open Subset of Niemytzki-plane
proofend;

theorem Th28: :: TOPGEN_5:28
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
proofend;

theorem Th29: :: TOPGEN_5:29
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
proofend;

theorem Th30: :: TOPGEN_5:30
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 &amp; a in U &amp; ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )
proofend;

theorem Th31: :: TOPGEN_5:31
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) &amp; |[w,v]| <> |[x,y]| )
proofend;

theorem Th32: :: TOPGEN_5:32
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
proofend;

theorem Th33: :: TOPGEN_5:33
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
proofend;

theorem Th34: :: TOPGEN_5:34
for A being Subset of Niemytzki-plane st A = y>=0-plane \ y=0-line holds
Cl A = [#] Niemytzki-plane
proofend;

theorem Th35: :: TOPGEN_5:35
for A being Subset of Niemytzki-plane st A = y=0-line holds
( Cl A = A &amp; Int A = {} )
proofend;

theorem Th36: :: TOPGEN_5:36
(y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) is dense Subset of Niemytzki-plane
proofend;

theorem :: TOPGEN_5:37
(y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) is dense-in-itself Subset of Niemytzki-plane
proofend;

theorem :: TOPGEN_5:38
y>=0-plane \ y=0-line is dense Subset of Niemytzki-plane
proofend;

theorem :: TOPGEN_5:39
y>=0-plane \ y=0-line is dense-in-itself Subset of Niemytzki-plane
proofend;

theorem :: TOPGEN_5:40
y=0-line is nowhere_dense Subset of Niemytzki-plane
proofend;

theorem Th41: :: TOPGEN_5:41
for A being Subset of Niemytzki-plane st A = y=0-line holds
Der A is empty
proofend;

theorem Th42: :: TOPGEN_5:42
for A being Subset of y=0-line holds A is closed Subset of Niemytzki-plane
proofend;

theorem Th43: :: TOPGEN_5:43
RAT is dense Subset of Sorgenfrey-line
proofend;

theorem :: TOPGEN_5:44
Sorgenfrey-line is separable
proofend;

theorem :: TOPGEN_5:45
Niemytzki-plane is separable
proofend;

theorem :: TOPGEN_5:46
Niemytzki-plane is T_1
proofend;

theorem :: TOPGEN_5:47
not Niemytzki-plane is normal
proofend;

begin

definition
let T be TopSpace;
attrT is Tychonoff  means :Def4: :: TOPGEN_5:def 4
 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 &amp; f .: A c= {1} );
end;

:: deftheorem Def4 defines Tychonoff TOPGEN_5:def_4_:_
 for T being TopSpace holds
( T is Tychonoff iff 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 &amp; f .: A c= {1} ) );

registration
cluster TopSpace-like Tychonoff  ->  regular for TopStruct ;
coherence
 for b1 being TopSpace st b1 is Tychonoff holds
b1 is regular
proofend;
cluster non empty TopSpace-like T_4  ->  non empty Tychonoff for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is T_4 holds
b1 is Tychonoff
proofend;
end;

theorem :: TOPGEN_5:48
for X being T_1 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 &amp; V in B holds
ex f being continuous Function of X,I[01] st
( f . x = 0 &amp; f .: (V `) c= {1} )
proofend;

theorem Th49: :: TOPGEN_5:49
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
proofend;

theorem Th50: :: TOPGEN_5:50
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))
proofend;

theorem Th51: :: TOPGEN_5:51
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
proofend;

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

theorem Th53: :: TOPGEN_5:53
Sorgenfrey-line is T_1
proofend;

theorem Th54: :: TOPGEN_5:54
for x being real number holds left_open_halfline x is closed Subset of Sorgenfrey-line
proofend;

theorem :: TOPGEN_5:55
for x being real number holds left_closed_halfline x is closed Subset of Sorgenfrey-line
proofend;

theorem Th56: :: TOPGEN_5:56
for x being real number holds right_closed_halfline x is closed Subset of Sorgenfrey-line
proofend;

theorem Th57: :: TOPGEN_5:57
for x, y being real number holds [.x,y.[ is closed Subset of Sorgenfrey-line
proofend;

::<DESC name="1.4.4. Przyk/lad funkcji ci/ag/lej ze strza/lce w [0,1]" monograph="topology"/>
theorem Th58: :: TOPGEN_5:58
for x being real number
for w being rational number 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 ) &amp; ( not a in [.x,w.[ implies f . a = 1 ) )
proofend;

theorem :: TOPGEN_5:59
Sorgenfrey-line is Tychonoff
proofend;

begin

::<DESC name="1.4.5. Przyk/lad funkcji ci/ag/lej z p/laszczyzny Niemytzkiego w R^1" monograph="topology"/>
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 &amp; ( for a being real number
for b being real non negative number holds
( ( ( a <> x or b <> 0 ) &amp; not |[a,b]| in Ball (|[x,r]|,r) implies it . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,r]|,r) implies it . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) );
existence
 ex b1 being Function of Niemytzki-plane,I[01] st
( b1 . |[x,0]| = 0 &amp; ( for a being real number
for b being real non negative number holds
( ( ( a <> x or b <> 0 ) &amp; not |[a,b]| in Ball (|[x,r]|,r) implies b1 . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,r]|,r) implies b1 . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Function of Niemytzki-plane,I[01] st b1 . |[x,0]| = 0 &amp; ( for a being real number
for b being real non negative number holds
( ( ( a <> x or b <> 0 ) &amp; not |[a,b]| in Ball (|[x,r]|,r) implies b1 . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,r]|,r) implies b1 . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) &amp; b2 . |[x,0]| = 0 &amp; ( for a being real number
for b being real non negative number holds
( ( ( a <> x or b <> 0 ) &amp; not |[a,b]| in Ball (|[x,r]|,r) implies b2 . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,r]|,r) implies b2 . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines + TOPGEN_5:def_5_:_
 for x being real number
for r being real positive number
for b3 being Function of Niemytzki-plane,I[01] holds
( b3 = + (x,r) iff ( b3 . |[x,0]| = 0 &amp; ( for a being real number
for b being real non negative number holds
( ( ( a <> x or b <> 0 ) &amp; not |[a,b]| in Ball (|[x,r]|,r) implies b3 . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,r]|,r) implies b3 . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) ) );

theorem Th60: :: TOPGEN_5:60
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]|
proofend;

theorem Th61: :: TOPGEN_5:61
for x, y being real number
for r being real positive number st x <> y holds
(+ (x,r)) . |[y,0]| = 1
proofend;

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

theorem Th63: :: TOPGEN_5:63
for p being Point of (TOP-REAL 2)
for x, a being real number
for r being real positive number st a <= 1 &amp; |.(p - |[x,(r * a)]|).| < r * a holds
(+ (x,r)) . p < a
proofend;

theorem Th64: :: TOPGEN_5:64
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 &amp; a < 1 &amp; |.(p - |[x,(r * a)]|).| > r * a holds
(+ (x,r)) . p > a
proofend;

theorem Th65: :: TOPGEN_5:65
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 &amp; b <= 1 &amp; (+ (x,r)) . p in ].a,b.[ holds
ex r1 being real positive number st
( r1 <= p `2 &amp; Ball (p,r1) c= (+ (x,r)) " ].a,b.[ )
proofend;

theorem Th66: :: TOPGEN_5:66
for x being real number
for a, r being real positive number holds Ball (|[x,(r * a)]|,(r * a)) c= (+ (x,r)) " ].0,a.[
proofend;

theorem Th67: :: TOPGEN_5:67
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.[
proofend;

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 < (+ (x,r)) . p &amp; (+ (x,r)) . p < a &amp; a <= 1 holds
p in Ball (|[x,(r * a)]|,(r * a))
proofend;

theorem Th69: :: TOPGEN_5:69
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 &amp; a < (+ (x,r)) . p holds
ex r1 being real positive number st
( r1 <= p `2 &amp; Ball (p,r1) c= (+ (x,r)) " ].a,1.] )
proofend;

theorem Th70: :: TOPGEN_5:70
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}
proofend;

theorem Th71: :: TOPGEN_5:71
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 &amp; A meets [#] S )  }  is Basis of S
proofend;

theorem Th72: :: TOPGEN_5:72
 {  ].a,b.[ where a, b is Real : a < b  }  is Basis of R^1
proofend;

theorem Th73: :: TOPGEN_5:73
for T being TopSpace
for U, V being Subset of T
for B being set st U in B &amp; V in B &amp; B \/ {(U \/ V)} is Basis of T holds
B is Basis of T
proofend;

theorem Th74: :: TOPGEN_5:74
( {  [.0,a.[ where a is Real : ( 0 < a &amp; a <= 1 )  }  \/  {  ].a,1.] where a is Real : ( 0 <= a &amp; a < 1 )  }  ) \/  {  ].a,b.[ where a, b is Real : ( 0 <= a &amp; a < b &amp; b <= 1 )  }  is Basis of I[01]
proofend;

theorem Th75: :: TOPGEN_5:75
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 &amp; a < 1 &amp; 0 < b &amp; b <= 1 holds
( f " [.0,b.[ is open &amp; f " ].a,1.] is open ) )
proofend;

registration
let x be real number ;
let r be real positive number ;
cluster + (x,r) ->  continuous ;
coherence
 + (x,r) is continuous
proofend;
end;

theorem Th76: :: TOPGEN_5:76
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 &amp; ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) &amp; ( |[a,b]| in U \ {|[x,0]|} implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) )
proofend;

::<DESC name="1.4.5. Przyk/lad funkcji ci/ag/lej z p/laszczyzny Niemytzkiego w R^1" monograph="topology"/>
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 ) &amp; ( |[a,b]| in Ball (|[x,y]|,r) implies it . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) );
existence
 ex b1 being Function of Niemytzki-plane,I[01] st
for a being real number
for b being real non negative number holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies b1 . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,y]|,r) implies b1 . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
proofend;
uniqueness
 for b1, b2 being Function of Niemytzki-plane,I[01] st ( for a being real number
for b being real non negative number holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies b1 . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,y]|,r) implies b1 . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) &amp; ( for a being real number
for b being real non negative number holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies b2 . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,y]|,r) implies b2 . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines + TOPGEN_5:def_6_:_
 for x, y being real number
for r being real positive number
for b4 being Function of Niemytzki-plane,I[01] holds
( b4 = + (x,y,r) iff for a being real number
for b being real non negative number holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies b4 . |[a,b]| = 1 ) &amp; ( |[a,b]| in Ball (|[x,y]|,r) implies b4 . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) );

theorem Th77: :: TOPGEN_5:77
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]| )
proofend;

theorem Th78: :: TOPGEN_5:78
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
proofend;

theorem Th79: :: TOPGEN_5:79
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 &amp; (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane c= (+ (x,y,r)) " ].a,1.] )
proofend;

theorem Th80: :: TOPGEN_5:80
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 &amp; ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 &amp; (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) )
proofend;

registration
let x be real number ;
let y, r be real positive number ;
cluster + (x,y,r) ->  continuous ;
coherence
 + (x,y,r) is continuous
proofend;
end;

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

theorem Th82: :: TOPGEN_5:82
Niemytzki-plane is T_1
proofend;

theorem :: TOPGEN_5:83
Niemytzki-plane is Tychonoff
proofend;