:: Niemytzki Plane -- an Example of {T}ychonoff Space Which Is Not $T_4$ :: by Grzegorz Bancerek :: :: Received November 7, 2005 :: Copyright (c) 2005-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, XXREAL_0, ORDINAL1, FUNCT_1, PARTFUN1, FUNCT_4, RELAT_1, XBOOLE_0, TARSKI, FUNCT_6, FUNCOP_1, FUNCT_2, FUNCT_5, ZFMISC_1, MCART_1, CARD_3, FINSEQ_1, CARD_1, CARD_2, COMPLEX1, EUCLID, SQUARE_1, ARYTM_3, PRE_TOPC, RCOMP_1, ORDINAL2, STRUCT_0, METRIC_1, ARYTM_1, SUPINF_2, REAL_1, TOPGEN_3, TOPGEN_2, CANTOR_1, PBOOLE, SETFAM_1, RAT_1, TOPS_1, TOPGEN_1, XXREAL_1, RLVECT_3, BORSUK_1, CARD_5, TOPMETR, TOPS_2, VALUED_1, FINSET_1, LIMFUNC1, TOPGEN_5, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, RELAT_1, FINSET_1, SUBSET_1, MCART_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, FUNCT_4, FUNCOP_1, PBOOLE, ORDINAL1, CARD_1, CARD_2, CARD_3, FUNCT_5, FUNCT_6, NUMBERS, XCMPLX_0, SQUARE_1, COMPLEX1, REAL_1, XREAL_0, XXREAL_2, RAT_1, RCOMP_1, LIMFUNC1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, RLVECT_1, EUCLID, CANTOR_1, TOPMETR, TOPREAL9, TOPGEN_1, TOPGEN_2, TOPGEN_3, XXREAL_0; constructors WELLORD2, FUNCT_4, REAL_1, SQUARE_1, COMPLEX1, CARD_2, PROB_1, RCOMP_1, LIMFUNC1, FUNCT_6, TOPS_1, MONOID_0, BORSUK_4, TOPGEN_2, TOPREAL9, TOPGEN_1, TOPGEN_3, XXREAL_2, BINOP_2, XTUPLE_0, BINOP_1; registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, RAT_1, CARD_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, MONOID_0, EUCLID, TOPMETR, TOPGRP_1, TOPGEN_1, VALUED_0, XXREAL_2, RELSET_1, XTUPLE_0, REAL_1, ORDINAL1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Preliminaries reserve x,y for Real, u,v,w for set, r for positive Real; theorem :: TOPGEN_5:1 for f,g being Function st f tolerates g for A being set holds (f +*g)"A = (f"A)\/(g"A); theorem :: TOPGEN_5:2 for f,g being Function st dom f misses dom g for A being set holds (f +*g)"A = (f"A)\/(g"A); theorem :: TOPGEN_5:3 for x,a being set, f being Function st a in dom f holds (commute (x .--> f)).a = x .--> f.a; theorem :: TOPGEN_5:4 for b being set, f being Function holds b in dom commute f iff ex a being set, g being Function st a in dom f & g = f.a & b in dom g; theorem :: TOPGEN_5:5 for a,b being set, 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; theorem :: TOPGEN_5:6 for a,b being set, f,g being Function st a in dom f & g = f.a & b in dom g holds (commute f).b.a = g.b; theorem :: TOPGEN_5:7 for a being set, f,g,h being Function st h = f \/ g holds ( commute h).a = (commute f).a \/ (commute g).a; theorem :: TOPGEN_5:8 for X,Y being set holds product <*X,Y*>, [:X,Y:] are_equipotent & card product <*X,Y*> = (card X)*`(card Y); scheme :: TOPGEN_5:sch 1 SCH1{P[object], A,B,C()-> non empty set, F1,F2(object)-> set}: ex f being Function of C(), B() st for a being Element of A() st a in C() holds (P[a] implies f.a = F1(a)) & (not P[a] implies f.a = F2(a)) provided C() c= A() and for a being Element of A() st a in C() holds (P[a] implies F1(a) in B()) & (not P[a] implies F2(a) in B()); scheme :: TOPGEN_5:sch 2 SCH2{P,Q[object], A,B,C()-> non empty set, F1,F2,F3(object)-> object}: ex f being Function of C(), B() st for a being Element of A() st a in C() holds (P[a] implies f.a = F1(a)) & (not P[a] & Q[a] implies f.a = F2(a)) & (not P[a] & not Q[a] implies f.a = F3(a)) provided C() c= A() and for a being Element of A() st a in C() holds (P[a] implies F1(a) in B()) & (not P[a] & Q[a] implies F2(a) in B()) & (not P[a] & not Q[a] implies F3 (a) in B()); theorem :: TOPGEN_5:9 for a,b being Real holds |.|[a,b]|.|^2 = a^2+b^2; theorem :: TOPGEN_5:10 for X being TopSpace, 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; theorem :: TOPGEN_5:11 for X being TopSpace, Y being non empty TopSpace for A,B being closed Subset of X st A misses B 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; theorem :: TOPGEN_5:12 for X being TopSpace, 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; begin :: Niemytzki plane theorem :: TOPGEN_5:13 for n being Element of NAT for a being Point of TOP-REAL n for r being positive Real holds a in Ball(a,r); definition func y=0-line -> Subset of TOP-REAL 2 equals :: TOPGEN_5:def 1 the set of all |[x,0]|; func y>=0-plane -> Subset of TOP-REAL 2 equals :: TOPGEN_5:def 2 {|[x,y]|: y >= 0}; end; theorem :: TOPGEN_5:14 for a,b being set holds <*a,b*> in y=0-line iff a in REAL & b = 0; theorem :: TOPGEN_5:15 for a,b being Real holds |[a,b]| in y=0-line iff b = 0; theorem :: TOPGEN_5:16 card y=0-line = continuum; theorem :: TOPGEN_5:17 for a,b being set holds <*a,b*> in y>=0-plane iff a in REAL & ex y st b = y & y >= 0; theorem :: TOPGEN_5:18 for a,b being Real holds |[a,b]| in y>=0-plane iff b >= 0; registration cluster y=0-line -> non empty; cluster y>=0-plane -> non empty; end; theorem :: TOPGEN_5:19 y=0-line c= y>=0-plane; theorem :: TOPGEN_5:20 for a,b,r being Real st r > 0 holds Ball(|[a,b]|,r) c= y>=0-plane iff r <= b; theorem :: TOPGEN_5:21 for a,b,r being Real st r > 0 & b >= 0 holds Ball(|[a,b]| ,r) misses y=0-line iff r <= b; theorem :: TOPGEN_5:22 for n being Element of NAT, a,b being Element of TOP-REAL n, r1, r2 being positive Real st |.a-b.| <= r1-r2 holds Ball(b,r2) c= Ball(a, r1); theorem :: TOPGEN_5:23 for a being Real, r1,r2 being positive Real st r1 <= r2 holds Ball(|[a,r1]|,r1) c= Ball(|[a,r2]|,r2); theorem :: 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 the TopStruct of T1 = the TopStruct of T2; definition ::$N Niemytzki plane func Niemytzki-plane -> strict non empty TopSpace means :: TOPGEN_5:def 3 the carrier of it = y>=0-plane & ex B being Neighborhood_System of it st (for x holds B.(|[ x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is Real: r > 0}) & for x,y st y > 0 holds B.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane where r is Real: r > 0}; end; theorem :: TOPGEN_5:25 y>=0-plane \ y=0-line is open Subset of Niemytzki-plane; theorem :: TOPGEN_5:26 y=0-line is closed Subset of Niemytzki-plane; theorem :: TOPGEN_5:27 for x being Real, r being positive Real holds Ball(|[x,r]|,r) \/ {|[x,0]|} is open Subset of Niemytzki-plane; theorem :: TOPGEN_5:28 for x being Real for y,r being positive Real holds Ball(|[x,y]|,r) /\ y>=0-plane is open Subset of Niemytzki-plane; theorem :: TOPGEN_5:29 for x,y being Real for r being positive Real st r <= y holds Ball(|[x,y]|,r) is open Subset of Niemytzki-plane; theorem :: TOPGEN_5:30 for p being Point of Niemytzki-plane for r being positive Real ex a being Point of TOP-REAL 2, 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; theorem :: TOPGEN_5:31 for x,y being Real for r being positive Real ex w,v being Rational st |[w,v]| in Ball(|[x,y]|,r) & |[w,v]| <> |[x,y]|; theorem :: TOPGEN_5:32 for A being Subset of Niemytzki-plane st A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane; theorem :: TOPGEN_5:33 for A being Subset of Niemytzki-plane st A = y>=0-plane \ y=0-line for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane; theorem :: TOPGEN_5:34 for A being Subset of Niemytzki-plane st A = y>=0-plane \ y=0-line holds Cl A = [#] Niemytzki-plane; theorem :: TOPGEN_5:35 for A being Subset of Niemytzki-plane st A = y=0-line holds Cl A = A & Int A = {}; theorem :: TOPGEN_5:36 (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> is dense Subset of Niemytzki-plane; theorem :: TOPGEN_5:37 (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> is dense-in-itself Subset of Niemytzki-plane; theorem :: TOPGEN_5:38 y>=0-plane \ y=0-line is dense Subset of Niemytzki-plane; theorem :: TOPGEN_5:39 y>=0-plane \ y=0-line is dense-in-itself Subset of Niemytzki-plane; theorem :: TOPGEN_5:40 y=0-line is nowhere_dense Subset of Niemytzki-plane; theorem :: TOPGEN_5:41 for A being Subset of Niemytzki-plane st A = y=0-line holds Der A is empty; theorem :: TOPGEN_5:42 for A being Subset of y=0-line holds A is closed Subset of Niemytzki-plane; theorem :: TOPGEN_5:43 RAT is dense Subset of Sorgenfrey-line; theorem :: TOPGEN_5:44 Sorgenfrey-line is separable; theorem :: TOPGEN_5:45 Niemytzki-plane is separable; theorem :: TOPGEN_5:46 Niemytzki-plane is T_1; theorem :: TOPGEN_5:47 Niemytzki-plane is not normal; begin :: Tychonoff spaces definition let T be TopSpace; attr T is Tychonoff means :: TOPGEN_5:def 4 for A being closed Subset of T, a being Point of T st a in A` ex f being continuous Function of T, I[01] st f.a = 0 & f .:A c= {1}; end; registration cluster Tychonoff -> regular for TopSpace; cluster T_4 -> Tychonoff for non empty TopSpace; end; theorem :: TOPGEN_5:48 for X being T_1 TopSpace st X is Tychonoff 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 ex f being continuous Function of X, I[01] st f.x = 0 & f.:V` c= {1}; theorem :: TOPGEN_5:49 for X being TopSpace, 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; theorem :: TOPGEN_5:50 for X being TopSpace, 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); theorem :: TOPGEN_5:51 for X being non empty TopSpace, R being non empty SubSpace of R^1 for A being finite non empty 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 ex f being continuous Function of X,R st for x being Point of X, S being finite non empty Subset of REAL st S = rng ((commute F).x) holds f.x = max S; theorem :: TOPGEN_5:52 for X being T_1 non empty 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 ex f being continuous Function of X, I[01] st f.x = 0 & f.:V` c= {1} holds X is Tychonoff; theorem :: TOPGEN_5:53 Sorgenfrey-line is T_1; theorem :: TOPGEN_5:54 for x being Real holds left_open_halfline x is closed Subset of Sorgenfrey-line; theorem :: TOPGEN_5:55 for x being Real holds left_closed_halfline x is closed Subset of Sorgenfrey-line; theorem :: TOPGEN_5:56 for x being Real holds right_closed_halfline x is closed Subset of Sorgenfrey-line; theorem :: TOPGEN_5:57 for x,y being Real holds [.x,y.[ is closed Subset of Sorgenfrey-line; :: theorem :: TOPGEN_5:58 for x being Real, w being Rational 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); theorem :: TOPGEN_5:59 Sorgenfrey-line is Tychonoff; begin :: Niemytzki plane is Tychonoff space :: definition let x be Real, r be positive Real; func +(x,r) -> Function of Niemytzki-plane, I[01] means :: TOPGEN_5:def 5 it.(|[x,0]|) = 0 & for a being Real, b being non negative Real 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)); end; theorem :: TOPGEN_5:60 for p being Point of TOP-REAL 2 st p`2 >= 0 for x being Real , r being positive Real st +(x,r).p = 0 holds p = |[x,0]|; theorem :: TOPGEN_5:61 for x,y being Real, r being positive Real st x <> y holds +(x,r).(|[y,0]|) = 1; theorem :: TOPGEN_5:62 for p being Point of TOP-REAL 2 for x being Real, a,r being positive Real st a <= 1 & |.p-|[x,r*a]|.| = r*a & p`2 <> 0 holds +(x,r).p = a; theorem :: TOPGEN_5:63 for p being Point of TOP-REAL 2 for x,a being Real, r being positive Real st a <= 1 & |.p-|[x,r*a]|.| < r*a holds +(x,r).p < a; theorem :: TOPGEN_5:64 for p being Point of TOP-REAL 2 st p`2 >= 0 for x,a being Real , r being positive Real st 0 <= a & a < 1 & |.p-|[x,r*a]|.| > r* a holds +(x,r).p > a; theorem :: TOPGEN_5:65 for p being Point of TOP-REAL 2 st p`2 >= 0 for x,a,b being Real , r being positive Real st 0 <= a & b <= 1 & +(x,r).p in ].a,b.[ ex r1 being positive Real st r1 <= p`2 & Ball(p,r1) c= +(x,r)"].a,b.[; theorem :: TOPGEN_5:66 for x being Real, a,r being positive Real holds Ball(|[x,r*a]|,r*a) c= +(x,r)"].0,a.[; theorem :: TOPGEN_5:67 for x being Real, a,r being positive Real holds Ball(|[x,r*a]|,r*a) \/ {|[x,0]|} c= +(x,r)"[.0,a.[; theorem :: TOPGEN_5:68 for p being Point of TOP-REAL 2 st p`2 >= 0 for x,a being Real , r being positive Real st 0 < +(x,r).p & +(x,r).p < a & a <= 1 holds p in Ball(|[x,r*a]|,r*a); theorem :: TOPGEN_5:69 for p being Point of TOP-REAL 2 st p`2 > 0 for x,a being Real , r being positive Real st 0 <= a & a < +(x,r).p ex r1 being positive Real st r1 <= p`2 & Ball(p,r1) c= +(x,r)"].a,1.]; theorem :: TOPGEN_5:70 for p being Point of TOP-REAL 2 st p`2 = 0 for x being Real , r being positive Real st +(x,r).p = 1 ex r1 being positive Real st Ball(|[p`1,r1]|,r1) \/ {p} c= +(x,r)"{1}; theorem :: TOPGEN_5:71 for T being non empty TopSpace, 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; theorem :: TOPGEN_5:72 {].a,b.[ where a,b is Real: a < b} is Basis of R^1; theorem :: TOPGEN_5:73 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; theorem :: TOPGEN_5:74 {[.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]; theorem :: 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 st 0 <= a & a < 1 & 0 < b & b <= 1 holds f"[.0,b.[ is open & f"].a,1.] is open; registration let x be Real, r be positive Real; cluster +(x,r) -> continuous; end; theorem :: TOPGEN_5:76 for U being Subset of Niemytzki-plane for x,r st U = Ball(|[x,r ]|,r) \/ {|[x,0]|} ex f being continuous Function of Niemytzki-plane, I[01] st f.(|[x,0]|) = 0 & for a,b being Real 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)); :: definition let x,y be Real, r be positive Real; func +(x,y,r) -> Function of Niemytzki-plane, I[01] means :: TOPGEN_5:def 6 for a being Real, b being non negative Real 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); end; theorem :: TOPGEN_5:77 for p being Point of TOP-REAL 2 st p`2 >= 0 for x being Real , y being non negative Real for r being positive Real holds +(x,y,r).p = 0 iff p = |[x,y]|; theorem :: TOPGEN_5:78 for x being Real, y being non negative Real for r,a being positive Real st a <= 1 holds +(x,y,r)"[.0,a.[ = Ball(|[x,y ]|,r*a) /\ y>=0-plane; theorem :: TOPGEN_5:79 for p being Point of TOP-REAL 2 st p`2 > 0 for x being Real , a being non negative Real for y,r being positive Real 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.]; theorem :: TOPGEN_5:80 for p being Point of TOP-REAL 2 st p`2 = 0 for x being Real , a being non negative Real for y,r being positive Real st +(x,y,r).p > a holds |.|[x,y]|-p.| > r*a & ex r1 being positive Real st r1 = (|.|[x,y]|-p.|-r*a)/2 & Ball(|[p`1,r1]|,r1) \/ {p} c= +(x,y,r)"].a,1 .]; registration let x be Real; let y,r be positive Real; cluster +(x,y,r) -> continuous; end; theorem :: TOPGEN_5:81 for U being Subset of Niemytzki-plane for x,y,r st y > 0 & U = Ball(|[x,y]|,r) /\ y>=0-plane ex f being continuous Function of Niemytzki-plane , I[01] st f.(|[x,y]|) = 0 & for a,b being Real holds (|[a,b]| in U` implies f.(|[a,b]|) = 1) & (|[a,b]| in U implies f.(|[a,b]|) = |.|[x,y]|-|[a,b ]|.|/r); theorem :: TOPGEN_5:82 Niemytzki-plane is T_1; theorem :: TOPGEN_5:83 Niemytzki-plane is Tychonoff;