:: Niemytzki Plane -- an Example of {T}ychonoff Space Which Is Not $T_4$
:: by Grzegorz Bancerek
::
:: Received November 7, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: TOPGEN_5:1
theorem :: TOPGEN_5:2
theorem Th3: :: TOPGEN_5:3
theorem :: TOPGEN_5:4
theorem Th5: :: TOPGEN_5:5
theorem Th6: :: TOPGEN_5:6
theorem Th7: :: TOPGEN_5:7
theorem :: TOPGEN_5:8
canceled;
theorem :: TOPGEN_5:9
canceled;
theorem :: TOPGEN_5:10
canceled;
theorem :: TOPGEN_5:11
canceled;
theorem Th12: :: TOPGEN_5:12
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) ) & (
P1[
a] &
P2[
a] implies
f . a = F5(
a) ) & (
P1[
a] &
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() ) & (
P1[
a] &
P2[
a] implies
F5(
a)
in F2() ) & (
P1[
a] &
P2[
a] implies
F6(
a)
in F2() ) )
theorem Th13: :: TOPGEN_5:13
theorem Th14: :: TOPGEN_5:14
theorem Th15: :: TOPGEN_5:15
theorem Th16: :: TOPGEN_5:16
theorem Th17: :: TOPGEN_5:17
:: deftheorem defines y=0-line TOPGEN_5:def 1 :
:: deftheorem defines y>=0-plane TOPGEN_5:def 2 :
theorem :: TOPGEN_5:18
theorem Th19: :: TOPGEN_5:19
theorem Th20: :: TOPGEN_5:20
theorem :: TOPGEN_5:21
theorem Th22: :: TOPGEN_5:22
theorem Th23: :: TOPGEN_5:23
theorem Th24: :: TOPGEN_5:24
theorem Th25: :: TOPGEN_5:25
theorem Th26: :: TOPGEN_5:26
theorem Th27: :: TOPGEN_5:27
theorem Th28: :: TOPGEN_5:28
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
ex b1 being non empty strict TopSpace st
( the carrier of b1 = y>=0-plane & 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 } ) & ( 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 } ) ) )
uniqueness
for b1, b2 being non empty strict TopSpace st the carrier of b1 = y>=0-plane & 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 } ) & ( 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 } ) ) & the carrier of b2 = y>=0-plane & 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 } ) & ( 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
end;
:: deftheorem Def3 defines Niemytzki-plane TOPGEN_5:def 3 :
theorem Th29: :: TOPGEN_5:29
Lm1:
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
theorem Th30: :: TOPGEN_5:30
theorem Th31: :: TOPGEN_5:31
theorem Th32: :: TOPGEN_5:32
theorem Th33: :: TOPGEN_5:33
theorem Th34: :: TOPGEN_5:34
theorem Th35: :: TOPGEN_5:35
theorem Th36: :: TOPGEN_5:36
theorem Th37: :: TOPGEN_5:37
theorem Th38: :: TOPGEN_5:38
theorem Th39: :: TOPGEN_5:39
theorem Th40: :: TOPGEN_5:40
theorem :: TOPGEN_5:41
theorem :: TOPGEN_5:42
theorem :: TOPGEN_5:43
theorem :: TOPGEN_5:44
theorem Th45: :: TOPGEN_5:45
theorem Th46: :: TOPGEN_5:46
theorem Th47: :: TOPGEN_5:47
theorem :: TOPGEN_5:48
theorem :: TOPGEN_5:49
theorem :: TOPGEN_5:50
theorem :: TOPGEN_5:51
:: deftheorem Def4 defines Tychonoff TOPGEN_5:def 4 :
theorem :: TOPGEN_5:52
theorem Th53: :: TOPGEN_5:53
theorem Th54: :: TOPGEN_5:54
theorem Th55: :: TOPGEN_5:55
theorem Th56: :: TOPGEN_5:56
theorem Th57: :: TOPGEN_5:57
theorem Th58: :: TOPGEN_5:58
theorem :: TOPGEN_5:59
theorem Th60: :: TOPGEN_5:60
theorem Th61: :: TOPGEN_5:61
theorem Th62: :: TOPGEN_5:62
theorem :: TOPGEN_5:63
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
ex b1 being Function of Niemytzki-plane ,I[01] st
( b1 . |[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 b1 . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,r]|,r implies b1 . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) )
uniqueness
for b1, b2 being Function of Niemytzki-plane ,I[01] st b1 . |[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 b1 . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,r]|,r implies b1 . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) & b2 . |[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 b2 . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,r]|,r implies b2 . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) holds
b1 = b2
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 & ( 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
b3 . |[a,b]| = 1 ) & (
|[a,b]| in Ball |[x,r]|,
r implies
b3 . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) ) );
theorem Th64: :: TOPGEN_5:64
theorem Th65: :: TOPGEN_5:65
theorem Th66: :: TOPGEN_5:66
theorem Th67: :: TOPGEN_5:67
theorem Th68: :: TOPGEN_5:68
theorem Th69: :: TOPGEN_5:69
theorem Th70: :: TOPGEN_5:70
theorem Th71: :: TOPGEN_5:71
theorem Th72: :: TOPGEN_5:72
theorem Th73: :: TOPGEN_5:73
theorem Th74: :: TOPGEN_5:74
theorem Th75: :: TOPGEN_5:75
theorem Th76: :: TOPGEN_5:76
theorem Th77: :: TOPGEN_5:77
theorem Th78: :: TOPGEN_5:78
theorem Th79: :: TOPGEN_5:79
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) ) ) ) )
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
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 ) & ( |[a,b]| in Ball |[x,y]|,r implies b1 . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
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 ) & ( |[a,b]| in Ball |[x,y]|,r implies b1 . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) & ( 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 ) & ( |[a,b]| in Ball |[x,y]|,r implies b2 . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) holds
b1 = b2
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 ) & (
|[a,b]| in Ball |[x,y]|,
r implies
b4 . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) );
theorem Th81: :: TOPGEN_5:81
theorem Th82: :: TOPGEN_5:82
theorem Th83: :: TOPGEN_5:83
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.] ) )
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 ) ) ) )
theorem Th86: :: TOPGEN_5:86
theorem :: TOPGEN_5:87