:: Niemytzki Plane -- an Example of {T}ychonoff Space Which Is Not $T_4$
:: by Grzegorz Bancerek
::
:: Received November 7, 2005
:: Copyright (c) 2005-2017 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;