:: Niemytzki Plane -- an Example of {T}ychonoff Space Which Is Not $T_4$
:: by Grzegorz Bancerek
::
:: Received November 7, 2005
:: Copyright (c) 2005-2026 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;
definitions TARSKI, XBOOLE_0, FUNCT_1, PARTFUN1, FUNCOP_1, WELLORD2, PBOOLE,
PRE_TOPC, TOPS_3, URYSOHN1, TOPGEN_1, COMPTS_1;
equalities RELAT_1, XBOOLE_0, FUNCOP_1, FUNCT_6, BINOP_1, SQUARE_1, SUBSET_1,
STRUCT_0, LIMFUNC1, PROB_1, ORDINAL1, RLVECT_1;
expansions RELAT_1, TARSKI, XBOOLE_0, PBOOLE, PRE_TOPC, TOPGEN_1;
theorems TOPS_3, TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, FUNCT_1, EUCLID,
PBOOLE, EUCLID_2, TOPREAL9, TOPGEN_3, SETWISEO, XREAL_1, XREAL_0,
XCMPLX_1, TOPRNS_1, TOPREAL6, ABSVALUE, SPPOL_2, FINSEQ_1, COMPLEX1,
JGRAPH_1, YELLOW_9, NUMBERS, CARD_5, TOPGEN_2, SUBSET_1, YELLOW_8,
TOPS_1, PRE_TOPC, TOPGEN_1, SQUARE_1, RAT_1, CARD_1, CARD_2, CARD_3,
CARD_4, FINSEQ_3, MCART_1, FUNCT_6, BORSUK_1, TOPALG_1, TOPS_2, FUNCT_2,
TIETZE, JGRAPH_5, URYSOHN1, TOPMETR, BOOLMARK, FUNCOP_1, FUNCT_4,
RELAT_1, RELSET_1, CANTOR_1, PARTFUN1, SETFAM_1, JORDAN6, YELLOW12,
FUNCT_7, DICKSON, FUNCT_5, FRECHET, TSP_1, JORDAN, XXREAL_0, TSEP_1,
XXREAL_1, XXREAL_2, XTUPLE_0, RLVECT_1;
schemes SUBSET_1, FUNCT_1, PRE_CIRC, FUNCT_5, CLASSES1, FINSET_1, FUNCT_2;
begin :: Preliminaries
reserve x,y for Real,
u,v,w for set,
r for positive Real;
theorem Th1:
for f,g being Function st f tolerates g for A being set holds (f
+*g)"A = (f"A)\/(g"A)
proof
let f,g be Function;
assume
A1: f tolerates g;
let A be set;
f c= f+*g by A1,FUNCT_4:28;
then
A2: f"A c= (f+*g)"A by RELAT_1:144;
thus (f+*g)"A c= (f"A)\/(g"A)
proof
let x be object;
assume
A3: x in (f+*g)"A;
then x in dom (f+*g) by FUNCT_1:def 7;
then x in dom f \/ dom g by FUNCT_4:def 1;
then x in dom f or x in dom g by XBOOLE_0:def 3;
then
A4: x in dom f & (f+*g).x = f.x or x in dom g & (f+*g).x = g.x by A1,FUNCT_4:13
,15;
(f+*g).x in A by A3,FUNCT_1:def 7;
then x in f"A or x in g"A by A4,FUNCT_1:def 7;
hence thesis by XBOOLE_0:def 3;
end;
g"A c= (f+*g)"A by FUNCT_4:25,RELAT_1:144;
hence thesis by A2,XBOOLE_1:8;
end;
theorem
for f,g being Function st dom f misses dom g for A being set holds (f
+*g)"A = (f"A)\/(g"A) by Th1,PARTFUN1:56;
theorem Th3:
for x,a being set, f being Function st a in dom f holds (commute
(x .--> f)).a = x .--> f.a
proof
let x,a be set;
let f be Function;
set g = x .--> f;
A1: dom g = {x};
A2: f in Funcs(dom f, rng f) by FUNCT_2:def 2;
rng g = {f} by FUNCOP_1:8;
then rng g c= Funcs(dom f, rng f) by A2,ZFMISC_1:31;
then
A3: g in Funcs({x}, Funcs(dom f, rng f)) by A1,FUNCT_2:def 2;
A4: g.x = f by FUNCOP_1:72;
A5: x in {x} by TARSKI:def 1;
assume
A6: a in dom f;
then
A7: (commute g).a.x = f.a by A3,A4,A5,FUNCT_6:56;
dom ((commute g).a) = {x} by A3,A6,A4,A5,FUNCT_6:56;
hence thesis by A7,DICKSON:1;
end;
theorem
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
proof
let b be set;
let f be Function;
A1: dom commute f = proj2 dom uncurry f by FUNCT_5:23;
hereby
assume b in dom commute f;
then consider a being object such that
A2: [a,b] in dom uncurry f by A1,XTUPLE_0:def 13;
consider a9 being object, g being Function, b9 being object such that
A3: [a,b] = [a9,b9] and
A4: a9 in dom f and
A5: g = f.a9 and
A6: b9 in dom g by A2,FUNCT_5:def 2;
reconsider a as set by TARSKI:1;
take a, g;
thus a in dom f & g = f.a & b in dom g by A3,A4,A5,A6,XTUPLE_0:1;
end;
given a being set, g being Function such that
A7: a in dom f and
A8: g = f.a and
A9: b in dom g;
[a,b] in dom uncurry f by A7,A8,A9,FUNCT_5:def 2;
hence thesis by A1,XTUPLE_0:def 13;
end;
theorem Th5:
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
proof
let a,b be set;
let f be Function;
dom uncurry f c= [:dom f, proj1 union rng f:]
proof
let u be object;
assume u in dom uncurry f;
then consider a being object, g being Function, b being object such that
A1: u = [a,b] and
A2: a in dom f and
A3: g = f.a and
A4: b in dom g by FUNCT_5:def 2;
g in rng f by A2,A3,FUNCT_1:def 3;
then g c= union rng f by ZFMISC_1:74;
then proj1 g c= proj1 union rng f by XTUPLE_0:8;
hence thesis by A1,A2,A4,ZFMISC_1:def 2;
end;
then
A5: uncurry' commute f = uncurry f by FUNCT_5:50;
hereby
assume
A6: a in dom ((commute f).b);
then b in dom commute f by FUNCT_1:def 2,RELAT_1:38;
then [a,b] in dom uncurry f by A5,A6,FUNCT_5:39;
then consider a9 being object, g being Function, b9 being object
such that
A7: [a,b] = [a9,b9] and
A8: a9 in dom f and
A9: g = f.a9 and
A10: b9 in dom g by FUNCT_5:def 2;
take g;
thus a in dom f & g = f.a & b in dom g by A7,A8,A9,A10,XTUPLE_0:1;
end;
given g being Function such that
A11: a in dom f and
A12: g = f.a and
A13: b in dom g;
[a,b] in dom uncurry f by A11,A12,A13,FUNCT_5:def 2;
hence thesis by FUNCT_5:22;
end;
theorem Th6:
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
proof
let a,b be set;
let f,g be Function;
assume that
A1: a in dom f and
A2: g = f.a and
A3: b in dom g;
A4: [a,b] in dom uncurry f by A1,A2,A3,FUNCT_5:def 2;
A5: [a,b]`2 = b;
[a,b]`1 = a;
then (uncurry f).(a,b) = g.b by A5,A4,A2,FUNCT_5:def 2;
hence thesis by A4,FUNCT_5:22;
end;
theorem Th7:
for a being set, f,g,h being Function st h = f \/ g holds (
commute h).a = (commute f).a \/ (commute g).a
proof
let a be set;
let f,g,h be Function;
assume
A1: h = f \/ g;
now
let u,v be object;
hereby
assume
A2: [u,v] in (commute h).a;
then
A3: (commute h).a.u = v by FUNCT_1:1;
u in dom ((commute h).a) by A2,FUNCT_1:1;
then consider k being Function such that
A4: u in dom h and
A5: k = h.u and
A6: a in dom k by Th5;
[u,k] in h by A4,A5,FUNCT_1:def 2;
then [u,k] in f or [u,k] in g by A1,XBOOLE_0:def 3;
then u in dom f & k = f.u or u in dom g & k = g.u by FUNCT_1:1;
then
A7: u in dom ((commute f).a) & (commute f).a.u = k.a or u in dom ((
commute g).a) & (commute g).a.u = k.a by A6,Th5,Th6;
(commute h).a.u = k.a by A4,A5,A6,Th6;
then [u,v] in (commute f).a or [u,v] in (commute g).a by A7,A3,FUNCT_1:1;
hence [u,v] in (commute f).a \/ (commute g).a by XBOOLE_0:def 3;
end;
assume
A8: [u,v] in (commute f).a \/ (commute g).a;
per cases by A8,XBOOLE_0:def 3;
suppose
A9: [u,v] in (commute f).a;
then
A10: (commute f).a.u = v by FUNCT_1:1;
u in dom ((commute f).a) by A9,FUNCT_1:1;
then consider k being Function such that
A11: u in dom f and
A12: k = f.u and
A13: a in dom k by Th5;
A14: (commute f).a.u = k.a by A11,A12,A13,Th6;
[u,k] in f by A11,A12,FUNCT_1:1;
then
A15: [u,k] in h by A1,XBOOLE_0:def 3;
then
A16: u in dom h by FUNCT_1:1;
A17: k = h.u by A15,FUNCT_1:1;
then
A18: (commute h).a.u = k.a by A16,A13,Th6;
u in dom ((commute h).a) by A16,A17,A13,Th5;
hence [u,v] in (commute h).a by A18,A14,A10,FUNCT_1:1;
end;
suppose
A19: [u,v] in (commute g).a;
then
A20: (commute g).a.u = v by FUNCT_1:1;
u in dom ((commute g).a) by A19,FUNCT_1:1;
then consider k being Function such that
A21: u in dom g and
A22: k = g.u and
A23: a in dom k by Th5;
A24: (commute g).a.u = k.a by A21,A22,A23,Th6;
[u,k] in g by A21,A22,FUNCT_1:1;
then
A25: [u,k] in h by A1,XBOOLE_0:def 3;
then
A26: u in dom h by FUNCT_1:1;
A27: k = h.u by A25,FUNCT_1:1;
then
A28: (commute h).a.u = k.a by A26,A23,Th6;
u in dom ((commute h).a) by A26,A27,A23,Th5;
hence [u,v] in (commute h).a by A28,A24,A20,FUNCT_1:1;
end;
end;
hence thesis;
end;
theorem Th8:
for X,Y being set holds product <*X,Y*>, [:X,Y:] are_equipotent
& card product <*X,Y*> = (card X)*`(card Y)
proof
deffunc F(Function) = [$1.1,$1.2];
let X,Y be set;
consider f being Function such that
A1: dom f = product <*X,Y*> & for g being Function st g in product <*X,Y
*> holds f.g = F(g) from FUNCT_5:sch 1;
A2: <*X,Y*>.2 = Y;
A3: dom <*X,Y*> = {1,2} by FINSEQ_1:2,89;
A4: <*X,Y*>.1 = X;
thus product <*X,Y*>, [:X,Y:] are_equipotent
proof
take f;
thus f is one-to-one
proof
let x1,x2 be object;
assume that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f.x1 = f.x2;
consider g2 being Function such that
A8: x2 = g2 and
A9: dom g2 = dom <*X,Y*> and
for y being object st y in dom <*X,Y*> holds g2.y in <*X,Y*>.y by A1,A6,
CARD_3:def 5;
consider g1 being Function such that
A10: x1 = g1 and
A11: dom g1 = dom <*X,Y*> and
for y being object st y in dom <*X,Y*> holds g1.y in <*X,Y*>.y by A5,A1,
CARD_3:def 5;
A12: [g1.1,g1.2] = f.x1 by A1,A5,A10
.= [g2.1,g2.2] by A1,A6,A7,A8;
now
let z being object;
assume z in {1,2};
then z = 1 or z = 2 by TARSKI:def 2;
hence g1.z = g2.z by A12,XTUPLE_0:1;
end;
hence thesis by A3,A10,A11,A8,A9,FUNCT_1:2;
end;
thus dom f = product <*X,Y*> by A1;
thus rng f c= [:X,Y:]
proof
let z be object;
assume z in rng f;
then consider t being object such that
A13: t in dom f and
A14: z = f.t by FUNCT_1:def 3;
consider g being Function such that
A15: t = g and
dom g = dom <*X,Y*> and
A16: for y being object st y in dom <*X,Y*> holds g.y in <*X,Y*>.y by A1,A13,
CARD_3:def 5;
1 in {1,2} by TARSKI:def 2;
then
A17: g.1 in X by A3,A4,A16;
2 in {1,2} by TARSKI:def 2;
then
A18: g.2 in Y by A3,A2,A16;
z = [g.1,g.2] by A1,A13,A14,A15;
hence thesis by A17,A18,ZFMISC_1:87;
end;
let z be object;
set g = <*z`1,z`2*>;
A19: g.1 = z`1;
A20: g.2 = z`2;
assume
A21: z in [:X,Y:];
then
A22: z`2 in Y by MCART_1:10;
z`1 in X by A21,MCART_1:10;
then
A23: g in product <*X,Y*> by A22,FINSEQ_3:124;
z = [z`1,z`2] by A21,MCART_1:21;
then f.g = z by A23,A1,A19,A20;
hence thesis by A1,A23,FUNCT_1:def 3;
end;
hence card product <*X,Y*> = card [:X,Y:] by CARD_1:5
.= card [:card X, card Y:] by CARD_2:7
.= (card X)*`card Y by CARD_2:def 2;
end;
scheme
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
A1: C() c= A() and
A2: 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())
proof
A3: for a being object st a in C()
holds (P[a] implies F1(a) in B()) & (not P[a
] implies F2(a) in B()) by A1,A2;
consider f being Function of C(),B() such that
A4: for x being object st x in C() holds (P[ x] implies f.x = F1(x)) & (not
P[ x] implies f.x = F2(x)) from FUNCT_2:sch 5(A3);
take f;
thus thesis by A4;
end;
scheme
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
A1: C() c= A() and
A2: 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())
proof
set D = {a where a is Element of C(): P[a] or Q[a]};
per cases;
suppose
A3: D = {};
consider f being Function such that
A4: dom f = C() &
for u being object st u in C() holds f.u = F3(u) from FUNCT_1:sch
3;
rng f c= B()
proof
let v be object;
assume v in rng f;
then consider u being object such that
A5: u in dom f and
A6: v = f.u by FUNCT_1:def 3;
A7: v = F3(u) by A4,A5,A6;
A8: not u in D by A3;
then
A9: not Q[u] by A4,A5;
not P[u] by A8,A4,A5;
hence thesis by A9,A7,A1,A2,A4,A5;
end;
then reconsider f as Function of C(), B() by A4,FUNCT_2:2;
take f;
let a be Element of A();
assume
A10: a in C();
not a in D by A3;
hence thesis by A4,A10;
end;
suppose
D <> {};
then reconsider D as non empty set;
defpred PQ[object] means P[$1] or Q[$1];
A11: for a being object st a in D holds (P[a] implies F1(a) in B()) & (not P[
a] implies F2(a) in B())
proof
let a be object;
assume a in D;
then
A12: ex b being Element of C() st a = b & (P[b] or Q[b]);
then a in C();
hence thesis by A12,A1,A2;
end;
consider g being Function of D,B() such that
A13: for x being object st x in D holds (P[ x] implies g.x = F1(x)) & (
not P[ x] implies g.x = F2(x)) from FUNCT_2:sch 5(A11);
deffunc F12(object) = g.$1;
A14: for a being object st a in C() holds (PQ[a] implies F12(a) in B()) & (
not PQ[a] implies F3(a) in B())
proof
let a be object;
assume
A15: a in C();
hereby
assume PQ[a];
then
A16: a in D by A15;
then
A17: not P[a] implies F2(a) in B() by A11;
P[a] implies F1(a) in B() by A16,A11;
hence F12(a) in B() by A17,A16,A13;
end;
thus thesis by A1,A2,A15;
end;
consider f being Function of C(),B() such that
A18: for x being object st x in C() holds (PQ[ x] implies f.x = F12(x)) &
(not PQ[ x] implies f.x = F3(x)) from FUNCT_2:sch 5(A14);
take f;
let a be Element of A();
assume
A19: a in C();
then PQ[a] implies f.a = g.a & a in D by A18;
hence
(P[a] implies f.a = F1(a)) & (not P[a] & Q[a] implies f.a = F2(a)) by A13;
thus thesis by A18,A19;
end;
end;
theorem Th9:
for a,b being Real holds |.|[a,b]|.|^2 = a^2+b^2
proof
let a,b be Real;
A1: |[a,b]|`2 = b by EUCLID:52;
|[a,b]|`1 = a by EUCLID:52;
hence thesis by A1,JGRAPH_1:29;
end;
theorem Th10:
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
proof
let X be TopSpace, Y be non empty TopSpace;
let A,B be closed Subset of X;
let f be continuous Function of X|A, Y;
let g be continuous Function of X|B, Y such that
A1: f tolerates g;
A2: the carrier of X|(A \/ B) = A \/ B by PRE_TOPC:8;
the carrier of X|B = B by PRE_TOPC:8;
then
A3: dom g = B by FUNCT_2:def 1;
the carrier of X|A = A by PRE_TOPC:8;
then
A4: dom f = A by FUNCT_2:def 1;
A5: rng (f+*g) c= rng f \/ rng g by FUNCT_4:17;
dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
then reconsider h = f+*g as Function of X|(A \/ B), Y by A5,A2,A4,A3,
FUNCT_2:2,XBOOLE_1:1;
h is continuous
proof
let C be Subset of Y;
A6: [#](X|(A \/ B)) = A \/ B by PRE_TOPC:8;
assume
A7: C is closed;
then f"C is closed by PRE_TOPC:def 6;
then consider C1 being Subset of X such that
A8: C1 is closed and
A9: C1 /\ [#](X|A) = f"C by PRE_TOPC:13;
g"C is closed by A7,PRE_TOPC:def 6;
then consider C2 being Subset of X such that
A10: C2 is closed and
A11: C2 /\ [#](X|B) = g"C by PRE_TOPC:13;
A12: C1/\A\/C2/\B is closed by A8,A10;
A13: [#](X|A) = A by PRE_TOPC:8;
A14: [#](X|B) = B by PRE_TOPC:8;
h"C = (f"C)\/(g"C) by A1,Th1
.= ((f"C)\/(g"C))/\(A\/B) by A13,A14,XBOOLE_1:13,28;
hence thesis by A12,A9,A11,A6,A13,A14,PRE_TOPC:13;
end;
hence thesis;
end;
theorem Th11:
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
proof
let X be TopSpace, Y be non empty TopSpace;
let A,B be closed Subset of X such that
A1: A misses B;
let f be continuous Function of X|A, Y;
let g be continuous Function of X|B, Y;
the carrier of X|B = B by PRE_TOPC:8;
then
A2: dom g = B by FUNCT_2:def 1;
the carrier of X|A = A by PRE_TOPC:8;
then dom f = A by FUNCT_2:def 1;
hence thesis by A2,A1,Th10,PARTFUN1:56;
end;
theorem Th12:
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
proof
let X be TopSpace;
let Y be non empty TopSpace;
let A be open closed Subset of X;
let f be continuous Function of X|A, Y;
let g be continuous Function of X|A`, Y;
A\/A` = [#]X by PRE_TOPC:2;
then
A1: X|(A\/A`) = the TopStruct of X by TSEP_1:93;
A misses A` by XBOOLE_1:79;
then
A2: f+*g is continuous Function of X|(A\/A`), Y by Th11;
the TopStruct of Y = the TopStruct of Y;
hence thesis by A2,A1,YELLOW12:36;
end;
begin :: Niemytzki plane
theorem Th13:
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)
proof
let n be Element of NAT;
let a be Point of TOP-REAL n;
let r be positive Real;
a-a = 0.TOP-REAL n by RLVECT_1:5;
then |.a-a.| = 0 by EUCLID_2:39;
hence thesis by TOPREAL9:7;
end;
definition
func y=0-line -> Subset of TOP-REAL 2 equals
the set of all |[x,0]|;
coherence
proof
set A = the set of all |[x,0]|;
A c= the carrier of TOP-REAL 2
proof
let a be object;
assume a in A;
then ex x st a = |[x,0]|;
hence thesis;
end;
hence thesis;
end;
func y>=0-plane -> Subset of TOP-REAL 2 equals
{|[x,y]|: y >= 0};
coherence
proof
set A = {|[x,y]|: y >= 0};
A c= the carrier of TOP-REAL 2
proof
let a be object;
assume a in A;
then ex x,y st a = |[x,y]| & y >= 0;
hence thesis;
end;
hence thesis;
end;
end;
theorem
for a,b being set holds <*a,b*> in y=0-line iff a in REAL & b = 0
proof
let a,b be set;
A1: <*a,b*> in y=0-line iff ex x st <*a,b*> = |[x,0]|;
hereby
assume <*a,b*> in y=0-line;
then consider x,y such that
A3: <*a,b*> = |[x,0]| by A1;
<*a,b*>.1 = x by A3,FINSEQ_1:44;
hence a in REAL by XREAL_0:def 1;
<*a,b*>.2 = b;
hence b = 0 by A3,FINSEQ_1:44;
end;
assume a in REAL;
then reconsider x = a as Real;
|[x,0]| = <*a,0 *>;
hence thesis;
end;
theorem Th15:
for a,b being Real holds |[a,b]| in y=0-line iff b = 0
proof
let a,b be Real;
|[a,b]| in y=0-line iff ex x st |[a,b]| = |[x,0]|;
hence thesis by SPPOL_2:1;
end;
theorem Th16:
card y=0-line = continuum
proof
deffunc F(Real) = |[$1,0]|;
consider f being Function such that
A1: dom f = REAL and
A2: for r being Element of REAL holds f.r = F(r) from FUNCT_1:sch 4;
REAL, y=0-line are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A3: x in dom f and
A4: y in dom f;
reconsider x,y as Element of REAL by A3,A4,A1;
A5: f.y = |[y,0]| by A2;
f.x = |[x,0]| by A2;
hence thesis by A5,SPPOL_2:1;
end;
thus dom f = REAL by A1;
thus rng f c= y=0-line
proof
let a be object;
assume a in rng f;
then consider b being object such that
A6: b in dom f and
A7: a = f.b by FUNCT_1:def 3;
reconsider b as Element of REAL by A1,A6;
a = |[b,0]| by A2,A7;
hence thesis;
end;
let a be object;
assume
A8: a in y=0-line;
then reconsider a as Point of TOP-REAL 2;
reconsider a1 = a`1 as Element of REAL by XREAL_0:def 1;
A9: a = |[a`1,a`2]| by EUCLID:53;
then a`2 = 0 by A8,Th15;
then a = f.a1 by A2,A9;
hence thesis by A1,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5,TOPGEN_3:def 4;
end;
theorem
for a,b being set holds <*a,b*> in y>=0-plane iff a in REAL & ex y st
b = y & y >= 0
proof
let a,b be set;
hereby
assume <*a,b*> in y>=0-plane;
then consider x,y such that
A2: <*a,b*> = |[x,y]| and
A3: y >= 0;
<*a,b*>.1 = x by A2,FINSEQ_1:44;
hence a in REAL by XREAL_0:def 1;
take y;
<*a,b*>.2 = b;
hence b = y & y >= 0 by A3,A2,FINSEQ_1:44;
end;
assume a in REAL;
then reconsider x = a as Real;
given y such that
A4: b = y and
A5: y >= 0;
|[x,y]| = <*a,b*> by A4;
hence thesis by A5;
end;
theorem Th18:
for a,b being Real holds |[a,b]| in y>=0-plane iff b >= 0
proof
let a,b be Real;
|[a,b]| in y>=0-plane iff ex x,y st |[a,b]| = |[x,y]| & y >= 0;
hence thesis by SPPOL_2:1;
end;
registration
cluster y=0-line -> non empty;
coherence by Th15;
cluster y>=0-plane -> non empty;
coherence by Th18;
end;
theorem Th19:
y=0-line c= y>=0-plane
proof
let x be object;
assume x in y=0-line;
then reconsider x as Element of y=0-line;
A1: x = |[x`1,x`2]| by EUCLID:53;
then x`2 = 0 by Th15;
hence thesis by A1;
end;
theorem Th20:
for a,b,r being Real st r > 0 holds Ball(|[a,b]|,r) c=
y>=0-plane iff r <= b
proof
let a,b,r be Real such that
A1: r > 0;
hereby
A2: |[a,b]| in Ball(|[a,b]|,r) by A1,Th13;
assume that
A3: Ball(|[a,b]|,r) c= y>=0-plane and
A4: r > b;
reconsider b as non negative Real by A2,A3,Th18;
reconsider br=b-r as negative Real by A4,XREAL_1:49;
set y = br/2;
reconsider r as positive Real by A1;
|[a,y]|-|[a,b]| = |[a-a,y-b]| by EUCLID:62;
then
A5: |.|[a,y]|-|[a,b]|.| = |.y-b.| by TOPREAL6:23
.= |.b-y.| by COMPLEX1:60
.= (b+r)/2 by ABSVALUE:def 1;
b+r < r+r by A4,XREAL_1:6;
then (b+r)/2 < (r+r)/2 by XREAL_1:74;
then |[a,y]| in Ball(|[a,b]|,r) by A5,TOPREAL9:7;
hence contradiction by A3,Th18;
end;
assume
A6: r <= b;
let x be object;
assume
A7: x in Ball(|[a,b]|,r);
then reconsider z = x as Element of TOP-REAL 2;
A8: |.z-|[a,b]|.| < r by A7,TOPREAL9:7;
A9: |[z`1-a,z`2-b]|`1 = z`1-a by EUCLID:52;
A10: |[z`1-a,z`2-b]|`2 = z`2-b by EUCLID:52;
A11: z = |[z`1,z`2]| by EUCLID:53;
then z-|[a,b]| = |[z`1-a,z`2-b]| by EUCLID:62;
then |.z-|[a,b]|.| = sqrt((z`1-a)^2+(z`2-b)^2) by A9,A10,JGRAPH_1:30;
then |.z`2-b.| <= |.z-|[a,b]|.| by COMPLEX1:79;
then |.z`2-b.| < r by A8,XXREAL_0:2;
then
A12: |.b-z`2.| < r by COMPLEX1:60;
now
assume z`2 < 0;
then b-z`2 > b by XREAL_1:46;
then b-z`2 > r by A6,XXREAL_0:2;
hence contradiction by A1,A12,ABSVALUE:def 1;
end;
hence thesis by A11;
end;
theorem Th21:
for a,b,r being Real st r > 0 & b >= 0 holds Ball(|[a,b]|
,r) misses y=0-line iff r <= b
proof
let a,b,r be Real;
assume that
A1: r > 0 and
A2: b >= 0;
hereby
A3: |[a,0]| in y=0-line;
assume that
A4: Ball(|[a,b]|,r) misses y=0-line and
A5: r > b;
|[a,0]|-|[a,b]| = |[a-a,0-b]| by EUCLID:62;
then |.|[a,0]|-|[a,b]|.| = |.0-b.| by TOPREAL6:23
.= |.b-0 .| by COMPLEX1:60;
then |.|[a,0]|-|[a,b]|.| < r by A2,A5,ABSVALUE:def 1;
then |[a,0]| in Ball(|[a,b]|,r) by TOPREAL9:7;
hence contradiction by A3,A4,XBOOLE_0:3;
end;
assume
A6: r <= b;
assume Ball(|[a,b]|,r) meets y=0-line;
then consider x being object such that
A7: x in Ball(|[a,b]|,r) and
A8: x in y=0-line by XBOOLE_0:3;
reconsider x as Element of TOP-REAL 2 by A7;
A9: x = |[x`1,x`2]| by EUCLID:53;
then x`2 = 0 by A8,Th15;
then
A10: x-|[a,b]| = |[x`1-a,0-b]| by A9,EUCLID:62;
then
A11: (x-|[a,b]|)`2 = 0-b by EUCLID:52;
(x-|[a,b]|)`1 = x`1-a by A10,EUCLID:52;
then |.x-|[a,b]|.| = sqrt((x`1-a)^2+(0-b)^2) by A11,JGRAPH_1:30;
then |.x-|[a,b]|.| >= |.0-b.| by COMPLEX1:79;
then
A12: |.x-|[a,b]|.| >= |.b-0 .| by COMPLEX1:60;
|.x-|[a,b]|.| < r by A7,TOPREAL9:7;
then |.b.| < r by A12,XXREAL_0:2;
hence contradiction by A1,A6,ABSVALUE:def 1;
end;
theorem Th22:
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)
proof
let n be Element of NAT, a,b be Element of TOP-REAL n, r1,r2 be positive
Real;
assume |.a-b.| <= r1-r2;
then
A1: |.b-a.| <= r1-r2 by TOPRNS_1:27;
let x be object;
assume
A2: x in Ball(b,r2);
then reconsider x as Element of TOP-REAL n;
|.x-b.| < r2 by A2,TOPREAL9:7;
then
A3: |.x-b.|+|.b-a.| < r2+(r1-r2) by A1,XREAL_1:8;
|.x-a.| <= |.x-b.|+|.b-a.| by TOPRNS_1:34;
then |.x-a.| < r2+(r1-r2) by A3,XXREAL_0:2;
hence thesis by TOPREAL9:7;
end;
theorem Th23:
for a being Real, r1,r2 being positive Real st
r1 <= r2 holds Ball(|[a,r1]|,r1) c= Ball(|[a,r2]|,r2)
proof
let a be Real;
let r1,r2 be positive Real;
assume r1 <= r2;
then
A1: r2-r1 >= 0 by XREAL_1:48;
let x be object;
assume
A2: x in Ball(|[a,r1]|,r1);
then reconsider x as Element of TOP-REAL 2;
A3: |.x-|[a,r1]|.| < r1 by A2,TOPREAL9:7;
|[a,r1]|-|[a,r2]| = |[a-a,r1-r2]| by EUCLID:62;
then |.|[a,r1]|-|[a,r2]|.| = |.r1-r2.| by TOPREAL6:23;
then |.|[a,r1]|-|[a,r2]|.| = |.r2-r1.| by COMPLEX1:60;
then |.|[a,r1]|-|[a,r2]|.| = r2-r1 by A1,ABSVALUE:def 1;
then
A4: |.x-|[a,r1]|.|+|.|[a,r1]|-|[a,r2]|.| < r1+(r2-r1) by A3,XREAL_1:8;
|.x-|[a,r2]|.| <= |.x-|[a,r1]|.|+|.|[a,r1]|-|[a,r2]|.| by TOPRNS_1:34;
then |.x-|[a,r2]|.| < r2 by A4,XXREAL_0:2;
hence thesis by TOPREAL9:7;
end;
theorem Th24:
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
proof
let T1,T2 be non empty TopSpace;
let B1 be Neighborhood_System of T1;
let B2 be Neighborhood_System of T2;
A1: dom B1 = the carrier of T1 by PARTFUN1:def 2;
A2: dom B2 = the carrier of T2 by PARTFUN1:def 2;
A3: UniCl Union B2 = the topology of T2 by YELLOW_9:22;
A4: UniCl Union B1 = the topology of T1 by YELLOW_9:22;
assume B1 = B2;
hence thesis by A4,A3,A1,A2;
end;
definition
::$N Niemytzki plane
func Niemytzki-plane -> strict non empty TopSpace means
:Def3:
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};
existence
proof
defpred P[object] means $1 in y=0-line;
deffunc F1(Element of TOP-REAL 2) = {Ball(|[$1`1,r]|,r) \/ {$1} where r is
Real: r > 0};
set X = y>=0-plane;
deffunc F2(Element of TOP-REAL 2) = {Ball($1,r) /\ X where r is
Real: r > 0};
consider B being ManySortedSet of X such that
A1: for a being Element of X st a in X holds (P[a] implies B.a = F1(a)
) & (not P[a] implies B.a = F2(a)) from PRE_CIRC:sch 2;
B is non-empty
proof
let z be object;
assume z in X;
then reconsider s = z as Element of X;
per cases;
suppose
A2: P[z];
set r = the positive Element of REAL;
set a = |[s`1,r]|;
B.s = F1(s) by A2,A1;
then Ball(a,r) \/ {s} in B.s;
hence thesis;
end;
suppose
A3: not P[z];
set r = the positive Element of REAL;
B.s = F2(s) by A3,A1;
then Ball(s,r) /\ X in B.s;
hence thesis;
end;
end;
then reconsider B as non-empty ManySortedSet of X;
A4: rng B c= bool bool X
proof
let w be object;
reconsider ww=w as set by TARSKI:1;
assume w in rng B;
then consider a being object such that
A5: a in dom B and
A6: w = B.a by FUNCT_1:def 3;
reconsider a as Element of X by A5;
ww c= bool X
proof
let z be object;
reconsider zz=z as set by TARSKI:1;
assume
A7: z in ww;
per cases by A1,A6;
suppose
w = F1(a);
then consider r being Real such that
A8: z = Ball(|[a`1,r]|,r) \/ {a} and
A9: r > 0 by A7;
Ball(|[a`1,r]|,r) c= X by A9,Th20;
then zz c= X by A8,XBOOLE_1:8;
hence thesis;
end;
suppose
w = F2(a);
then
ex r being Real st z = Ball(a,r) /\ X & r > 0 by A7;
then zz c= X by XBOOLE_1:17;
hence thesis;
end;
end;
hence thesis;
end;
A10: for x,y,U being set st x in U & U in B.y & y in X ex V being set st V
in B.x & V c= U
proof
let x,y,U be set;
assume
A11: x in U;
assume
A12: U in B.y;
assume y in X;
then reconsider y as Element of X;
per cases;
suppose
P[y];
then B.y = F1(y) by A1;
then consider r being Real such that
A13: U = Ball(|[y`1,r]|,r) \/ {y} and
A14: r > 0 by A12;
A15: x in Ball(|[y`1,r]|,r) or x = y by A11,A13,ZFMISC_1:136;
then reconsider z = x as Element of TOP-REAL 2;
now
set r2 = r-|.z-|[y`1,r]|.|;
assume
A16: x in Ball(|[y`1,r]|,r);
take V = Ball(z,r2) /\ X;
|.z-|[y`1,r]|.| < r by A16,TOPREAL9:7;
then reconsider r1 = r, r2 as positive Real
by XREAL_1:50;
A17: r2 > 0;
Ball(|[y`1,r]|,r) misses y=0-line by A14,Th21;
then
A18: not P[x] by A16,XBOOLE_0:3;
Ball(|[y`1,r]|,r) c= X by A14,Th20;
then B.z = F2(z) by A16,A18,A1;
hence V in B.x by A17;
A19: Ball(|[y`1,r]|,r) c= U by A13,XBOOLE_1:7;
r1-r2 = |.|[y`1,r]|-z.| by TOPRNS_1:27;
then
A20: Ball(z,r2) c= Ball(|[y`1,r]|,r1) by Th22;
V c= Ball(z,r2) by XBOOLE_1:17;
then V c= Ball(|[y`1,r]|,r1) by A20;
hence V c= U by A19;
end;
hence thesis by A12,A15;
end;
suppose
not P[y];
then B.y = F2(y) by A1;
then consider r being Real such that
A21: U = Ball(y,r) /\ X and
r > 0 by A12;
reconsider z = x as Element of X by A11,A21,XBOOLE_0:def 4;
set r2 = r-|.z-y.|;
z in Ball(y,r) by A11,A21,XBOOLE_0:def 4;
then |.z-y.| < r by TOPREAL9:7;
then reconsider r1 = r, r2 as positive Real
by XREAL_1:50;
A22: z = |[z`1,z`2]| by EUCLID:53;
per cases;
suppose
A23: P[z];
then z`2 = 0 by A22,Th15;
then |[z`1,r2/2]|-z = |[z`1-z`1,r2/2-0]| by A22,EUCLID:62;
then |.|[z`1,r2/2]|-z.| = |.r2/2.| by TOPREAL6:23
.= r2/2 by ABSVALUE:def 1;
then |.|[z`1,r2/2]|-y.| <= r2/2+|.z-y.| by TOPRNS_1:34;
then |.y-|[z`1,r2/2]|.| <= r-r2/2 by TOPRNS_1:27;
then
A24: Ball(|[z`1,r2/2]|,r2/2) c= Ball(y,r1) by Th22;
set V = Ball(|[z`1,r2/2]|,r2/2) \/ {z};
take V;
B.z = F1(z) by A23,A1;
hence V in B.x;
A25: {z} c= U by A11,ZFMISC_1:31;
Ball(|[z`1,r2/2]|,r2/2) c= X by Th20;
then Ball(|[z`1,r2/2]|,r2/2) c= U by A24,A21,XBOOLE_1:19;
hence thesis by A25,XBOOLE_1:8;
end;
suppose
A26: not P[z];
take V = Ball(z,r2) /\ X;
B.z = F2(z) by A26,A1;
hence V in B.x;
|.y-z.| = r1-r2 by TOPRNS_1:27;
hence thesis by A21,Th22,XBOOLE_1:26;
end;
end;
end;
A27: for x,U1,U2 being set st x in X & U1 in B.x & U2 in B.x ex U being
set st U in B.x & U c= U1 /\ U2
proof
let x,U1,U2 be set;
assume x in X;
then reconsider z = x as Element of X;
assume that
A28: U1 in B.x and
A29: U2 in B.x;
per cases;
suppose
P[z];
then
A30: B.x = F1(z) by A1;
then consider r1 being Real such that
A31: U1 = Ball(|[z`1,r1]|,r1) \/ {z} and
A32: r1 > 0 by A28;
consider r2 being Real such that
A33: U2 = Ball(|[z`1,r2]|,r2) \/ {z} and
A34: r2 > 0 by A29,A30;
r1 <= r2 or r1 >= r2;
then consider U being set such that
A35: r1 <= r2 & U = U1 or r1 >= r2 & U = U2;
A36: U c= U2 by A31,A32,A33,A35,Th23,XBOOLE_1:9;
take U;
thus U in B.x by A28,A29,A35;
U c= U1 by A31,A33,A34,A35,Th23,XBOOLE_1:9;
hence thesis by A36,XBOOLE_1:19;
end;
suppose
not P[z];
then
A37: B.x = F2(z) by A1;
then consider r1 being Real such that
A38: U1 = Ball(z,r1) /\ X and
r1 > 0 by A28;
consider r2 being Real such that
A39: U2 = Ball(z,r2) /\ X and
r2 > 0 by A29,A37;
r1 <= r2 or r1 >= r2;
then consider U being set such that
A40: r1 <= r2 & U = U1 or r1 >= r2 & U = U2;
A41: U c= U2 by A38,A39,A40,JORDAN:18,XBOOLE_1:26;
take U;
thus U in B.x by A28,A29,A40;
U c= U1 by A38,A39,A40,JORDAN:18,XBOOLE_1:26;
hence thesis by A41,XBOOLE_1:19;
end;
end;
for x,U being set st x in X & U in B.x holds x in U
proof
let x,U be set;
assume x in X;
then reconsider a = x as Element of X;
assume
A42: U in B.x;
per cases by A1;
suppose
A43: B.x = F1(a);
A44: a in {a} by TARSKI:def 1;
ex r being Real st U = Ball(|[a`1,r]|,r
) \/ {a } & r > 0 by A43,A42;
hence thesis by A44,XBOOLE_0:def 3;
end;
suppose
B.x = F2(a);
then consider r being Real such that
A45: U = Ball(a,r) /\ X and
A46: r > 0 by A42;
a in Ball(a,r) by A46,Th13;
hence thesis by A45,XBOOLE_0:def 4;
end;
end;
then consider P being Subset-Family of X such that
P = Union B and
A47: for T being TopStruct st the carrier of T = X & the topology of
T = UniCl P holds T is TopSpace & for T9 being non empty TopSpace st T9 = T
holds B is Neighborhood_System of T9 by A27,A4,A10,TOPGEN_3:3;
set T = TopStruct(#X, UniCl P#);
reconsider T as non empty strict TopSpace by A47;
reconsider B as Neighborhood_System of T by A47;
take T;
thus the carrier of T = X;
take B;
hereby
defpred R[Real] means $1 > 0;
let x;
deffunc a1(Real) = Ball(|[x,$1]|,$1) \/ {|[x,0]|};
deffunc a2(Real) = Ball(|[|[x,0]|`1,$1]|,$1) \/ {|[x,0]|};
A48: |[x,0]| in X;
A49: for r being Real holds a1(r) = a2(r) by EUCLID:52;
A50: {a2(r) where r is Real: R[r]}
c= {a1(r1) where r1 is Real: R[r1]}
proof let e be object;
assume e in {a2(r) where r is Real: R[r]};
then consider r being Real such that
A51: e = a2(r) & R[r];
e = a1(r) & R[r] by A49,A51;
hence e in {a1(r1) where r1 is Real: R[r1]};
end;
{a1(r) where r is Real: R[r]}
c= {a2(r1) where r1 is Real: R[r1]}
proof let e be object;
assume e in {a1(r) where r is Real: R[r]};
then consider r being Real such that
A52: e = a1(r) & R[r];
e = a2(r) & R[r] by A49,A52;
hence e in {a2(r1) where r1 is Real: R[r1]};
end;
then
A53: {a1(r) where r is Real: R[r]}
= {a2(r) where r is Real: R[r]} by A50;
P[ |[x,0]| ];
then B.(|[x,0]|) = F1(|[x,0]|) by A48,A1;
hence B.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|}
where r is Real: r > 0} by A53;
end;
let x,y;
assume
A54: y > 0;
then
A55: |[x,y]| in X;
not |[x,y]| in y=0-line by A54,Th15;
hence thesis by A55,A1;
end;
uniqueness
proof
let T1,T2 be strict non empty TopSpace such that
A56: the carrier of T1 = y>=0-plane and
A57: ex B being Neighborhood_System of T1 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} and
A58: the carrier of T2 = y>=0-plane and
A59: ex B being Neighborhood_System of T2 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};
consider B2 being Neighborhood_System of T2 such that
A60: for x holds B2.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r
is Real: r > 0} and
A61: for x,y st y > 0 holds B2.(|[x,y]|) = {Ball(|[x,y]|,r) /\
y>=0-plane where r is Real: r > 0} by A59;
consider B1 being Neighborhood_System of T1 such that
A62: for x holds B1.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r
is Real: r > 0} and
A63: for x,y st y > 0 holds B1.(|[x,y]|) = {Ball(|[x,y]|,r) /\
y>=0-plane where r is Real: r > 0} by A57;
now
let a be object;
assume a in y>=0-plane;
then reconsider z = a as Element of y>=0-plane;
A64: z = |[z`1,z`2]| by EUCLID:53;
then z`2 = 0 or z`2 > 0 by Th18;
then z`2 = 0 & B1.z = {Ball(|[z`1,r]|,r) \/ {|[z`1,0]|} where r is
Real: r > 0} & B2.z = {Ball(|[z`1,r]|,r) \/ {|[z`1,0]|} where r is
Real: r > 0} or z`2 > 0 & B1.z = {Ball(|[z`1,z`2]|,r) /\ y>=0-plane
where r is Real: r > 0} & B2.z = {Ball(|[z`1,z`2]|,r) /\ y>=0-plane
where r is Real: r > 0} by A62,A63,A60,A61,A64;
hence B1.a = B2.a;
end;
hence thesis by A56,A58,Th24,PBOOLE:3;
end;
end;
theorem Th25:
y>=0-plane \ y=0-line is open Subset of Niemytzki-plane
proof
consider BB being Neighborhood_System of Niemytzki-plane such that
for x holds BB.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is
Real: r > 0} and
A1: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane
where r is Real: r > 0} by Def3;
A2: the carrier of Niemytzki-plane = y>=0-plane by Def3;
then reconsider A = y>=0-plane \ y=0-line as Subset of Niemytzki-plane by
XBOOLE_1:36;
now
let a be Point of Niemytzki-plane;
assume
A3: a in A;
then a in y>=0-plane by XBOOLE_0:def 5;
then consider x,y such that
A4: a = |[x,y]| and
A5: y >= 0;
set B = Ball(|[x,y]|,y)/\y>=0-plane;
reconsider B as Subset of Niemytzki-plane by A2,XBOOLE_1:17;
not a in y=0-line by A3,XBOOLE_0:def 5;
then
A6: y <> 0 by A4;
then B in {Ball(|[x,y]|,r) /\ y>=0-plane where r is Real: r >
0} by A5;
then
A7: B in BB.a by A1,A4,A5,A6;
take B;
dom BB = the carrier of Niemytzki-plane by PARTFUN1:def 2;
hence B in Union BB by A7,CARD_5:2;
thus a in B by A7,YELLOW_8:12;
Ball(|[x,y]|,y) c= y>=0-plane by A5,A6,Th20;
then B = Ball(|[x,y]|,y) by XBOOLE_1:28;
then B misses y=0-line by A5,A6,Th21;
hence B c= A by A2,XBOOLE_1:86;
end;
hence thesis by YELLOW_9:31;
end;
Lm1: the carrier of Niemytzki-plane = y>=0-plane by Def3;
theorem Th26:
y=0-line is closed Subset of Niemytzki-plane
proof
reconsider B = y=0-line as Subset of Niemytzki-plane by Def3,Th19;
reconsider A = y>=0-plane \ y=0-line as open Subset of Niemytzki-plane by
Th25;
B` = A by Def3;
then A` = y=0-line;
hence thesis;
end;
theorem Th27:
for x being Real, r being positive Real holds
Ball(|[x,r]|,r) \/ {|[x,0]|} is open Subset of Niemytzki-plane
proof
let x be Real;
let r be positive Real;
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then reconsider a = |[x,0]| as Point of Niemytzki-plane by Th18;
consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is
Real: q > 0} and
for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane
where q is Real: q > 0} by Def3;
BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is Real:
q > 0} by A1;
then Ball(|[x,r]|,r) \/ {|[x,0]|} in BB.a;
hence thesis by YELLOW_8:12;
end;
theorem Th28:
for x being Real for y,r being positive Real
holds Ball(|[x,y]|,r) /\ y>=0-plane is open Subset of Niemytzki-plane
proof
let x be Real;
let y,r be positive Real;
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then reconsider a = |[x,y]| as Point of Niemytzki-plane by Th18;
consider BB being Neighborhood_System of Niemytzki-plane such that
for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is
Real: q > 0} and
A1: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane
where q is Real: q > 0} by Def3;
BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane where q is Real
: q > 0} by A1;
then Ball(|[x,y]|,r) /\ y>=0-plane in BB.a;
hence thesis by YELLOW_8:12;
end;
theorem Th29:
for x,y being Real for r being positive Real st
r <= y holds Ball(|[x,y]|,r) is open Subset of Niemytzki-plane
proof
let x,y be Real;
let r be positive Real;
assume
A1: r <= y;
A2: Ball(|[x,y]|,r) c= y>=0-plane
proof
let a be object;
assume
A3: a in Ball(|[x,y]|,r);
then reconsider z = a as Element of TOP-REAL 2;
A4: z`2 < 0 implies y-z`2 > y & |.y-z`2.| = y-z`2 by A1,ABSVALUE:def 1
,XREAL_1:46;
A5: z = |[z`1,z`2]| by EUCLID:53;
then
A6: z-|[x,y]| = |[z`1-x,z`2-y]| by EUCLID:62;
then
A7: (z-|[x,y]|)`2 = z`2-y by EUCLID:52;
(z-|[x,y]|)`1 = z`1-x by A6,EUCLID:52;
then |.z-|[x,y]|.| = sqrt((z`1-x)^2+(z`2-y)^2) by A7,JGRAPH_1:30;
then |.z-|[x,y]|.| >= |.z`2-y.| by COMPLEX1:79;
then
A8: |.z-|[x,y]|.| >= |.y-z`2.| by COMPLEX1:60;
|.z-|[x,y]|.| < r by A3,TOPREAL9:7;
then |.y-z`2.| < r by A8,XXREAL_0:2;
hence thesis by A4,A1,A5,XXREAL_0:2;
end;
Ball(|[x,y]|,r) /\ y>=0-plane is open Subset of Niemytzki-plane by A1,Th28;
hence thesis by A2,XBOOLE_1:28;
end;
theorem Th30:
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
proof
let p be Point of Niemytzki-plane;
let r be positive Real;
consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is
Real: q > 0} and
A2: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane
where q is Real: q > 0} by Def3;
A3: the carrier of Niemytzki-plane = y>=0-plane by Def3;
p in the carrier of Niemytzki-plane;
then reconsider p9 = p as Point of TOP-REAL 2 by A3;
A4: p = |[p9`1,p9`2]| by EUCLID:53;
per cases by A3,A4,Th18;
suppose
A5: p9`2 = 0;
then
BB.p = {Ball(|[p9`1,q]|,q) \/ {|[p9`1,0]|} where q is Real:
q > 0} by A1,A4;
then
A6: Ball(|[p9`1,r/2]|,r/2) \/ {|[p9`1,0]|} in BB.p;
BB.p c= the topology of Niemytzki-plane by TOPS_2:64;
then reconsider U = Ball(|[p9`1,r/2]|,r/2) \/ {p} as open Subset of
Niemytzki-plane by A6,A4,A5,PRE_TOPC:def 2;
take a = |[p9`1,r/2]|, U;
thus p in U by ZFMISC_1:136;
A7: r/2 < r/2+r/2 by XREAL_1:29;
a in Ball(a,r/2) by Th13;
hence a in U by XBOOLE_0:def 3;
let b be Point of TOP-REAL 2;
assume b in U;
then
A8: b in Ball(a,r/2) or b = p by ZFMISC_1:136;
p9-a = |[p9`1-p9`1,0-r/2]| by A4,A5,EUCLID:62;
then |.p9-a.| = |.0-r/2.| by TOPREAL6:23
.= |.r/2-0 .| by COMPLEX1:60
.= r/2 by ABSVALUE:def 1;
then |.b-a.| <= r/2 by A8,TOPREAL9:7;
hence thesis by A7,XXREAL_0:2;
end;
suppose
A9: p9`2 > 0;
then BB.p = {Ball(|[p9`1,p9`2]|,q) /\ y>=0-plane
where q is Real: q > 0} by A2,A4;
then
A10: Ball(p9,r/2) /\ y>=0-plane in BB.p by A4;
BB.p c= the topology of Niemytzki-plane by TOPS_2:64;
then reconsider U = Ball(p9,r/2) /\ y>=0-plane as open Subset of
Niemytzki-plane by A10,PRE_TOPC:def 2;
take a = p9, U;
A11: p in Ball(a,r/2) by Th13;
p in y>=0-plane by A4,A9;
hence p in U & a in U by A11,XBOOLE_0:def 4;
let b be Point of TOP-REAL 2;
assume b in U;
then b in Ball(a,r/2) by XBOOLE_0:def 4;
then
A12: |.b-a.| <= r/2 by TOPREAL9:7;
r/2 < r/2+r/2 by XREAL_1:29;
hence thesis by A12,XXREAL_0:2;
end;
end;
theorem Th31:
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]|
proof
let x,y be Real;
let r be positive Real;
x < x+r/2 by XREAL_1:39;
then consider w being Rational such that
A1: x < w and
A2: w < x+r/2 by RAT_1:7;
A3: w-x > 0 by A1,XREAL_1:50;
y < y+r/2 by XREAL_1:39;
then consider v being Rational such that
A4: y < v and
A5: v < y+r/2 by RAT_1:7;
A6: v-y > 0 by A4,XREAL_1:50;
|[w,v]|-|[x,v]| = |[w-x,v-v]| by EUCLID:62;
then |.|[w,v]|-|[x,v]|.| = |.w-x.| by TOPREAL6:23;
then |.|[w,v]|-|[x,v]|.| = w-x by A3,ABSVALUE:def 1;
then
A7: |.|[w,v]|-|[x,v]|.| < x+r/2-x by A2,XREAL_1:9;
take w,v;
A8: |[x,v]|-|[x,y]| = |[x-x,v-y]| by EUCLID:62;
A9: |.|[w,v]|-|[x,y]|.| <= |.|[w,v]|-|[x,v]|.|+|.|[x,v]|-|[x,y]|.| by
TOPRNS_1:34;
|.|[x,v]|-|[x,y]|.| = |.v-y.| by A8,TOPREAL6:23;
then |.|[x,v]|-|[x,y]|.| = v-y by A6,ABSVALUE:def 1;
then |.|[x,v]|-|[x,y]|.| <= y+r/2-y by A5,XREAL_1:9;
then |.|[w,v]|-|[x,v]|.|+|.|[x,v]|-|[x,y]|.| < x+r/2-x+(y+r/2-y) by A7,
XREAL_1:8;
then |.|[w,v]|-|[x,y]|.| < r by A9,XXREAL_0:2;
hence |[w,v]| in Ball(|[x,y]|,r) by TOPREAL9:7;
thus thesis by A4,SPPOL_2:1;
end;
theorem Th32:
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
proof
let A be Subset of Niemytzki-plane;
assume
A1: A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*>;
let s be set;
thus Cl (A\{s}) c= [#] Niemytzki-plane;
let x be object;
assume x in [#] Niemytzki-plane;
then reconsider a = x as Element of Niemytzki-plane;
reconsider b = a as Element of y>=0-plane by Def3;
consider BB being Neighborhood_System of Niemytzki-plane such that
A2: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is
Real: q > 0} and
A3: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane
where q is Real: q > 0} by Def3;
A4: a = |[b`1,b`2]| by EUCLID:53;
for U being set st U in BB.a holds U meets A\{s}
proof
let U be set;
assume
A5: U in BB.a;
per cases by A4,Th18;
suppose
A6: b`2 = 0;
then
BB.a = {Ball(|[b`1,q]|,q) \/ {|[b`1,0]|} where q is Real
: q > 0} by A2,A4;
then consider q being Real such that
A7: U = Ball(|[b`1,q]|,q) \/ {a} and
A8: q > 0 by A4,A5,A6;
reconsider q as positive Real by A8;
consider w1,v1 being Rational such that
A9: |[w1,v1]| in Ball(|[b`1,q]|,q) and
A10: |[w1,v1]| <> |[b`1,q]| by Th31;
A11: |[w1,v1]| in U by A7,A9,XBOOLE_0:def 3;
set q2 = |.|[w1,v1]|-|[b`1,q]|.|;
|[w1,v1]|-|[b`1,q]| <> 0.TOP-REAL 2 by A10,RLVECT_1:21;
then q2 <> 0 by EUCLID_2:42;
then reconsider q2 as positive Real;
A12: q2 < q by A9,TOPREAL9:7;
consider w2,v2 being Rational such that
A13: |[w2,v2]| in Ball(|[b`1,q]|,q2) and
|[w2,v2]| <> |[b`1,q]| by Th31;
|.|[w2,v2]|-|[b`1,q]|.| < q2 by A13,TOPREAL9:7;
then |.|[w2,v2]|-|[b`1,q]|.| < q by A12,XXREAL_0:2;
then
A14: |[w2,v2]| in Ball(|[b`1,q]|,q) by TOPREAL9:7;
then
A15: |[w2,v2]| in U by A7,XBOOLE_0:def 3;
A16: Ball(|[b`1,q]|,q) misses y=0-line by Th21;
Ball(|[b`1,q]|,q) c= y>=0-plane by Th20;
then
A17: Ball(|[b`1,q]|,q) c= y>=0-plane \ y=0-line by A16,XBOOLE_1:86;
A18: v1 in RAT by RAT_1:def 2;
w1 in RAT by RAT_1:def 2;
then |[w1,v1]| in product <*RAT, RAT*> by A18,FINSEQ_3:124;
then
A19: |[w1,v1]| in A by A17,A9,A1,XBOOLE_0:def 4;
A20: s = |[w1,v1]| or s <> |[w1,v1]|;
A21: v2 in RAT by RAT_1:def 2;
w2 in RAT by RAT_1:def 2;
then |[w2,v2]| in product <*RAT,RAT*> by A21,FINSEQ_3:124;
then
A22: |[w2,v2]| in A by A17,A14,A1,XBOOLE_0:def 4;
|[w2,v2]| <> |[w1,v1]| by A13,TOPREAL9:7;
then |[w1,v1]| in A\{s} or |[w2,v2]| in A\{s} by A20,A19,A22,ZFMISC_1:56;
hence thesis by A11,A15,XBOOLE_0:3;
end;
suppose
A23: b`2 > 0;
then BB.a = {Ball(|[b`1,b`2]|,q) /\ y>=0-plane
where q is Real: q > 0} by A3,A4;
then consider q being Real such that
A24: U = Ball(b,q) /\ y>=0-plane and
A25: q > 0 by A4,A5;
reconsider q, b2 = b`2 as positive Real by A23,A25;
reconsider q1 = min(q,b2) as positive Real by XXREAL_0:def 9;
consider w1,v1 being Rational such that
A26: |[w1,v1]| in Ball(b,q1) and
A27: |[w1,v1]| <> b by A4,Th31;
A28: v1 in RAT by RAT_1:def 2;
set q2 = |.|[w1,v1]|-b.|;
|[w1,v1]|-b <> 0.TOP-REAL 2 by A27,RLVECT_1:21;
then q2 <> 0 by EUCLID_2:42;
then reconsider q2 as positive Real;
A29: q2 < q1 by A26,TOPREAL9:7;
A30: q1 <= b`2 by XXREAL_0:17;
then
A31: Ball(b,q1) c= y>=0-plane by A4,Th20;
Ball(b,q1) misses y=0-line by A30,A4,Th21;
then
A32: Ball(b,q1) c= y>=0-plane \ y=0-line by A31,XBOOLE_1:86;
w1 in RAT by RAT_1:def 2;
then |[w1,v1]| in product <*RAT, RAT*> by A28,FINSEQ_3:124;
then
A33: |[w1,v1]| in A by A32,A26,A1,XBOOLE_0:def 4;
A34: s = |[w1,v1]| or s <> |[w1,v1]|;
consider w2,v2 being Rational such that
A35: |[w2,v2]| in Ball(b,q2) and
|[w2,v2]| <> b by A4,Th31;
A36: |[w2,v2]| <> |[w1,v1]| by A35,TOPREAL9:7;
|.|[w2,v2]|-b.| < q2 by A35,TOPREAL9:7;
then
A37: |.|[w2,v2]|-b.| < q1 by A29,XXREAL_0:2;
then
A38: |[w2,v2]| in Ball(b,q1) by TOPREAL9:7;
A39: q1 <= q by XXREAL_0:17;
then |.|[w2,v2]|-b.| < q by A37,XXREAL_0:2;
then |[w2,v2]| in Ball(b,q) by TOPREAL9:7;
then
A40: |[w2,v2]| in U by A24,A38,A31,XBOOLE_0:def 4;
A41: v2 in RAT by RAT_1:def 2;
w2 in RAT by RAT_1:def 2;
then |[w2,v2]| in product <*RAT,RAT*> by A41,FINSEQ_3:124;
then |[w2,v2]| in A by A32,A38,A1,XBOOLE_0:def 4;
then
A42: |[w1,v1]| in A\{s} or |[w2,v2]| in A\{s} by A34,A36,A33,ZFMISC_1:56;
q2 < q by A39,A29,XXREAL_0:2;
then |[w1,v1]| in Ball(b,q) by TOPREAL9:7;
then |[w1,v1]| in U by A24,A26,A31,XBOOLE_0:def 4;
hence thesis by A42,A40,XBOOLE_0:3;
end;
end;
hence thesis by TOPGEN_2:10;
end;
theorem Th33:
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
proof
let A be Subset of Niemytzki-plane;
assume
A1: A = y>=0-plane \ y=0-line;
let s be set;
reconsider B = A /\ product <*RAT,RAT*> as Subset of Niemytzki-plane;
thus Cl (A\{s}) c= [#] Niemytzki-plane;
B\{s} c= A\{s} by XBOOLE_1:17,33;
then Cl (B\{s}) c= Cl (A\{s}) by PRE_TOPC:19;
hence thesis by A1,Th32;
end;
theorem Th34:
for A being Subset of Niemytzki-plane st A = y>=0-plane \
y=0-line holds Cl A = [#] Niemytzki-plane
proof
let A be Subset of Niemytzki-plane;
A\{A} = A
proof
thus A\{A} c= A by XBOOLE_1:36;
let x be object;
not A in A;
hence thesis by ZFMISC_1:56;
end;
hence thesis by Th33;
end;
theorem Th35:
for A being Subset of Niemytzki-plane st A = y=0-line holds Cl A
= A & Int A = {}
proof
let A be Subset of Niemytzki-plane;
assume
A1: A = y=0-line;
then
A2: A` = y>=0-plane \ y=0-line by Def3;
thus Cl A = A by A1,Th26,PRE_TOPC:22;
thus Int A = (Cl A`)` by TOPS_1:def 1
.= ([#] Niemytzki-plane)` by A2,Th34
.= {} by XBOOLE_1:37;
end;
theorem Th36:
(y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> is dense Subset
of Niemytzki-plane
proof
(y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> c= y>=0-plane \ y=0-line
by XBOOLE_1:17;
then reconsider
A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> as Subset of
Niemytzki-plane by Th25,XBOOLE_1:1;
A\{A} = A
proof
thus A\{A} c= A by XBOOLE_1:36;
let x be object;
not A in A;
hence thesis by ZFMISC_1:56;
end;
then Cl A = [#] Niemytzki-plane by Th32;
hence thesis by TOPS_1:def 3;
end;
theorem
(y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> is dense-in-itself
Subset of Niemytzki-plane
proof
(y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> c= y>=0-plane \ y=0-line
by XBOOLE_1:17;
then reconsider
A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> as Subset of
Niemytzki-plane by Th25,XBOOLE_1:1;
A is dense-in-itself
proof
let a be object;
assume a in A;
then reconsider x = a as Point of Niemytzki-plane;
Cl (A\{x}) = the carrier of Niemytzki-plane by Th32;
then x is_an_accumulation_point_of A;
hence thesis by TOPGEN_1:def 3;
end;
hence thesis;
end;
theorem
y>=0-plane \ y=0-line is dense Subset of Niemytzki-plane
proof
reconsider A = y>=0-plane \ y=0-line as open Subset of Niemytzki-plane by
Th25;
Cl A = [#] Niemytzki-plane by Th34;
hence thesis by TOPS_1:def 3;
end;
theorem
y>=0-plane \ y=0-line is dense-in-itself Subset of Niemytzki-plane
proof
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then reconsider A = y>=0-plane \ y=0-line as Subset of Niemytzki-plane by
XBOOLE_1:36;
A is dense-in-itself
proof
let a be object;
assume a in A;
then reconsider x = a as Point of Niemytzki-plane;
Cl (A\{x}) = the carrier of Niemytzki-plane by Th33;
then x is_an_accumulation_point_of A;
hence thesis by TOPGEN_1:def 3;
end;
hence thesis;
end;
theorem
y=0-line is nowhere_dense Subset of Niemytzki-plane
proof
reconsider A = y=0-line as Subset of Niemytzki-plane by Def3,Th19;
Int Cl A = Int A by Th26,PRE_TOPC:22
.= {} by Th35;
hence thesis by TOPS_3:def 3;
end;
theorem Th41:
for A being Subset of Niemytzki-plane st A = y=0-line holds Der A is empty
proof
consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is
Real: r > 0} and
for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane
where r is Real: r > 0} by Def3;
let A be Subset of Niemytzki-plane;
assume that
A2: A = y=0-line and
A3: Der A is not empty;
set a = the Element of Der A;
a in Der A by A3;
then reconsider a as Point of Niemytzki-plane;
A4: a in Der A by A3;
a is_an_accumulation_point_of A by A3,TOPGEN_1:def 3;
then
A5: a in Cl (A \ {a});
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then a in y>=0-plane;
then reconsider b = a as Point of TOP-REAL 2;
A6: a = |[b`1,b`2]| by EUCLID:53;
A7: Der A c= Cl A by TOPGEN_1:28;
Cl A = A by A2,Th35;
then
A8: b`2 = 0 by A4,A7,A2,A6,Th15;
then
BB.a = {Ball(|[b`1,r]|,r) \/ {|[b`1,0]|} where r is Real:
r > 0 } by A1,A6;
then Ball(|[b`1,1]|,1) \/ {b} in BB.a by A6,A8;
then Ball(|[b`1,1]|,1) \/ {b} meets A \ {a} by A5,TOPGEN_2:9;
then consider z being object such that
A9: z in Ball(|[b`1,1]|,1) \/ {b} and
A10: z in A \ {a} by XBOOLE_0:3;
A11: z in A by A10,ZFMISC_1:56;
z <> a by A10,ZFMISC_1:56;
then
A12: z in Ball(|[b`1,1]|,1) by A9,ZFMISC_1:136;
reconsider z as Point of TOP-REAL 2 by A9;
A13: z = |[z`1,z`2]| by EUCLID:53;
then z`2 = 0 by A2,A11,Th15;
then
A14: z-|[b`1,1]| = |[z`1-b`1,0-1]| by A13,EUCLID:62;
A15: |[z`1-b`1,0-1]|`2 = 0-1 by EUCLID:52;
|[z`1-b`1,0-1]|`1 = z`1-b`1 by EUCLID:52;
then |.z-|[b`1,1]|.| = sqrt((z`1-b`1)^2+(-1)^2) by A14,A15,JGRAPH_1:30
.= sqrt((z`1-b`1)^2+1^2);
then
A16: |.z-|[b`1,1]|.| >= |.1.| by COMPLEX1:79;
|.z-|[b`1,1]|.| < 1 by A12,TOPREAL9:7;
then |.1.| < 1 by A16,XXREAL_0:2;
hence contradiction by ABSVALUE:4;
end;
theorem Th42:
for A being Subset of y=0-line holds A is closed Subset of Niemytzki-plane
proof
reconsider B = y=0-line as closed Subset of Niemytzki-plane by Th26;
let A be Subset of y=0-line;
A c= B;
then reconsider A as Subset of Niemytzki-plane by XBOOLE_1:1;
Der A c= Der B by TOPGEN_1:30;
then Der A c= {} by Th41;
then Der A = {};
then Cl A = A \/ {} by TOPGEN_1:29;
hence thesis;
end;
theorem Th43:
RAT is dense Subset of Sorgenfrey-line
proof
reconsider A = RAT as Subset of Sorgenfrey-line by NUMBERS:12,TOPGEN_3:def 2;
consider B being Subset-Family of REAL such that
A1: the topology of Sorgenfrey-line = UniCl B and
A2: B = {[.x,q.[ where x,q is Real: x < q & q is rational}
by TOPGEN_3:def 2;
the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;
then
A3: B is Basis of Sorgenfrey-line by A1,YELLOW_9:22;
A is dense
proof
thus Cl A c= the carrier of Sorgenfrey-line;
let x be object;
assume x in the carrier of Sorgenfrey-line;
then reconsider x as Point of Sorgenfrey-line;
now
let C be Subset of Sorgenfrey-line;
assume C in B;
then consider y,q being Real such that
A4: C = [.y,q.[ and
A5: y < q and
q is rational by A2;
assume x in C;
consider r being Rational such that
A6: y < r and
A7: r < q by A5,RAT_1:7;
A8: r in A by RAT_1:def 2;
r in C by A4,A6,A7,XXREAL_1:3;
hence A meets C by A8,XBOOLE_0:3;
end;
hence thesis by A3,YELLOW_9:37;
end;
hence thesis;
end;
theorem
Sorgenfrey-line is separable
by Th43,TOPGEN_1:def 12,TOPGEN_3:17;
theorem
Niemytzki-plane is separable
proof
reconsider A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> as dense
Subset of Niemytzki-plane by Th36;
A1: card A c= card product <*RAT, RAT*> by CARD_1:11,XBOOLE_1:17;
density Niemytzki-plane c= card A by TOPGEN_1:def 12;
then density Niemytzki-plane c= card product <*RAT,RAT*> by A1;
hence density Niemytzki-plane c= omega by Th8,CARD_4:6,TOPGEN_3:17;
end;
theorem
Niemytzki-plane is T_1
proof
set T = Niemytzki-plane;
let p,q be Point of T such that
A1: p <> q;
A2: q in the carrier of T;
A3: the carrier of T = y>=0-plane by Def3;
p in the carrier of T;
then reconsider p9 = p, q9 = q as Point of TOP-REAL 2 by A2,A3;
p9-q9 <> 0.TOP-REAL 2 by A1,RLVECT_1:21;
then |.p9-q9.| <> 0 by EUCLID_2:42;
then reconsider r = |.p9-q9.| as positive Real;
consider ap being Point of TOP-REAL 2, Up being open Subset of T such that
A4: p in Up and
ap in Up and
A5: for b being Point of TOP-REAL 2 st b in Up holds |.b-ap.| < r/2 by Th30;
consider aq being Point of TOP-REAL 2, Uq being open Subset of T such that
A6: q in Uq and
aq in Uq and
A7: for b being Point of TOP-REAL 2 st b in Uq holds |.b-aq.| < r/2 by Th30;
take Up,Uq;
thus Up is open & Uq is open & p in Up by A4;
thus not q in Up
proof
assume q in Up;
then
A8: |.q9-ap.| < r/2 by A5;
|.q9-ap.| = |.ap-q9.| by TOPRNS_1:27;
then |.p9-ap.|+|.ap-q9.| < r/2+r/2 by A8,A4,A5,XREAL_1:8;
hence contradiction by TOPRNS_1:34;
end;
thus q in Uq by A6;
assume
A9: p in Uq;
A10: |.q9-aq.| = |.aq-q9.| by TOPRNS_1:27;
|.q9-aq.| < r/2 by A6,A7;
then |.p9-aq.|+|.aq-q9.| < r/2+r/2 by A10,A9,A7,XREAL_1:8;
hence contradiction by TOPRNS_1:34;
end;
theorem
Niemytzki-plane is not normal
proof
reconsider C = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> as dense
Subset of Niemytzki-plane by Th36;
set T = Niemytzki-plane;
defpred P[object,object] means
ex D1 being set, U,V being open Subset of T st D1 = $1 & $2 = U /\ C & D1
c= U & y=0-line \ D1 c= V & U misses V;
A1: exp(2, omega) in exp(2, exp(2, omega)) by CARD_5:14;
card C c= card product <*RAT,RAT*> by CARD_1:11,XBOOLE_1:17;
then card C c= omega by Th8,CARD_4:6,TOPGEN_3:17;
then
A2: exp(2, card C) c= exp(2, omega) by CARD_2:93;
assume
A3: for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is
closed & W misses V ex P, Q being Subset of T st P is open & Q is open & W c= P
& V c= Q & P misses Q;
A4: for a being object st a in bool y=0-line ex b being object st P[a,b]
proof
let a be object;
assume a in bool y=0-line;
then reconsider aa = a as Subset of y=0-line;
reconsider a9 = y=0-line \ aa as Subset of y=0-line by
XBOOLE_1:36;
reconsider A = aa, B = a9 as closed Subset of T by Th42;
per cases;
suppose
A5: a = {};
take {};
take {},{}T,[#]T;
thus thesis by A5,Def3,Th19;
end;
suppose
A6: a = y=0-line;
take ([#]T)/\ C;
take aa,[#]T,{}T;
thus aa = a;
thus thesis by A6,Def3,Th19,XBOOLE_1:37;
end;
suppose
A7: a <> {} & a <> y=0-line;
aa`` = a9`;
then
A8: B <> {}y=0-line by A7;
A misses B by XBOOLE_1:79;
then consider P, Q being Subset of T such that
A9: P is open and
A10: Q is open and
A11: A c= P and
A12: B c= Q and
A13: P misses Q by A8,A3,A7;
take P /\ C;
thus thesis by A9,A10,A11,A12,A13;
end;
end;
consider G being Function such that
A14: dom G = bool y=0-line and
A15: for a being object st a in bool y=0-line holds P[a,G.a] from CLASSES1:
sch 1(A4);
G is one-to-one
proof
let x,y be object;
assume that
A16: x in dom G and
A17: y in dom G;
reconsider A = x, B = y as Subset of y=0-line by A16,A17,A14;
assume that
A18: G.x = G.y and
A19: x <> y;
consider z being object such that
A20: not (z in A iff z in B) by A19,TARSKI:2;
A21: z in A\B or z in B\A by A20,XBOOLE_0:def 5;
consider D1 being set,UB,VB being open Subset of T such that
A22: D1 = B and
A23: G.B = UB /\ C and
A24: D1 c= UB and
A25: y=0-line \ D1 c= VB and
A26: UB misses VB by A15;
consider D1 being set,UA,VA being open Subset of T such that
A27: D1 = A and
A28: G.A = UA /\ C and
A29: D1 c= UA and
A30: y=0-line \ D1 c= VA and
A31: UA misses VA by A15;
B\A = B/\A` by SUBSET_1:13;
then
A32: B\A c= UB /\ VA by A30,A24,XBOOLE_1:27,A22,A27;
A\B = A/\B` by SUBSET_1:13;
then A\B c= UA /\ VB by A29,A25,XBOOLE_1:27,A22,A27;
then C meets UA /\ VB or C meets UB /\ VA by A32,A21,TOPS_1:45;
then (ex z being object st z in C & z in UA /\ VB)
or ex z being object st z in
C & z in UB /\ VA by XBOOLE_0:3;
then consider z being set such that
A33: z in C and
A34: z in UA /\ VB or z in UB /\ VA;
z in UA & z in VB or z in UB & z in VA by A34,XBOOLE_0:def 4;
then z in UA & not z in UB or z in UB & not z in UA by A31,A26,XBOOLE_0:3;
then z in G.A & not z in G.B or z in G.B & not z in G.A by A28,A23,A33,
XBOOLE_0:def 4;
hence thesis by A18;
end;
then
A35: card dom G c= card rng G by CARD_1:10;
rng G c= bool C
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in rng G;
then consider b being object such that
A36: b in dom G and
A37: a = G.b by FUNCT_1:def 3;
P[b,aa] by A14,A15,A36,A37;
then aa c= C by XBOOLE_1:17;
hence thesis;
end;
then card rng G c= card bool C by CARD_1:11;
then card bool y=0-line c= card bool C by A35,A14;
then
A38: exp(2, continuum) c= card bool C by Th16,CARD_2:31;
card bool C = exp(2, card C) by CARD_2:31;
then exp(2, continuum) c= exp(2, omega) by A38,A2;
then exp(2, omega) in exp(2, omega) by A1,TOPGEN_3:29;
hence contradiction;
end;
begin :: Tychonoff spaces
definition
let T be TopSpace;
attr T is Tychonoff means
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;
coherence
proof
reconsider z = 0, j = 1, half = 1/2 as Element of I[01] by BORSUK_1:40
,XXREAL_1:1;
let T be TopSpace;
assume that
A1: 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};
reconsider A = [.z,half.[, B = ].half,j.] as Subset of I[01] by BORSUK_1:40
,XXREAL_1:35,36;
reconsider A,B as open Subset of I[01] by TOPALG_1:4,5;
let p be Point of T, P be Subset of T;
assume that
A2: P is closed and
A3: p in P`;
consider f being continuous Function of T, I[01] such that
A4: f.p = 0 and
A5: f.:P c= {1} by A2,A3,A1;
take W = f"A, V = f"B;
[#]I[01] <> {};
hence W is open & V is open by TOPS_2:43;
0 in A by XXREAL_1:3;
hence p in W by A3,A4,FUNCT_2:38;
A6: dom f = the carrier of T by FUNCT_2:def 1;
1 in B by XXREAL_1:2;
then {1} c= B by ZFMISC_1:31;
then f.:P c= B by A5;
hence P c= V by A6,FUNCT_1:93;
assume W meets V;
then consider x being object such that
A7: x in W and
A8: x in V by XBOOLE_0:3;
A9: f.x in A by A7,FUNCT_1:def 7;
then reconsider fx = f.x as Element of I[01];
A10: fx < half by A9,XXREAL_1:3;
f.x in B by A8,FUNCT_1:def 7;
hence thesis by A10,XXREAL_1:2;
end;
cluster T_4 -> Tychonoff for non empty TopSpace;
coherence
proof
the carrier of Closed-Interval-TSpace(-1,1) = [.-1,1.] by TOPMETR:18;
then reconsider j = 1, k = -1 as Point of Closed-Interval-TSpace(-1,1) by
XXREAL_1:1;
reconsider z = 0, o = 1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
let T be non empty TopSpace;
assume
A11: T is T_4;
let A be closed Subset of T, a be Point of T;
per cases;
suppose
A12: A is empty;
set f = T --> z;
A13: f.a = z;
f.:A = {} by A12;
hence thesis by A13,XBOOLE_1:2;
end;
suppose
A is non empty;
then reconsider aa = {a}, A9 = A as non empty closed Subset of T by A11,
URYSOHN1:19;
reconsider B = A9 \/ aa as closed Subset of T;
set h = (T|A9 --> j)+*(T|aa --> k);
A14: T|aa --> k = aa --> k by PRE_TOPC:8;
A15: (A9 --> 1).:A c= {1} by FUNCOP_1:81;
A16: a in aa by TARSKI:def 1;
then
A17: a in B by XBOOLE_0:def 3;
assume a in A`;
then
A18: not a in A by XBOOLE_0:def 5;
then A9 misses aa by ZFMISC_1:50;
then reconsider
h as continuous Function of T|B, Closed-Interval-TSpace(- 1,1
) by Th11;
consider g being continuous Function of T, Closed-Interval-TSpace(-1,1)
such that
A19: g|B = h by A11,TIETZE:23;
consider p being Function of I[01], Closed-Interval-TSpace(-1,1) such
that
A20: p is being_homeomorphism and
for r being Real st r in [.0,1.] holds p.r=2*r-1 and
A21: p.0=-1 and
A22: p.1=1 by JGRAPH_5:39;
reconsider p9 = p/" as continuous Function of Closed-Interval-TSpace(-1,
1), I[01] by A20,TOPS_2:def 5;
A23: p9 = p qua Function" by A20,TOPS_2:def 4;
then
A24: p9.k = z by A20,A21,FUNCT_2:26;
A25: the carrier of T|aa = aa by PRE_TOPC:8;
then dom (T|aa --> k) = aa;
then
A26: h.a = (T|aa --> k).a by A16,FUNCT_4:13
.= -1 by A25,A16,FUNCOP_1:7;
reconsider f = p9*g as continuous Function of T, I[01];
A27: f.:A = p9.:(g.:A) by RELAT_1:126
.= p9.:(h.:A) by A19,RELAT_1:129,XBOOLE_1:7;
T|A9 --> j = A9 --> 1 by PRE_TOPC:8;
then h.:A c= {1} by A14,A15,A18,BOOLMARK:3,ZFMISC_1:50;
then
A28: f.:A c= Im(p9,1) by A27,RELAT_1:123;
take f;
thus f.a = p9.(g.a) by FUNCT_2:15
.= 0 by A26,A17,A19,A24,FUNCT_1:49;
p9.j = o by A20,A22,A23,FUNCT_2:26;
hence thesis by A28,SETWISEO:8;
end;
end;
end;
theorem
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}
proof
let X be T_1 TopSpace;
assume
A1: X is Tychonoff;
let B be prebasis of X;
let x be Point of X;
let V be Subset of X;
assume that
A2: x in V and
A3: V in B;
A4: V`` = V;
V is open by A3,TOPS_2:def 1;
hence thesis by A4,A1,A2;
end;
theorem Th49:
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
proof
let X be TopSpace;
let R be non empty SubSpace of R^1;
let f,g be continuous Function of X,R;
let A be Subset of X;
assume
A1: for x being Point of X holds x in A iff f.x <= g.x;
now
thus the topology of X is Basis of X by CANTOR_1:2;
let p be Point of X;
set r = f.p-g.p;
reconsider U1 = ].f.p-r/2,f.p+r/2.[, V1 = ].g.p-r/2,g.p+r/2.[ as open
Subset of R^1 by JORDAN6:35,TOPMETR:17;
reconsider U = U1/\[#]R, V = V1/\[#]R as open Subset of R by TOPS_2:24;
A2: g"V is open by TOPS_2:43;
assume
A3: p in A`;
then
A4: f.p in [#]R by FUNCT_2:5;
not p in A by A3,XBOOLE_0:def 5;
then f.p > g.p by A1;
then reconsider r as positive Real by XREAL_1:50;
A5: f.p < f.p+r/2 by XREAL_1:29;
take B = f"U /\ g"V;
A6: g.p < g.p+r/2 by XREAL_1:29;
A7: g.p in [#]R by A3,FUNCT_2:5;
g.p-r/2 < g.p by XREAL_1:44;
then g.p in V1 by A6,XXREAL_1:4;
then g.p in V by A7,XBOOLE_0:def 4;
then
A8: p in g"V by A3,FUNCT_2:38;
f.p-r/2 < f.p by XREAL_1:44;
then f.p in U1 by A5,XXREAL_1:4;
then f.p in U by A4,XBOOLE_0:def 4;
then
A9: p in f"U by A3,FUNCT_2:38;
f"U is open by TOPS_2:43;
hence B in the topology of X & p in B by A9,A8,A2,PRE_TOPC:def 2
,XBOOLE_0:def 4;
thus B c= A`
proof
let q be object;
reconsider qq=q as set by TARSKI:1;
assume
A10: q in B;
then q in g"V by XBOOLE_0:def 4;
then g.q in V by FUNCT_2:38;
then g.q in V1 by XBOOLE_0:def 4;
then
A11: g.qq < g.p+r/2 by XXREAL_1:4;
q in f"U by A10,XBOOLE_0:def 4;
then f.q in U by FUNCT_2:38;
then f.q in U1 by XBOOLE_0:def 4;
then f.qq > f.p-r/2 by XXREAL_1:4;
then g.qq < f.qq by A11,XXREAL_0:2;
then not q in A by A1;
hence thesis by A10,SUBSET_1:29;
end;
end;
then A` is open by YELLOW_9:31;
hence thesis;
end;
theorem Th50:
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)
proof
let X be TopSpace;
let R be non empty SubSpace of R^1;
let f,g be continuous Function of X,R;
defpred A[set] means f.$1 >= g.$1;
consider A being Subset of X such that
A1: for a being set holds a in A iff a in the carrier of X & A[a] from
SUBSET_1:sch 1;
defpred B[set] means f.$1 <= g.$1;
consider B being Subset of X such that
A2: for a being set holds a in B iff a in the carrier of X & B[a] from
SUBSET_1:sch 1;
per cases;
suppose
A3: X is empty;
set h = the continuous Function of X,R;
take h;
let x be Point of X;
A4: f.x = 0 by A3;
A5: g.x = 0 by A3;
thus thesis by A3,A4,A5;
end;
suppose
A6: X is non empty & A is empty;
take g;
let x be Point of X;
f.x < g.x by A6,A1;
hence thesis by XXREAL_0:def 10;
end;
suppose
A7: X is non empty & B is empty;
take f;
let x be Point of X;
g.x < f.x by A7,A2;
hence thesis by XXREAL_0:def 10;
end;
suppose
A8: X is not empty & A is not empty & B is not empty;
then reconsider X9 = X as non empty TopSpace;
for x being Point of X9 holds (x in A iff f.x >= g.x) & (x in B iff f
.x <= g.x) by A1,A2;
then reconsider A9 = A, B9 = B as non empty closed Subset of X9 by A8,Th49;
reconsider ff = f, gg = g as continuous Function of X9, R;
A9: the carrier of X9|A9 = [#](X9|A9) .= A9 by PRE_TOPC:def 5;
A10: dom ff = the carrier of X9 by FUNCT_2:def 1;
then dom (ff|A9) = A9 by RELAT_1:62;
then reconsider f9 = ff|A9 as continuous Function of X9|A9, R by A9,
FUNCT_2:def 1,RELSET_1:18,TOPMETR:7;
A11: the carrier of X9|B9 = [#](X9|B9) .= B9 by PRE_TOPC:def 5;
A12: dom gg = the carrier of X9 by FUNCT_2:def 1;
then dom (gg|B9) = B9 by RELAT_1:62;
then reconsider g9 = gg|B9 as continuous Function of X9|B9, R by A11,
FUNCT_2:def 1,RELSET_1:18,TOPMETR:7;
A13: dom g9 = B by A12,RELAT_1:62;
A14: A9 \/ B9 = the carrier of X9
proof
thus A9 \/ B9 c= the carrier of X9;
let a be object;
reconsider aa=a as set by TARSKI:1;
f.aa >= g.aa or f.aa <= g.aa;
then a in the carrier of X implies a in A9 or a in B9 by A1,A2;
hence thesis by XBOOLE_0:def 3;
end;
then
A15: X9|(A9 \/ B9) = X9 | [#]X9 .= the TopStruct of X by TSEP_1:93;
A16: the TopStruct of R = the TopStruct of R;
A17: dom f9 = A by A10,RELAT_1:62;
A18: f9 tolerates g9
proof
let a be object;
assume
A19: a in dom f9 /\ dom g9;
then
A20: a in A by A17,XBOOLE_0:def 4;
then
A21: f.a >= g.a by A1;
A22: a in B by A19,A13,XBOOLE_0:def 4;
then f.a <= g.a by A2;
then f.a = g.a by A21,XXREAL_0:1;
hence f9.a = g.a by A20,FUNCT_1:49
.= g9.a by A22,FUNCT_1:49;
end;
then f9+*g9 is continuous Function of X9|(A9 \/ B9), R by Th10;
then reconsider h = f9+*g9 as continuous Function of X,R by A16,A15,
YELLOW12:36;
take h;
let x be Point of X;
x in A9 or x in B9 by A14,XBOOLE_0:def 3;
then
x in A9 & f.x >= g.x & h.x = f9.x & f.x = f9.x or x in B9 & f.x <= g.
x & h.x = g9.x & g.x = g9.x by A1,A17,A13,A18,FUNCT_1:49,FUNCT_4:13,15;
hence thesis by XXREAL_0:def 10;
end;
end;
theorem Th51:
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
proof
let X be non empty TopSpace;
let R be non empty SubSpace of R^1;
let A be finite non empty set;
let F be ManySortedFunction of A;
defpred P[set] means $1 is empty or 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|$1)).x) holds f.x = max S;
A1: P[{}];
A2: dom F = A by PARTFUN1:def 2;
assume
A3: for a being set st a in A holds F.a is continuous Function of X,R;
rng F c= Funcs(the carrier of X,the carrier of R)
proof
let a be object;
assume a in rng F;
then ex b being object st b in dom F & a = F.b by FUNCT_1:def 3;
then a is Function of X,R by A3;
hence thesis by FUNCT_2:8;
end;
then
A4: F in Funcs(A,Funcs(the carrier of X,the carrier of R)) by A2,FUNCT_2:def 2;
A5: now
let x,B be set;
assume
A6: x in A;
then reconsider fx = F.x as continuous Function of X,R by A3;
assume
A7: B c= A;
assume
A8: P[B];
per cases;
suppose
A9: B = {};
thus P[B \/ {x}]
proof
assume B \/ {x} is not empty;
take fx;
let a be Point of X, S be finite non empty Subset of REAL;
A10: dom fx = the carrier of X by FUNCT_2:def 1;
F|{x} = x .--> (F.x) by A2,A6,FUNCT_7:6;
then (commute (F|{x})).a = x .--> (fx.a) by A10,Th3;
then
A11: rng ((commute (F|{x})).a) = {fx.a} by FUNCOP_1:8;
assume S = rng ((commute (F|(B \/ {x}))).a);
hence thesis by A11,A9,XXREAL_2:11;
end;
end;
suppose
A12: B <> {};
then reconsider B9 = B as non empty set;
consider f being continuous Function of X,R such that
A13: for x being Point of X, S being finite non empty Subset of REAL
st S = rng ((commute (F|B9)).x) holds f.x = max S by A8;
consider h being continuous Function of X,R such that
A14: for x being Point of X holds h.x = max(f.x,fx.x) by Th50;
thus P[B \/ {x}]
proof
F is Function of A, Funcs(the carrier of X,the carrier of R) by A4,
FUNCT_2:66;
then
F|B is Function of B, Funcs(the carrier of X,the carrier of R) by A7,
FUNCT_2:32;
then F|B in Funcs(B, Funcs(the carrier of X,the carrier of R)) by
FUNCT_2:8;
then commute (F|B) in Funcs(the carrier of X, Funcs(B, the carrier of
R)) by A12,FUNCT_6:55;
then reconsider
cFB = commute (F|B) as Function of the carrier of X, Funcs(
B, the carrier of R) by FUNCT_2:66;
assume B \/ {x} is not empty;
take h;
let a be Point of X, S be finite non empty Subset of REAL;
reconsider cFBa = cFB.a as Function of B9, the carrier of R;
A15: dom fx = the carrier of X by FUNCT_2:def 1;
F|(B \/ {x}) = (F|B) \/ (F|{x}) by RELAT_1:78;
then
A16: (commute (F|(B\/{x}))).a = cFB.a \/ (commute (F|{x})).a by Th7;
assume S = rng ((commute (F|(B \/ {x}))).a);
then
A17: S = rng cFBa \/ rng ((commute (F|{x})).a) by A16,RELAT_1:12;
then rng cFBa c= S by XBOOLE_1:7;
then reconsider S1 = rng cFBa as non empty finite Subset of REAL by
XBOOLE_1:1;
F|{x} = x .--> (F.x) by A2,A6,FUNCT_7:6;
then (commute (F|{x})).a = x .--> (fx.a) by A15,Th3;
then
A18: S = S1 \/ {fx.a} by A17,FUNCOP_1:8;
f.a = max S1 by A13;
then max S = max(f.a, max {fx.a}) by A18,XXREAL_2:10
.= max(f.a, fx.a) by XXREAL_2:11;
hence thesis by A14;
end;
end;
end;
A19: A is finite;
P[A] from FINSET_1:sch 2(A19,A1,A5);
hence thesis;
end;
theorem Th52:
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
proof
reconsider z = 0 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
let X be T_1 non empty TopSpace;
let BB be prebasis of X such that
A1: for x being Point of X for V being Subset of X st x in V & V in BB
ex f being continuous Function of X, I[01] st f.x = 0 & f.:V` c= {1};
let A be closed Subset of X;
let a be Point of X;
A2: FinMeetCl BB is Basis of X by YELLOW_9:23;
assume a in A`;
then consider B being Subset of X such that
A3: B in FinMeetCl BB and
A4: a in B and
A5: B c= A` by A2,YELLOW_9:31;
consider F being Subset-Family of X such that
A6: F c= BB and
A7: F is finite and
A8: B = Intersect F by A3,CANTOR_1:def 3;
per cases;
suppose
F is empty;
then B = the carrier of X by A8,SETFAM_1:def 9;
then A`` = {}X by A5,XBOOLE_1:37;
then
A9: (X-->z).:A = {};
(X-->z).a = z;
hence thesis by A9,XBOOLE_1:2;
end;
suppose
F is non empty;
then reconsider F as finite non empty Subset-Family of X by A7;
defpred P[object,object] means
ex S being Subset of X, f being continuous
Function of X, I[01] st S = $1 & f = $2 & f.a = 0 & f.:S` c= {1};
reconsider Sa = {In(0,REAL)}
as finite non empty Subset of REAL;
set z = the Element of F;
set R = I[01];
A10: for x being object st x in F ex y being object st P[x,y]
proof
let x be object;
assume
A11: x in F;
then reconsider S = x as Subset of X;
a in S by A4,A8,A11,SETFAM_1:43;
then consider f being continuous Function of X, I[01] such that
A12: f.a = 0 and
A13: f.:S` c= {1} by A6,A11,A1;
take f;
thus thesis by A12,A13;
end;
consider G being Function such that
A14: dom G = F & for x being object st x in F holds P[x,G.x] from
CLASSES1:sch 1(A10);
G is Function-yielding
proof
let x be object;
assume x in dom G;
then P[x,G.x] by A14;
hence thesis;
end;
then reconsider G as ManySortedFunction of F by A14,PARTFUN1:def 2
,RELAT_1:def 18;
rng G c= Funcs(the carrier of X,the carrier of R)
proof
let u be object;
assume u in rng G;
then consider v being object such that
A15: v in dom G and
A16: u = G.v by FUNCT_1:def 3;
P[v,u] by A14,A15,A16;
hence thesis by FUNCT_2:8;
end;
then G is Function of F, Funcs(the carrier of X,the carrier of R) by A14,
FUNCT_2:2;
then
A17: G in Funcs(F, Funcs(the carrier of X,the carrier of R)) by FUNCT_2:8;
then commute G in Funcs(the carrier of X, Funcs(F, the carrier of R)) by
FUNCT_6:55;
then reconsider
cG = commute G as Function of the carrier of X, Funcs(F, the
carrier of R) by FUNCT_2:66;
now
let a be set;
assume a in F;
then P[a,G.a] by A14;
hence G.a is continuous Function of X, I[01];
end;
then consider f being continuous Function of X, I[01] such that
A18: for x being Point of X, S being finite non empty Subset of REAL
st S = rng ((commute G).x) holds f.x = max S by Th51;
take f;
reconsider cGa = cG.a as Function of F, the carrier of R;
A19: dom cGa = F by FUNCT_2:def 1;
Sa = rng ((commute G).a)
proof
thus Sa c= rng ((commute G).a)
proof
let x be object;
assume x in Sa;
then
A20: x = 0 by TARSKI:def 1;
P[z,G.z] by A14;
then x = (commute G).a.z by A20,A17,FUNCT_6:56;
hence thesis by A19,FUNCT_1:def 3;
end;
let x be object;
assume x in rng ((commute G).a);
then consider z being object such that
A21: z in dom cGa and
A22: x = cGa.z by FUNCT_1:def 3;
P[z,G.z] by A14,A21;
then x = 0 by A17,A21,A22,FUNCT_6:56;
hence thesis by TARSKI:def 1;
end;
hence f.a = max Sa by A18
.= 0 by XXREAL_2:11;
let z be object;
assume z in f.:A;
then consider x being object such that
A23: x in dom f and
A24: x in A and
A25: z = f.x by FUNCT_1:def 6;
reconsider x as Element of X by A23;
not x in B by A5,A24,XBOOLE_0:def 5;
then consider w such that
A26: w in F and
A27: not x in w by A8,SETFAM_1:43;
reconsider cGx = cG.x as Function of F, the carrier of R;
reconsider S = rng cGx as finite non empty Subset of REAL by BORSUK_1:40
,XBOOLE_1:1;
A28: f.x = max S by A18;
consider T being Subset of X, g being continuous Function of X, R such
that
A29: T = w and
A30: g = G.w and
g.a = 0 and
A31: g.:T` c= {1} by A14,A26;
x in T` by A27,A29,SUBSET_1:29;
then g.x in g.:T` by FUNCT_2:35;
then g.x = 1 by A31,TARSKI:def 1;
then
A32: cGx.w = 1 by A17,A26,A30,FUNCT_6:56;
w in dom cGx by A17,A26,A30,FUNCT_6:56;
then
A33: 1 in S by A32,FUNCT_1:def 3;
for r being ExtReal st r in S holds r <= 1 by BORSUK_1:40,XXREAL_1:1;
then max S = 1 by A33,XXREAL_2:def 8;
hence thesis by A25,A28,TARSKI:def 1;
end;
end;
theorem Th53:
Sorgenfrey-line is T_1
proof
set T = Sorgenfrey-line;
consider B being Subset-Family of REAL such that
A1: the topology of Sorgenfrey-line = UniCl B and
A2: B = {[.x,q.[ where x,q is Real: x < q & q is rational}
by TOPGEN_3:def 2;
let x,y be Point of T;
reconsider a = x, b = y as Element of REAL by TOPGEN_3:def 2;
A3: B c= the topology of T by A1,CANTOR_1:1;
assume
A4: x <> y;
per cases by A4,XXREAL_0:1;
suppose
A5: a < b;
b < b+1 by XREAL_1:29;
then consider q being Rational such that
A6: b < q and
q < b+1 by RAT_1:7;
[.b,q.[ in B by A2,A6;
then
A7: [.b,q.[ in the topology of T by A3;
consider w being Rational such that
A8: a < w and
A9: w < b by A5,RAT_1:7;
[.a,w.[ in B by A2,A8;
then [.a,w.[ in the topology of T by A3;
then reconsider U = [.a,w.[, V = [.b,q.[ as open Subset of T by A7,
PRE_TOPC:def 2;
take U,V;
thus U is open & V is open;
thus thesis by A5,A8,A9,A6,XXREAL_1:3;
end;
suppose
A10: a > b;
a < a+1 by XREAL_1:29;
then consider q being Rational such that
A11: a < q and
q < a+1 by RAT_1:7;
[.a,q.[ in B by A2,A11;
then
A12: [.a,q.[ in the topology of T by A3;
consider w being Rational such that
A13: b < w and
A14: w < a by A10,RAT_1:7;
[.b,w.[ in B by A2,A13;
then [.b,w.[ in the topology of T by A3;
then reconsider V = [.b,w.[, U = [.a,q.[ as open Subset of T by A12,
PRE_TOPC:def 2;
take U,V;
thus U is open & V is open;
thus thesis by A10,A13,A14,A11,XXREAL_1:3;
end;
end;
theorem Th54:
for x being Real holds left_open_halfline x is closed
Subset of Sorgenfrey-line
proof
let x be Real;
set T = Sorgenfrey-line;
reconsider A = right_closed_halfline x as open Subset of T by TOPGEN_3:15;
the carrier of T = REAL by TOPGEN_3:def 2;
then left_open_halfline x = A` by XXREAL_1:224,294;
hence thesis;
end;
theorem
for x being Real holds left_closed_halfline x is closed Subset
of Sorgenfrey-line
proof
let x be Real;
set T = Sorgenfrey-line;
reconsider A = right_open_halfline x as open Subset of T by TOPGEN_3:14;
the carrier of T = REAL by TOPGEN_3:def 2;
then (left_closed_halfline x)`` = A` by XXREAL_1:224,288;
hence thesis;
end;
theorem Th56:
for x being Real holds right_closed_halfline x is closed
Subset of Sorgenfrey-line
proof
let x be Real;
set T = Sorgenfrey-line;
reconsider A = left_open_halfline x as open Subset of T by TOPGEN_3:13;
the carrier of T = REAL by TOPGEN_3:def 2;
then (right_closed_halfline x)`` = A` by XXREAL_1:224,294;
hence thesis;
end;
theorem Th57:
for x,y being Real holds [.x,y.[ is closed Subset of Sorgenfrey-line
proof
let x,y be Real;
set T = Sorgenfrey-line;
reconsider A = right_closed_halfline x, B = left_open_halfline y as closed
Subset of T by Th54,Th56;
A1: the carrier of T = REAL by TOPGEN_3:def 2;
[.x,y.[ = [.x,y.[``
.= (left_open_halfline(x) \/ right_closed_halfline(y))` by XXREAL_1:382
.= (left_open_halfline x)` /\ (right_closed_halfline y)` by XBOOLE_1:53
.= A`` /\ (right_closed_halfline y)` by A1,XXREAL_1:224,294
.= A /\ B by XXREAL_1:224,294;
hence thesis;
end;
::<DESC name="1.4.4. Przyk/lad funkcji ci/ag/lej ze strza/lce w [0,1]" monograph="topology"/>
theorem Th58:
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)
proof
reconsider 00 = 0, 01 = 1 as Element of I[01] by BORSUK_1:40,XXREAL_1:1;
let x be Real;
set X = Sorgenfrey-line;
let w be Rational;
reconsider V = [.x,w.[ as open closed Subset of X by Th57,TOPGEN_3:11;
defpred P[object] means $1 in [.x,w.[;
deffunc 00(object) = 0;
deffunc 01(object) = 1;
:: funkcja charakterystyczna zbioru [.x,w.[ !!! ???
reconsider f1 = (X|V) --> 00 as continuous Function of X|V, I[01];
reconsider f2 = (X|V`) --> 01 as continuous Function of X|V`, I[01];
A1: for a being object st a in the carrier of X holds (P[a] implies 00(a) in
the carrier of I[01]) & (not P[a] implies 01(a) in the carrier of I[01]) by
BORSUK_1:40,XXREAL_1:1;
consider f being Function of X, I[01] such that
A2: for a being object st a in the carrier of X holds (P[a] implies f.a =
00(a)) & (not P[a] implies f.a = 01(a)) from FUNCT_2:sch 5(A1);
the carrier of X|V = V by PRE_TOPC:8;
then
A4: dom f1 = V;
A5: the carrier of X|V` = V` by PRE_TOPC:8;
then
A6: dom f2 = V`;
A7: dom f = [#]X by FUNCT_2:def 1;
A8: now
let u be object;
assume u in dom f1 \/ dom f2;
then reconsider x = u as Point of X by A7,A4,A6,PRE_TOPC:2;
hereby
assume
A9: u in dom f2;
then
A10: (V`-->1).u = 1 by A5,FUNCOP_1:7;
not x in V by A9,A5,XBOOLE_0:def 5;
hence f.u = f2.u by A10,A5,A2;
end;
assume not u in dom f2;
then
x in V by A6,SUBSET_1:29;
hence f.u = 0 by A2
.= f1.u;
end;
V \/ V` = [#]X by PRE_TOPC:2;
then f = f1+*f2 by A8,A7,A4,A6,FUNCT_4:def 1;
then reconsider f as continuous Function of Sorgenfrey-line, I[01] by Th12;
take f;
let a be Point of Sorgenfrey-line;
thus thesis by A2;
end;
theorem
Sorgenfrey-line is Tychonoff
proof
set X = Sorgenfrey-line;
A1: the carrier of X = REAL by TOPGEN_3:def 2;
consider B being Subset-Family of REAL such that
A2: the topology of X = UniCl B and
A3: B = {[.x,q.[ where x,q is Real: x < q & q is rational}
by TOPGEN_3:def 2;
B c= UniCl B by CANTOR_1:1;
then B is Basis of X by A1,A2,CANTOR_1:def 2,TOPS_2:64;
then reconsider B as prebasis of X by YELLOW_9:27;
now
let x be Point of X;
let V be Subset of X;
assume that
A4: x in V and
A5: V in B;
consider a,q being Real such that
A6: V = [.a,q.[ and
a < q and
A7: q is rational by A5,A3;
consider f being continuous Function of X, I[01] such that
A8: for b being Point of Sorgenfrey-line holds (b in [.a,q.[ implies
f.b = 0) & (not b in [.a,q.[ implies f.b = 1) by A7,Th58;
take f;
thus f.x = 0 by A4,A6,A8;
thus f.:V` c= {1}
proof
let u be object;
assume u in f.:V`;
then consider b being Point of X such that
A9: b in V` and
A10: u = f.b by FUNCT_2:65;
not b in [.a,q.[ by A6,A9,XBOOLE_0:def 5;
then u = 1 by A8,A10;
hence thesis by TARSKI:def 1;
end;
end;
hence thesis by Th52,Th53;
end;
begin :: Niemytzki plane is Tychonoff space
::<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, r be positive Real;
func +(x,r) -> Function of Niemytzki-plane, I[01] means
:Def5:
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));
existence
proof
deffunc F3(Point of TOP-REAL 2) = |.|[x,0]|-$1.|^2/(2*r*$1`2);
deffunc F2(Point of TOP-REAL 2) = 1;
deffunc F1(Point of TOP-REAL 2) = 0;
defpred Q[set] means not $1 in Ball(|[x,r]|, r);
defpred P[set] means $1 = |[x,0]|;
A1: for a being Point of TOP-REAL 2 st a in the carrier of Niemytzki-plane
holds (P[a] implies F1(a) in the carrier of I[01]) & (not P[a] & Q[a] implies
F2(a) in the carrier of I[01]) & (not P[a] & not Q[a] implies F3(a) in the
carrier of I[01])
proof
let a be Point of TOP-REAL 2;
assume a in the carrier of Niemytzki-plane;
thus P[a] implies F1(a) in the carrier of I[01] by BORSUK_1:40,XXREAL_1:1
;
thus not P[a] & Q[a] implies F2(a) in the carrier of I[01] by BORSUK_1:40
,XXREAL_1:1;
assume not P[a];
A2: a = |[a`1,a`2]| by EUCLID:53;
assume not Q[a];
then |.a-|[x,r]|.| < r by TOPREAL9:7;
then |.|[a`1-x,a`2-r]|.| < r by A2,EUCLID:62;
then
A3: |.|[a`1-x,a`2-r]|.|^2 < r^2 by SQUARE_1:16;
A4: |[a`1-x,a`2-r]|`2 = a`2-r by EUCLID:52;
|[a`1-x,a`2-r]|`1 = a`1-x by EUCLID:52;
then (a`1-x)^2+(a`2-r)^2 < r^2 by A4,A3,JGRAPH_1:29;
then (a`1-x)^2+(a`2^2-2*a`2*r)+r^2 < 0+r^2;
then (a`1-x)^2+a`2^2-2*a`2*r < 0 by XREAL_1:6;
then
A5: (a`1-x)^2+(a`2-0)^2 < 2*r*a`2 by XREAL_1:48;
A6: |[a`1-x,a`2]|`2 = a`2 by EUCLID:52;
|[a`1-x,a`2]|`1 = a`1-x by EUCLID:52;
then
A7: |.|[a`1-x,a`2-0]|.|^2 < 2*r*a`2 by A6,A5,JGRAPH_1:29;
then |.a-|[x,0]|.|^2 < 2*r*a`2 by A2,EUCLID:62;
then |.|[x,0]|-a.|^2 < 2*r*a`2 by TOPRNS_1:27;
then F3(a) <= 1 by XREAL_1:183;
hence thesis by A7,BORSUK_1:40,XXREAL_1:1;
end;
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then
A8: the carrier of Niemytzki-plane c= the carrier of TOP-REAL 2;
consider f being Function of Niemytzki-plane, I[01] such that
A9: for a being Point of TOP-REAL 2 st a in the carrier of
Niemytzki-plane 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)) from SCH2(A8,A1);
take f;
A10: the carrier of Niemytzki-plane = y>=0-plane by Def3;
then |[x,0]| in the carrier of Niemytzki-plane;
hence f.(|[x,0]|) = 0 by A9;
let a be Real, b be non negative Real;
A11: |[a,b]| in the carrier of Niemytzki-plane by A10;
hereby
assume a <> x or b <> 0;
then not P[ |[a,b]| ] by SPPOL_2:1;
hence not |[a,b]| in Ball(|[x,r]|,r) implies f.(|[a,b]|) = 1 by A9,A11;
end;
assume
A12: |[a,b]| in Ball(|[x,r]|,r);
A13: |[x,0]| in y=0-line;
A14: |[a,b]|`2 = b by EUCLID:52;
Ball(|[x,r]|,r) misses y=0-line by Th21;
then not P[ |[a,b]| ] by A13,A12,XBOOLE_0:3;
hence thesis by A14,A9,A11,A12;
end;
uniqueness
proof
let f,g be Function of Niemytzki-plane, I[01] such that
A15: f.(|[x,0]|) = 0 and
A16: for a being Real, b being non negative Real holds
((a <> x or b <> 0) & not |[a,b]| in Ball(|[x,r]|,r) implies f.(|[a,b]|) = 1) &
(|[a,b]| in Ball(|[x,r]|,r) implies f.(|[a,b]|) = |.|[x,0]|-|[a,b]|.|^2/(2*r*b)
) and
A17: g.(|[x,0]|) = 0 and
A18: for a being Real, b being non negative Real holds
((a <> x or b <> 0) & not |[a,b]| in Ball(|[x,r]|,r) implies g.(|[a,b]|) = 1) &
(|[a,b]| in Ball(|[x,r]|,r) implies g.(|[a,b]|) = |.|[x,0]|-|[a,b]|.|^2/(2*r*b)
);
A19: the carrier of Niemytzki-plane = y>=0-plane by Def3;
now
let p be Point of Niemytzki-plane;
p in y>=0-plane by A19;
then reconsider q = p as Point of TOP-REAL 2;
A20: p = |[q`1,q`2]| by EUCLID:53;
then reconsider q2 = q`2 as non negative Real by A19,Th18;
per cases by EUCLID:53;
suppose
q`1 = x & q2 = 0;
hence f.p = g.p by A15,A17,A20;
end;
suppose
A21: (q`1 <> x or q2 <> 0) & not |[q`1,q2]| in Ball(|[x,r]|,r);
then f.p = 1 by A16,A20;
hence f.p = g.p by A18,A20,A21;
end;
suppose
A22: p in Ball(|[x,r]|,r);
then f.p = |.|[x,0]|-q.|^2/(2*r*q2) by A16,A20;
hence f.p = g.p by A18,A20,A22;
end;
end;
hence thesis;
end;
end;
theorem Th60:
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]|
proof
let p be Point of TOP-REAL 2;
assume
A1: p`2 >= 0;
set p1 = p`1, p2 = p`2;
let x be Real;
let r be positive Real;
assume
A2: +(x,r).p = 0;
A3: p = |[p1,p2]| by EUCLID:53;
assume
A4: p <> |[x,0]|;
then p1 <> x or p2 <> 0 by EUCLID:53;
then
A5: |[p1,p2]| in Ball(|[x,r]|,r) by A1,A2,A3,Def5;
Ball(|[x,r]|,r) misses y=0-line by Th21;
then not |[p1,p2]| in y=0-line by A5,XBOOLE_0:3;
then p2 <> 0;
then reconsider p2 as positive Real by A1;
0/(2*r*p2) = |.|[x,0]|-|[p1,p2]|.|^2/(2*r*p2) by A2,A3,A5,Def5;
then 0 = |.|[x,0]|-p.| by A3;
hence contradiction by A4,TOPRNS_1:28;
end;
theorem Th61:
for x,y being Real, r being positive Real st x
<> y holds +(x,r).(|[y,0]|) = 1
proof
let x,y be Real;
let r be positive Real;
A1: |.x-y.| = x-y or |.x-y.| = - (x-y) by ABSVALUE:1;
A2: |[x-y,r]|`2 = r by EUCLID:52;
|[x-y,r]|`1 = x-y by EUCLID:52;
then
A3: |.|[x-y,r]|.|^2 = r^2+(x-y)^2 by A2,JGRAPH_1:29;
assume
A4: x <> y;
then x-y <> 0;
then
A5: |.x-y.| > 0 by COMPLEX1:47;
then |.x-y.|^2 <> 0;
then |.|[x-y,r]|.|^2 > r^2 by A1,A5,A3,XREAL_1:29;
then |.|[x-y,r-0]|.| > r by SQUARE_1:15;
then |.|[x,r]|-|[y,0]|.| > r by EUCLID:62;
then |.|[y,0]|-|[x,r]|.| > r by TOPRNS_1:27;
then not |[y,0]| in Ball(|[x,r]|,r) by TOPREAL9:7;
hence thesis by A4,Def5;
end;
theorem Th62:
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
proof
let p be Point of TOP-REAL 2;
set p1 = p`1, p2 = p`2;
let x be Real;
let a,r be positive Real;
assume
A1: a <= 1;
A2: |[p1-x,p2-r*a]|`1 = p1-x by EUCLID:52;
A3: |[p1-x,p2-r*a]|`2 = p2-r*a by EUCLID:52;
assume that
A4: |.p-|[x,r*a]|.| = r*a and
A5: p`2 <> 0;
A6: p = |[p`1,p`2]| by EUCLID:53;
then |.|[p1-x,p2-r*a]|.|^2 = (r*a)^2 by A4,EUCLID:62;
then
A7: (p1-x)^2+(p2-r*a)^2 = (r*a)^2 by A2,A3,JGRAPH_1:29;
then
A8: (p1-x)^2+p2^2 = 2*p2*r*a;
(p1-x)^2 >= 0 by XREAL_1:63;
then reconsider p2 as positive Real by A5,A8;
A9: |[p1-x,p2-0]|`1 = p1-x by EUCLID:52;
A10: |[p1-x,p2]|`2 = p2 by EUCLID:52;
per cases by A1,XXREAL_0:1;
suppose
a < 1;
then r*a < r by XREAL_1:157;
then reconsider s = r-r*a as positive Real by XREAL_1:50;
|.p-|[x,r]|.|^2 = |.|[p1-x,p2-r]|.|^2 by A6,EUCLID:62
.= (p1-x)^2+(p2-r)^2 by Th9
.= (p1-x)^2+(p2-a*r)^2+((r-a*r)^2+2*(r-a*r)*(a*r-p2))
.= |.|[p1-x,p2-a*r]|.|^2+((r-a*r)^2+2*(r-a*r)*(a*r-p2)) by Th9
.= (a*r)^2+(r*r-r*p2+r*a*r-r*p2-(a*r*r-a*r*p2+(a*r)^2-a*r*p2)) by A6,A4,
EUCLID:62
.= r^2-(1+1)*p2*s;
then |.p-|[x,r]|.|^2 < r^2 by XREAL_1:44;
then |.p-|[x,r]|.| < r by SQUARE_1:15;
then p in Ball(|[x,r]|,r) by TOPREAL9:7;
then +(x,r).p = |.|[x,0]|-p.|^2/(2*r*p2) by A6,Def5
.= |.p-|[x,0]|.|^2/(2*r*p2) by TOPRNS_1:27
.= |.|[p1-x,p2-0]|.|^2/(2*r*p2) by A6,EUCLID:62
.= ((p1-x)^2+p2^2)/(2*r*p2) by A9,A10,JGRAPH_1:29;
then
A11: +(x,r).p = (2*p2*r*a)/(2*r*p2) by A7;
a*((2*p2*r)/(2*r*p2)) = a*1 by XCMPLX_1:60;
hence thesis by A11,XCMPLX_1:74;
end;
suppose
A12: a = 1;
A13: p2 is non negative;
not p in Ball(|[x,r]|,r) by A12,A4,TOPREAL9:7;
hence thesis by A13,A6,A12,Def5;
end;
end;
theorem Th63:
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
proof
let p be Point of TOP-REAL 2;
set p1 = p`1, p2 = p`2;
let x,a be Real;
let r be positive Real;
assume that
A1: a <= 1;
A2: |[p1-x,p2-r*a]|`2 = p2-r*a by EUCLID:52;
A3: p = |[p`1,p`2]| by EUCLID:53;
then
A4: p2 = 0 implies p in y=0-line;
set r1 = r*a, r2 = r*1;
A5: |[p1-x,p2-r*a]|`1 = p1-x by EUCLID:52;
assume
A6: |.p-|[x,r*a]|.| < r*a;
then reconsider r1 as positive Real;
A7: p in Ball(|[x,r1]|,r1) by A6,TOPREAL9:7;
|.p-|[x,r*a]|.|^2 < (r*a)^2 by A6,SQUARE_1:16;
then |.|[p1-x,p2-r*a]|.|^2 < (r*a)^2 by A3,EUCLID:62;
then (p1-x)^2+(p2-r*a)^2 < (r*a)^2 by A5,A2,JGRAPH_1:29;
then (p1-x)^2+p2^2-2*p2*(r*a)+(r*a)^2 < (r*a)^2;
then (p1-x)^2+p2^2-2*p2*r*a < 0 by XREAL_1:31;
then
A8: (p1-x)^2+p2^2 < 2*p2*r*a by XREAL_1:48;
A9: Ball(|[x,r1]|,r1) misses y=0-line by Th21;
Ball(|[x,r1]|,r1) c= y>=0-plane by Th20;
then reconsider p2 as positive Real by A3,A7,Th18,A9,A4,XBOOLE_0:3;
A10: |[p1-x,p2-0]|`1 = p1-x by EUCLID:52;
A11: |[p1-x,p2]|`2 = p2 by EUCLID:52;
Ball(|[x,r1]|,r1) c= Ball(|[x,r2]|,r2) by A1,Th23,XREAL_1:64;
then +(x,r).p = |.|[x,0]|-p.|^2/(2*r*p2) by A3,A7,Def5
.= |.p-|[x,0]|.|^2/(2*r*p2) by TOPRNS_1:27
.= |.|[p1-x,p2-0]|.|^2/(2*r*p2) by A3,EUCLID:62
.= ((p1-x)^2+p2^2)/(2*r*p2) by A10,A11,JGRAPH_1:29;
then
A12: +(x,r).p < (2*p2*r*a)/(2*r*p2) by A8,XREAL_1:74;
a*((2*p2*r)/(2*r*p2)) = a*1 by XCMPLX_1:60;
hence thesis by A12,XCMPLX_1:74;
end;
theorem Th64:
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
proof
let p be Point of TOP-REAL 2 such that
A1: p`2 >= 0;
set p1 = p`1, p2 = p`2;
reconsider p2 as non negative Real by A1;
let x,a be Real;
let r be positive Real;
assume that
A2: 0 <= a and
A3: a < 1;
reconsider a9 = a as non negative Real by A2;
reconsider ra = r*a as Real;
assume
A4: |.p-|[x,r*a]|.| > r*a;
|.|[x,0]|-|[x,r*a]|.| = |.|[x,r*a]|-|[x,0]|.| by TOPRNS_1:27
.= |.|[x-x,ra-0]|.| by EUCLID:62
.= |.ra.| by TOPREAL6:23
.= r*a9 by ABSVALUE:def 1;
then
A5: p1 <> x or p2 <> 0 by A4,EUCLID:53;
A6: p = |[p`1,p`2]| by EUCLID:53;
then reconsider z = p as Element of Niemytzki-plane by A1,Lm1,Th18;
A7: +(x,r).z in the carrier of I[01];
per cases by A2;
suppose
A8: a = 0;
then p <> |[x,r*0]| by A4,TOPRNS_1:28;
then +(x,r).p <> 0 by A1,Th60;
hence thesis by A7,A8,BORSUK_1:40,XXREAL_1:1;
end;
suppose
+(x,r).p = 1;
hence thesis by A3;
end;
suppose
A9: a > 0 & +(x,r).z <> 1;
A10: |[p1-x,p2-0]|`1 = p1-x by EUCLID:52;
A11: |[p1-x,p2]|`2 = p2 by EUCLID:52;
p2 is non negative;
then
A12: p in Ball(|[x,r]|,r) by A6,A5,A9,Def5;
then
A13: +(x,r).p = |.|[x,0]|-p.|^2/(2*r*p2) by A6,Def5
.= |.p-|[x,0]|.|^2/(2*r*p2) by TOPRNS_1:27
.= |.|[p1-x,p2-0]|.|^2/(2*r*p2) by A6,EUCLID:62
.= ((p1-x)^2+p2^2)/(2*r*p2) by A10,A11,JGRAPH_1:29;
|.p-|[x,r*a]|.|^2 > (r*a)^2 by A2,A4,SQUARE_1:16;
then
A14: |.|[p1-x,p2-r*a]|.|^2 > (r*a)^2 by A6,EUCLID:62;
A15: |[p1-x,p2-r*a]|`2 = p2-r*a by EUCLID:52;
|[p1-x,p2-r*a]|`1 = p1-x by EUCLID:52;
then (p1-x)^2+(p2-r*a)^2 > (r*a)^2 by A14,A15,JGRAPH_1:29;
then (p1-x)^2+p2^2-2*p2*(r*a)+(r*a)^2 > (r*a)^2;
then (p1-x)^2+p2^2-2*p2*r*a > 0 by XREAL_1:32;
then
A16: (p1-x)^2+p2^2 > 2*p2*r*a by XREAL_1:47;
A17: p2 = 0 implies p in y=0-line by A6;
Ball(|[x,r]|,r) misses y=0-line by Th21;
then reconsider p2 as positive Real by A12,A17,XBOOLE_0:3;
A18: a*((2*p2*r)/(2*r*p2)) = a*1 by XCMPLX_1:60;
+(x,r).p > (2*p2*r*a)/(2*r*p2) by A13,A16,XREAL_1:74;
hence thesis by A18,XCMPLX_1:74;
end;
end;
theorem Th65:
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.[
proof
let p be Point of TOP-REAL 2 such that
A1: p`2 >= 0;
let x,a,b be Real, r be positive Real;
A2: p = |[p`1,p`2]| by EUCLID:53;
A3: Ball(|[x,r]|,r) misses y=0-line by Th21;
A4: |[p`1-x,p`2]|`1 = p`1-x by EUCLID:52;
assume that
A5: 0 <= a and
A6: b <= 1 and
A7: +(x,r).p in ].a,b.[;
A8: +(x,r).p > a by A7,XXREAL_1:4;
A9: +(x,r).p < b by A7,XXREAL_1:4;
then
A10: p in Ball(|[x,r]|,r) or p`1 = x & p`2 = 0 & p <> |[x,0]| by A8,A1,A2,A5,A6
,Def5;
then
A11: +(x,r).p = |.|[x,0]|-p.|^2/(2*r*p`2) by A1,A2,Def5;
p`2 = 0 implies p in y=0-line by A2;
then reconsider p2 = p`2, b9 = b as positive Real by A3,A1,A5,A8,A7,A10,
EUCLID:53,XBOOLE_0:3,XXREAL_1:4;
A12: |[p`1-x,p2]|`2 = p2 by EUCLID:52;
A13: 2*r*p2 > 0;
then |.|[x,0]|-p.|^2 > (2*r*p`2)*a by A11,A8,XREAL_1:79;
then |.p-|[x,0]|.|^2 > (2*r*p`2)*a by TOPRNS_1:27;
then |.|[p`1-x,p`2-0]|.|^2 > (2*r*p`2)*a by A2,EUCLID:62;
then (p`1-x)^2+p2^2 > (2*r*p2)*a by A4,A12,JGRAPH_1:29;
then (p`1-x)^2+p2^2 - (2*r*p2)*a > 0 by XREAL_1:50;
then (p`1-x)^2+p2^2 - (2*r*p2)*a + (r*a)^2 > (r*a)^2 by XREAL_1:29;
then
A14: (p`1-x)^2+(p2 - r*a)^2 > (r*a)^2;
|.|[x,0]|-p.|^2 < (2*r*p`2)*b by A13,A11,A9,XREAL_1:77;
then |.p-|[x,0]|.|^2 < (2*r*p`2)*b by TOPRNS_1:27;
then |.|[p`1-x,p`2-0]|.|^2 < (2*r*p`2)*b by A2,EUCLID:62;
then (p`1-x)^2+p2^2 < (2*r*p2)*b by A4,A12,JGRAPH_1:29;
then (p`1-x)^2+p2^2 - (2*r*p2)*b < 0 by XREAL_1:49;
then (p`1-x)^2+p2^2 - (2*r*p2)*b + (r*b)^2 < (r*b)^2 by XREAL_1:30;
then
A15: (p`1-x)^2+(p2 - r*b)^2 < (r*b)^2;
A16: |[p`1-x, p2-r*b]|`2 = p2-r*b by EUCLID:52;
A17: |[p`1-x, p2-r*a]|`2 = p2-r*a by EUCLID:52;
|[p`1-x, p2-r*a]|`1 = p`1-x by EUCLID:52;
then |.|[p`1-x, p2-r*a]|.|^2 > (r*a)^2 by A14,A17,JGRAPH_1:29;
then |.p-|[x,r*a]|.|^2 > (r*a)^2 by A2,EUCLID:62;
then
A18: |.p-|[x,r*a]|.| > r*a by SQUARE_1:48;
A19: r*b-|.p-|[x,r*b]|.|+|.p-|[x,r*b]|.| = r*b;
set r1 = min(r*b-|.p-|[x,r*b]|.|, |.p-|[x,r*a]|.|-r*a);
A20: |.p-|[x,r*b]|.| = |.|[x,r*b]|-p.| by TOPRNS_1:27;
|[p`1-x, p2-r*b]|`1 = p`1-x by EUCLID:52;
then |.|[p`1-x, p2-r*b]|.|^2 < (r*b)^2 by A15,A16,JGRAPH_1:29;
then
A21: |.p-|[x,r*b]|.|^2 < (r*b)^2 by A2,EUCLID:62;
r*b9 >= 0;
then |.p-|[x,r*b]|.| < r*b by A21,SQUARE_1:48;
then
r*b-|.p-|[x,r*b]|.| > 0 & r1 = r*b-|.p-|[x,r*b]|.| or |.p-|[x,r*a]|.|-r
*a > 0 & r1 = |.p-|[x,r*a]|.|-r*a by A18,XREAL_1:50,XXREAL_0:15;
then reconsider r1 as positive Real;
take r1;
r1 <= r*b-|.p-|[x,r*b]|.| by XXREAL_0:17;
then
A22: |.|[x,r*b]|-p.|+r1 <= r*b by A20,A19,XREAL_1:6;
|.p-|[p`1,0]|.| = |.|[p`1-p`1,p2-0]|.| by A2,EUCLID:62
.= |.p2.| by TOPREAL6:23
.= p2 by ABSVALUE:def 1;
then
A23: |.|[x,r*b]|-|[p`1,0]|.| <= |.|[x,r*b]|-p.|+p2 by TOPRNS_1:34;
thus now
assume r1 > p`2;
then |.|[x,r*b]|-p.|+p2 < |.|[x,r*b]|-p.|+r1 by XREAL_1:8;
then |.|[x,r*b]|-|[p`1,0]|.| < |.|[x,r*b]|-p.|+r1 by A23,XXREAL_0:2;
then |.|[x,r*b]|-|[p`1,0]|.| < r*b by A22,XXREAL_0:2;
then |.|[p`1,0]|-|[x,r*b]|.| < r*b by TOPRNS_1:27;
then
A24: |[p`1,0]| in Ball(|[x,r*b]|,r*b) by TOPREAL9:7;
|[p`1,0]| in y=0-line;
then Ball(|[x,r*b]|,r*b9) meets y=0-line by A24,XBOOLE_0:3;
hence contradiction by Th21;
end;
then
A25: Ball(p,r1) c= y>=0-plane by A2,Th20;
let u be object;
assume
A26: u in Ball(p,r1);
then reconsider q = u as Point of TOP-REAL 2;
A27: |.q-p.| < r1 by A26,TOPREAL9:7;
then |.q-p.|+|.p-|[x,r*b]|.| < r1+|.p-|[x,r*b]|.| by XREAL_1:8;
then
A28: |.q-p.|+|.p-|[x,r*b]|.| < r*b by A20,A22,XXREAL_0:2;
|.q-|[x,r*b]|.| <= |.q-p.|+|.p-|[x,r*b]|.| by TOPRNS_1:34;
then |.q-|[x,r*b]|.| < r*b by A28,XXREAL_0:2;
then
A29: +(x,r).q < b by A6,Th63;
A30: |.p-|[x,r*a]|.| <= |.p-q.|+|.q-|[x,r*a]|.| by TOPRNS_1:34;
a < b by A8,A9,XXREAL_0:2;
then
A31: a < 1 by A6,XXREAL_0:2;
|.p-|[x,r*a]|.|-r*a >= r1 by XXREAL_0:17;
then |.p-|[x,r*a]|.|-r*a > |.q-p.| by A27,XXREAL_0:2;
then
A32: |.p-|[x,r*a]|.|-|.q-p.| > r*a by XREAL_1:12;
|.p-q.| = |.q-p.| by TOPRNS_1:27;
then |.q-|[x,r*a]|.| >= |.p-|[x,r*a]|.|-|.q-p.| by A30,XREAL_1:20;
then
A33: |.q-|[x,r*a]|.| > r*a by A32,XXREAL_0:2;
q = |[q`1,q`2]| by EUCLID:53;
then q`2 >= 0 by A25,A26,Th18;
then +(x,r).q > a by A33,A5,A31,Th64;
then +(x,r).q in ].a,b.[ by A29,XXREAL_1:4;
hence thesis by A25,A26,Lm1,FUNCT_2:38;
end;
theorem Th66:
for x being Real, a,r being positive Real holds
Ball(|[x,r*a]|,r*a) c= +(x,r)"].0,a.[
proof
let x be Real;
let a,r be positive Real, u be object;
assume
A1: u in Ball(|[x,r*a]|,r*a);
then reconsider p = u as Point of TOP-REAL 2;
Ball(|[x,r*a]|,r*a) c= y>=0-plane by Th20;
then reconsider q = p as Point of Niemytzki-plane by A1,Def3;
q = |[p`1,p`2]| by EUCLID:53;
then
A2: p`2 >= 0 by Lm1,Th18;
A3: now
assume +(x,r).p = 0;
then p = |[x,0]| by A2,Th60;
then
A4: p in y=0-line;
Ball(|[x,r*a]|,r*a) misses y=0-line by Th21;
hence contradiction by A4,A1,XBOOLE_0:3;
end;
A5: +(x,r).q <= 1 by BORSUK_1:40,XXREAL_1:1;
per cases;
suppose
A6: a > 1;
A7: +(x,r).q > 0 by A3,BORSUK_1:40,XXREAL_1:1;
+(x,r).q < a by A6,A5,XXREAL_0:2;
then +(x,r).q in ].0,a.[ by A7,XXREAL_1:4;
hence thesis by FUNCT_2:38;
end;
suppose
A8: a <= 1;
|.p-|[x,r*a]|.| < r*a by A1,TOPREAL9:7;
then
A9: +(x,r).p < a by A8,Th63;
+(x,r).q > 0 by A3,BORSUK_1:40,XXREAL_1:1;
then +(x,r).q in ].0,a.[ by A9,XXREAL_1:4;
hence thesis by FUNCT_2:38;
end;
end;
theorem Th67:
for x being Real, a,r being positive Real holds
Ball(|[x,r*a]|,r*a) \/ {|[x,0]|} c= +(x,r)"[.0,a.[
proof
let x be Real;
let a,r be positive Real, u be object;
assume
A1: u in Ball(|[x,r*a]|,r*a) \/ {|[x,0]|};
then
A2: u in Ball(|[x,r*a]|,r*a) or u in {|[x,0]|} by XBOOLE_0:def 3;
reconsider p = u as Point of TOP-REAL 2 by A1;
A3: |[x,0]| in y>=0-plane;
Ball(|[x,r*a]|,r*a) c= y>=0-plane by Th20;
then reconsider q = p as Point of Niemytzki-plane by A3,A2,Lm1,TARSKI:def 1;
A4: +(x,r).q <= 1 by BORSUK_1:40,XXREAL_1:1;
A5: +(x,r).q >= 0 by BORSUK_1:40,XXREAL_1:1;
per cases by A2,TARSKI:def 1;
suppose
a > 1;
then +(x,r).q < a by A4,XXREAL_0:2;
then +(x,r).q in [.0,a.[ by A5,XXREAL_1:3;
hence thesis by FUNCT_2:38;
end;
suppose
A6: a <= 1 & u in Ball(|[x,r*a]|,r*a);
then |.p-|[x,r*a]|.| < r*a by TOPREAL9:7;
then +(x,r).p < a by A6,Th63;
then +(x,r).q in [.0,a.[ by A5,XXREAL_1:3;
hence thesis by FUNCT_2:38;
end;
suppose
u = |[x,0]|;
then +(x,r).u = 0 by Def5;
then +(x,r).q in [.0,a.[ by XXREAL_1:3;
hence thesis by FUNCT_2:38;
end;
end;
theorem Th68:
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)
proof
let p be Point of TOP-REAL 2;
assume
A1: p`2 >= 0;
let x,a be Real;
A2: p = |[p`1,p`2]| by EUCLID:53;
let r be positive Real;
set r1 = r*a;
assume that
A3: 0 < +(x,r).p and
A4: +(x,r).p < a and
A5: a <= 1;
A6: x <> p`1 implies p <> |[p`1,0]| by A4,A5,Th61;
A7: p <> |[x,0]| by A3,Def5;
assume not p in Ball(|[x,r1]|,r1);
then |.p-|[x,r1]|.| >= r1 by TOPREAL9:7;
then |.p-|[x,r1]|.| = r1 or |.p-|[x,r1]|.| > r1 & (a < 1 or a = 1) by A5,
XXREAL_0:1;
then
+(x,r).p = a or a < 1 & +(x,r).p > a or a = 1 & not p in Ball(|[x,r]|,r
) by A1,A2,A3,A5,A7,A6,Th62,Th64,TOPREAL9:7;
hence thesis by A1,A2,A4,A7,A6,Def5;
end;
theorem Th69:
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.]
proof
let p be Point of TOP-REAL 2;
assume
A1: p`2 > 0;
let x,a be Real;
let r be positive Real;
set f = +(x,r);
assume that
A2: 0 <= a and
A3: a < f.p;
A4: p = |[p`1,p`2]| by EUCLID:53;
then p in the carrier of Niemytzki-plane by A1,Lm1;
then f.p in the carrier of I[01] by FUNCT_2:5;
then f.p <= 1 by BORSUK_1:40,XXREAL_1:1;
then
A5: a < 1 by A3,XXREAL_0:2;
per cases by A2;
suppose
A6: a = 0;
reconsider r1 = p`2 as positive Real by A1;
reconsider A = Ball(p,r1) as Subset of Niemytzki-plane by A4,Lm1,Th20;
take r1;
thus r1 <= p`2;
let u be object;
assume
A7: u in Ball(p,r1);
then reconsider q = u as Point of TOP-REAL 2;
A8: q = |[q`1,q`2]| by EUCLID:53;
q in A by A7;
then
A9: q`2 >= 0 by A8,Lm1,Th18;
q in A by A7;
then reconsider z = q as Element of Niemytzki-plane;
A10: f.z >= 0 by BORSUK_1:40,XXREAL_1:1;
y=0-line misses Ball(p,r1) by A4,Th21;
then not q in y=0-line by A7,XBOOLE_0:3;
then
A11: q`2 <> 0 by A8;
A12: f.z <= 1 by BORSUK_1:40,XXREAL_1:1;
|[x,0]|`2 = 0 by EUCLID:52;
then f.q <> 0 by A11,A9,Th60;
then f.z in ].a,1.] by A10,A12,A6,XXREAL_1:2;
hence thesis by FUNCT_2:38;
end;
suppose
a > 0;
then reconsider b = a as positive Real;
set r1 = min(|.p-|[x,r*a]|.|-r*a, p`2);
A13: r1 = |.p-|[x,r*a]|.|-r*a or r1 = p`2 by XXREAL_0:def 9;
A14: b <> f.p by A3;
not |.p-|[x,r*a]|.| < r*a by A3,A5,Th63;
then |.p-|[x,r*a]|.| > r*a by A14,A1,A5,Th62,XXREAL_0:1;
then reconsider r1 as positive Real by A13,A1,XREAL_1:50;
take r1;
thus r1 <= p`2 by XXREAL_0:17;
then reconsider A = Ball(p,r1) as Subset of Niemytzki-plane by A4,Lm1,Th20;
let u be object;
assume
A15: u in Ball(p,r1);
then reconsider q = u as Point of TOP-REAL 2;
u in A by A15;
then reconsider z = q as Point of Niemytzki-plane;
A16: q = |[q`1,q`2]| by EUCLID:53;
q in A by A15;
then
A17: q`2 >= 0 by A16,Lm1,Th18;
A18: now
|.p-|[x,r*a]|.|-r*a >= r1 by XXREAL_0:17;
then
A19: r*a+r1 <= |.p-|[x,r*a]|.|-r*a+r*a by XREAL_1:6;
assume not f.z > a;
then |.q-|[x,r*a]|.| <= r*a by A2,A5,A17,Th64;
then
A20: |.|[x,r*a]|-q.| <= r*a by TOPRNS_1:27;
A21: |.|[x,r*a]|-q.|+|.q-p.| >= |.|[x,r*a]|-p.| by TOPRNS_1:34;
|.q-p.| < r1 by A15,TOPREAL9:7;
then |.|[x,r*a]|-q.|+|.q-p.| < r*a+r1 by A20,XREAL_1:8;
then |.|[x,r*a]|-p.| < r*a+r1 by A21,XXREAL_0:2;
hence contradiction by A19,TOPRNS_1:27;
end;
f.z <= 1 by BORSUK_1:40,XXREAL_1:1;
then f.z in ].a,1.] by A18,XXREAL_1:2;
hence thesis by FUNCT_2:38;
end;
end;
theorem Th70:
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}
proof
let p be Point of TOP-REAL 2;
assume
A1: p`2 = 0;
let x be Real;
let r be positive Real;
set r1 = (|.p-|[x,r]|.|-r)/2;
set f = +(x,r);
A2: p =|[p`1,p`2]| by EUCLID:53;
assume
A3: f.p = 1;
then p`1-x <> 0 by A2,A1,Def5;
then (p`1-x)^2 > 0 by SQUARE_1:12;
then (p`1-x)^2+(0-r)^2 > 0+(0-r)^2 by XREAL_1:6;
then |.|[p`1-x,p`2-r]|.|^2 > r^2 by A1,Th9;
then |.p-|[x,r]|.|^2 > r^2 by A2,EUCLID:62;
then |.p-|[x,r]|.| > r by SQUARE_1:15;
then |.p-|[x,r]|.|-r > 0 by XREAL_1:50;
then reconsider r1 as positive Real;
take r1;
let u be object;
assume
A4: u in Ball(|[p`1,r1]|,r1) \/ {p};
then reconsider q = u as Point of TOP-REAL 2;
A5: Ball(|[p`1,r1]|,r1) c= y>=0-plane by Th20;
u in Ball(|[p`1,r1]|,r1) or u = p by A4,ZFMISC_1:136;
then reconsider z = q as Point of Niemytzki-plane by A5,A1,A2,Lm1,Th18;
A6: q = |[q`1,q`2]| by EUCLID:53;
A7: now
assume
A8: q in Ball(|[p`1,r1]|,r1);
then |.q-|[p`1,r1]|.| < r1 by TOPREAL9:7;
then
A9: |.q-|[p`1,r1]|.|+|.|[p`1,r1]|-p.| < r1+|.|[p`1,r1]|-p.| by XREAL_1:6;
A10: |.r1.| = r1 by ABSVALUE:def 1;
A11: |.q-|[p`1,r1]|.|+|.|[p`1,r1]|-p.| >= |.q-p.| by TOPRNS_1:34;
A12: |.q-p.|+|.|[x,r]|-q.| >= |.|[x,r]|-p.| by TOPRNS_1:34;
A13: |.|[0,r1]|.| = |.r1.| by TOPREAL6:23;
|[p`1,r1]|-p = |[p`1-p`1,r1-0]| by A1,A2,EUCLID:62;
then r1+r1 > |.q-p.| by A9,A11,A10,A13,XXREAL_0:2;
then |.p-|[x,r]|.|-r+|.|[x,r]|-q.| > |.q-p.|+|.|[x,r]|-q.| by XREAL_1:6;
then |.|[x,r]|-p.| < |.p-|[x,r]|.|-r+|.|[x,r]|-q.| by A12,XXREAL_0:2;
then
A14: |.|[x,r]|-p.|-(|.p-|[x,r]|.|-r) < |.|[x,r]|-q.| by XREAL_1:19;
|.p-|[x,r]|.| = |.|[x,r]|-p.| by TOPRNS_1:27;
then |.q-|[x,r]|.| > r by A14,TOPRNS_1:27;
hence not q in Ball(|[x,r]|,r) by TOPREAL9:7;
q`2 = 0 implies q in y=0-line & Ball(|[p`1,r1]|,r1) misses y=0-line
by A6,Th21;
hence q`2 <> 0 by A8,XBOOLE_0:3;
end;
z in y>=0-plane by Lm1;
then q`2 >= 0 by A6,Th18;
then f.z = 1 by A7,A3,A4,A6,Def5,ZFMISC_1:136;
then f.z in {1} by TARSKI:def 1;
hence thesis by FUNCT_2:38;
end;
theorem Th71:
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
proof
let T be non empty TopSpace;
let S be SubSpace of T;
let B be Basis of T;
set X = {A/\[#]S where A is Subset of T: A in B & A meets [#]S};
X c= bool the carrier of S
proof
let u be object;
assume u in X;
then ex A being Subset of T st u = A/\[#]S & A in B & A meets [#]S;
hence thesis;
end;
then reconsider X as Subset-Family of S;
A1: now
let U be Subset of S;
assume U is open;
then consider U0 being Subset of T such that
A2: U0 is open and
A3: U = U0 /\ the carrier of S by TSP_1:def 1;
let x be Point of S;
assume
A4: x in U;
then x in U0 by A3,XBOOLE_0:def 4;
then consider V0 being Subset of T such that
A5: V0 in B and
A6: x in V0 and
A7: V0 c= U0 by A2,YELLOW_9:31;
reconsider V = V0 /\ [#]S as Subset of S;
take V;
V0 meets [#]S by A4,A6,XBOOLE_0:3;
hence V in X by A5;
thus x in V by A4,A6,XBOOLE_0:def 4;
thus V c= U by A3,A7,XBOOLE_1:26;
end;
X c= the topology of S
proof
let u be object;
assume u in X;
then
A8: ex A being Subset of T st u = A/\[#]S & A in B & A meets [#]S;
B c= the topology of T by TOPS_2:64;
hence thesis by A8,PRE_TOPC:def 4;
end;
hence thesis by A1,YELLOW_9:32;
end;
theorem Th72:
{].a,b.[ where a,b is Real: a < b} is Basis of R^1
proof
set X = {].a,b.[ where a,b is Real: a < b};
X c= bool REAL
proof
let u be object;
assume u in X;
then ex a,b being Real st u = ].a,b.[ & a < b;
hence thesis;
end;
then reconsider X as Subset-Family of R^1 by TOPMETR:17;
A1: now
let U be Subset of R^1 such that
A2: U is open;
let x be Point of R^1 such that
A3: x in U;
reconsider a = x as Real;
consider r being Real such that
A4: 0 < r and
A5: ].a-r,a+r.[ c= U by A2,A3,FRECHET:8;
reconsider V = ].a-r,a+r.[ as Subset of R^1 by TOPMETR:17;
take V;
A6: a < a+r by A4,XREAL_1:29;
A7: a-r < a by A4,XREAL_1:44;
then a-r < a+r by A6,XXREAL_0:2;
hence V in X;
thus x in V by A7,A6,XXREAL_1:4;
thus V c= U by A5;
end;
X c= the topology of R^1
proof
let u be object;
assume u in X;
then ex a, b being Real st u = ].a,b.[ & a < b;
then u is open Subset of R^1 by JORDAN6:35,TOPMETR:17;
hence thesis by PRE_TOPC:def 2;
end;
hence thesis by A1,YELLOW_9:32;
end;
theorem Th73:
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
let T be TopSpace;
let U,V be Subset of T;
let B be set;
assume that
A1: U in B and
A2: V in B and
A3: B \/ {U \/ V} is Basis of T;
A4: B c= B \/ {U \/ V} by XBOOLE_1:7;
then reconsider B9 = B as Subset-Family of T by A3,XBOOLE_1:1;
A5: now
A6: V c= U\/V by XBOOLE_1:7;
A7: U c= U\/V by XBOOLE_1:7;
let A be Subset of T such that
A8: A is open;
let p be Point of T;
assume p in A;
then consider A9 being Subset of T such that
A9: A9 in B \/ {U\/V} and
A10: p in A9 and
A11: A9 c= A by A3,A8,YELLOW_9:31;
assume
A12: not ex a being Subset of T st a in B9 & p in a & a c= A;
A9 in B or A9 = U \/ V by A9,ZFMISC_1:136;
then p in U & U c= A or p in V & V c= A by A10,A11,A12,A7,A6,XBOOLE_0:def 3
;
hence contradiction by A1,A2,A12;
end;
B \/ {U \/ V} c= the topology of T by A3,TOPS_2:64;
hence thesis by A5,A4,XBOOLE_1:1,YELLOW_9:32;
end;
theorem Th74:
{[.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
reconsider U = [.0,2/3.[, V = ].1/3,1.] as Subset of I[01] by BORSUK_1:40
,XXREAL_1:35,36;
reconsider B = {].a,b.[ where a,b is Real:
a < b} as Basis of R^1 by Th72;
set S = I[01], T = R^1;
set A1 = {[.0,a.[ where a is Real: 0 < a & a <= 1};
set A2 = {].a,1.] where a is Real: 0 <= a & a < 1};
set A3 = {].a,b.[ where a,b is Real: 0 <= a & a < b & b <= 1};
set B9 = {A/\[#]S where A is Subset of T: A in B & A meets [#]S};
A1: B9 = A1 \/ A2 \/ A3 \/ {[#]S}
proof
reconsider aa = ].-1,2.[ as Subset of T by TOPMETR:17;
thus B9 c= A1 \/ A2 \/ A3 \/ {[#]S}
proof
let u be object;
assume u in B9;
then consider A being Subset of T such that
A2: u = A/\[#]S and
A3: A in B and
A4: A meets [#]S;
consider x being object such that
A5: x in A and
A6: x in [#]S by A4,XBOOLE_0:3;
consider a,b being Real such that
A7: A = ].a,b.[ and
A8: a < b by A3;
reconsider x as Real by A5;
A9: a < x by A7,A5,XXREAL_1:4;
A10: x <= 1 by A6,BORSUK_1:40,XXREAL_1:1;
A11: 0 <= x by A6,BORSUK_1:40,XXREAL_1:1;
per cases;
suppose
A12: a < 0 & b <= 1;
A13: 0 < b by A11,A7,A5,XXREAL_1:4;
u = [.0,b.[ by A12,A2,A7,BORSUK_1:40,XXREAL_1:148;
then u in A1 by A13,A12;
then u in A1 \/ A2 by XBOOLE_0:def 3;
then u in A1 \/ A2 \/ (A3 \/ {[#]S}) by XBOOLE_0:def 3;
hence thesis by XBOOLE_1:4;
end;
suppose
a < 0 & b > 1;
then u = [#]S by A2,A7,BORSUK_1:40,XBOOLE_1:28,XXREAL_1:47;
hence thesis by ZFMISC_1:136;
end;
suppose
A14: a >= 0 & b <= 1;
then u = A by A2,A7,BORSUK_1:40,XBOOLE_1:28,XXREAL_1:37;
then u in A3 by A7,A8,A14;
then u in A1 \/ A2 \/ A3 by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A15: a >= 0 & b > 1;
A16: a < 1 by A10,A9,XXREAL_0:2;
u = ].a,1.] by A15,A2,A7,BORSUK_1:40,XXREAL_1:149;
then u in A2 by A16,A15;
then u in A1 \/ A2 by XBOOLE_0:def 3;
then u in A1 \/ A2 \/ (A3 \/ {[#]S}) by XBOOLE_0:def 3;
hence thesis by XBOOLE_1:4;
end;
end;
let u be object;
assume u in A1 \/ A2 \/ A3 \/ {[#]S};
then u in A1 \/ A2 \/ A3 or u in {[#]S} by XBOOLE_0:def 3;
then
A17: u in A1 \/ A2 or u in A3 or u in {[#]S} by XBOOLE_0:def 3;
per cases by A17,XBOOLE_0:def 3;
suppose
u in {[#]S};
then u = [#]S by TARSKI:def 1;
then
A18: u = aa/\[#]S by BORSUK_1:40,XBOOLE_1:28,XXREAL_1:47;
[#]S c= aa by BORSUK_1:40,XXREAL_1:47;
then
A19: aa meets [#]S by XBOOLE_1:68;
aa in B;
hence thesis by A18,A19;
end;
suppose
u in A1;
then consider a being Real such that
A20: u = [.0,a.[ and
A21: 0 < a and
A22: a <= 1;
reconsider A = ].-1,a.[ as Subset of T by TOPMETR:17;
A23: A in B by A21;
A24: 0 in [.0,1.] by XXREAL_1:1;
0 in A by A21,XXREAL_1:4;
then
A25: A meets [#]S by A24,BORSUK_1:40,XBOOLE_0:3;
u = A /\ [.0,1.] by A20,A22,XXREAL_1:148;
hence thesis by A23,A25,BORSUK_1:40;
end;
suppose
u in A2;
then consider a being Real such that
A26: u = ].a,1.] and
A27: 0 <= a and
A28: a < 1;
reconsider A = ].a,2.[ as Subset of T by TOPMETR:17;
2 > a by A28,XXREAL_0:2;
then
A29: A in B;
A30: 1 in [.0,1.] by XXREAL_1:1;
1 in A by A28,XXREAL_1:4;
then
A31: A meets [#]S by A30,BORSUK_1:40,XBOOLE_0:3;
u = A /\ [.0,1.] by A26,A27,XXREAL_1:149;
hence thesis by A29,A31,BORSUK_1:40;
end;
suppose
u in A3;
then consider a,b being Real such that
A32: u = ].a,b.[ and
A33: 0 <= a and
A34: a < b and
A35: b <= 1;
reconsider A = ].a,b.[ as Subset of T by TOPMETR:17;
A36: A c= [.0,1.] by A33,A35,XXREAL_1:37;
a+b < b+b by A34,XREAL_1:8;
then
A37: (a+b)/2 < (b+b)/2 by XREAL_1:74;
a+a < a+b by A34,XREAL_1:8;
then (a+a)/2 < (a+b)/2 by XREAL_1:74;
then (a+b)/2 in A by A37,XXREAL_1:4;
then
A38: A meets [#]S by A36,BORSUK_1:40,XBOOLE_0:3;
A39: A in B by A34;
u = A /\ [.0,1.] by A33,A35,A32,XBOOLE_1:28,XXREAL_1:37;
hence thesis by A39,A38,BORSUK_1:40;
end;
end;
U in A1;
then U in A1 \/ A2 by XBOOLE_0:def 3;
then
A40: U in A1 \/ A2 \/ A3 by XBOOLE_0:def 3;
V in A2;
then V in A1 \/ A2 by XBOOLE_0:def 3;
then
A41: V in A1 \/ A2 \/ A3 by XBOOLE_0:def 3;
U \/ V = [#]S by BORSUK_1:40,XXREAL_1:175;
hence thesis by A1,A40,A41,Th71,Th73;
end;
theorem Th75:
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
proof
set A3 = {].a,b.[ where a,b is Real: 0 <= a & a < b & b <= 1};
set A2 = {].a,1.] where a is Real: 0 <= a & a < 1};
set A1 = {[.0,a.[ where a is Real: 0 < a & a <= 1};
reconsider B = A1 \/ A2 \/ A3 as Basis of I[01] by Th74;
let T be non empty TopSpace;
let f be Function of T, I[01];
hereby
assume
A1: f is continuous;
let a,b be Real;
reconsider x = a, y = b as Real;
assume that
A2: 0 <= a and
A3: a < 1 and
A4: 0 < b and
A5: b <= 1;
].x,1.] in A2 by A2,A3;
then ].x,1.] in A1 \/ A2 by XBOOLE_0:def 3;
then
A6: ].x,1.] in B by XBOOLE_0:def 3;
[.0,y.[ in A1 by A4,A5;
then [.0,y.[ in A1 \/ A2 by XBOOLE_0:def 3;
then [.0,y.[ in B by XBOOLE_0:def 3;
hence f"[.0,b.[ is open & f"].a,1.] is open by A6,A1,YELLOW_9:34;
end;
assume
A7: 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;
now
let A be Subset of I[01];
assume A in B;
then
A8: A in A1 \/ A2 or A in A3 by XBOOLE_0:def 3;
per cases by A8,XBOOLE_0:def 3;
suppose
A in A1;
then ex a being Real st A = [.0,a.[ & 0 < a & a <= 1;
hence f"A is open by A7;
end;
suppose
A in A2;
then ex a being Real st A = ].a,1.] & 0 <= a & a < 1;
hence f"A is open by A7;
end;
suppose
A in A3;
then consider a,b being Real such that
A9: A = ].a,b.[ and
A10: 0 <= a and
A11: a < b and
A12: b <= 1;
a < 1 by A11,A12,XXREAL_0:2;
then reconsider
U = f"[.0,b.[, V = f"].a,1.] as open Subset of T by A10,A11,A7,A12;
A = [.0,b.[ /\ ].a,1.] by A9,A10,A12,XXREAL_1:153;
then f"A = U /\ V by FUNCT_1:68;
hence f"A is open;
end;
end;
hence thesis by YELLOW_9:34;
end;
registration
let x be Real, r be positive Real;
cluster +(x,r) -> continuous;
coherence
proof
set f = +(x,r);
consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q
is Real: q > 0} and
A2: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\
y>=0-plane where q is Real: q > 0} by Def3;
A3: dom BB = y>=0-plane by Lm1,PARTFUN1:def 2;
now
let a,b be Real;
assume that
A4: 0 <= a and
A5: a < 1 and
A6: 0 < b and
A7: b <= 1;
now
let c be Element of Niemytzki-plane;
assume c in f"[.0,b.[;
then
A8: f.c in [.0,b.[ by FUNCT_1:def 7;
c in y>=0-plane by Lm1;
then reconsider z = c as Point of TOP-REAL 2;
z = |[z`1,z`2]| by EUCLID:53;
then
A9: z`2 >= 0 by Lm1,Th18;
per cases by A8,XXREAL_1:3;
suppose
A10: f.c = 0;
reconsider r1 = r*b as positive Real by A6;
reconsider U = Ball(|[x,r1]|,r1) \/ {|[x,0]|} as Subset of
Niemytzki-plane by Th27;
take U;
A11: |[x,0]| in y>=0-plane;
U in {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is Real:
q > 0};
then
A12: U in BB.(|[x,0]|) by A1;
z = |[x,0]| by A10,A9,Th60;
hence U in Union BB & c in U & U c= f"[.0,b.[ by A12,A11,A3,A6,Th67,
CARD_5:2,ZFMISC_1:136;
end;
suppose
A13: 0 < f.c & f.c < b;
reconsider r1 = r*b as positive Real by A6;
reconsider U = Ball(|[x,r1]|,r1) as Subset of Niemytzki-plane by Th29
;
take U;
A14: |[x,r1]| in y>=0-plane;
U c= y>=0-plane by Th20;
then U /\ y>=0-plane = U by XBOOLE_1:28;
then
U in {Ball(|[x,r1]|,q) /\ y>=0-plane where q is Real
: q > 0};
then U in BB.(|[x,r1]|) by A2;
hence U in Union BB by A14,A3,CARD_5:2;
A15: f"].0,b.[ c= f"[.0,b.[ by RELAT_1:143,XXREAL_1:45;
Ball(|[x,r*b]|,r*b) c= +(x, r)"].0,b.[ by A13,Th66;
hence c in U & U c= f"[.0,b.[ by A15,A13,A7,A9,Th68;
end;
end;
hence f"[.0,b.[ is open by YELLOW_9:31;
now
let c be Element of Niemytzki-plane;
c in y>=0-plane by Lm1;
then reconsider z = c as Point of TOP-REAL 2;
assume c in f"].a,1.];
then
A16: f.c in ].a,1.] by FUNCT_1:def 7;
then
A17: f.c > a by XXREAL_1:2;
A18: f.c <= 1 by A16,XXREAL_1:2;
A19: z = |[z`1,z`2]| by EUCLID:53;
then
A20: z`2 >= 0 by Lm1,Th18;
per cases by A19,A16,A18,Lm1,Th18,XXREAL_0:1,XXREAL_1:2;
suppose
z`2 > 0;
then consider r1 being positive Real such that
A21: r1 <= z`2 and
A22: Ball(z,r1) c= +(x,r)"].a,1.] by A4,A17,Th69;
reconsider U = Ball(z,r1) as Subset of Niemytzki-plane by A19,A21
,Th29;
U c= y>=0-plane by A19,A21,Th20;
then
A23: U /\ y>=0-plane = U by XBOOLE_1:28;
U in {Ball(|[z`1,z`2]|,q) /\ y>=0-plane
where q is Real: q > 0} by A23,A19;
then
A24: U in BB.(|[z`1,z`2]|) by A21,A2;
take U;
|[z`1,z`2]| in y>=0-plane by A21;
hence U in Union BB by A24,A3,CARD_5:2;
thus c in U & U c= f"].a,1.] by A22,Th13;
end;
suppose
A25: f.c = 1 & z`2 = 0;
then consider r1 being positive Real such that
A26: Ball(|[z`1,r1]|,r1) \/ {z} c= +(x,r)"{1} by Th70;
reconsider U = Ball(|[z`1,r1]|,r1) \/ {z} as Subset of
Niemytzki-plane by A19,A25,Th27;
U in {Ball(|[z`1,q]|,q) \/ {|[z`1,0]|}
where q is Real: q > 0} by A19,A25;
then
A27: U in BB.(|[z`1,z`2]|) by A1,A25;
take U;
|[z`1,z`2]| in y>=0-plane by A25;
hence U in Union BB by A27,A3,CARD_5:2;
thus c in U by ZFMISC_1:136;
1 in ].a,1.] by A5,XXREAL_1:2;
then {1} c= ].a,1.] by ZFMISC_1:31;
then f"{1} c= f"].a,1.] by RELAT_1:143;
hence U c= f"].a,1.] by A26;
end;
suppose
a < f.c & f.c < 1;
then f.c in ].a,1.[ by XXREAL_1:4;
then consider r1 being positive Real such that
A28: r1 <= z`2 and
A29: Ball(z,r1) c= +(x,r)"].a,1.[ by A4,A20,Th65;
reconsider U = Ball(z,r1) as Subset of Niemytzki-plane by A19,A28
,Th29;
U c= y>=0-plane by A19,A28,Th20;
then
A30: U /\ y>=0-plane = U by XBOOLE_1:28;
U in {Ball(|[z`1,z`2]|,q) /\ y>=0-plane
where q is Real: q > 0} by A30,A19;
then
A31: U in BB.(|[z`1,z`2]|) by A28,A2;
take U;
|[z`1,z`2]| in y>=0-plane by A28;
hence U in Union BB by A31,A3,CARD_5:2;
f"].a,1.[ c= f"].a,1.] by RELAT_1:143,XXREAL_1:41;
hence c in U & U c= f"].a,1.] by A29,Th13;
end;
end;
hence f"].a,1.] is open by YELLOW_9:31;
end;
hence thesis by Th75;
end;
end;
theorem Th76:
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))
proof
let U be Subset of Niemytzki-plane;
let x,r;
assume
A1: U = Ball(|[x,r]|,r) \/ {|[x,0]|};
take f = +(x,r);
thus f.(|[x,0]|) = 0 by Def5;
let a,b be Real;
thus |[a,b]| in U` implies f.(|[a,b]|) = 1
proof
assume
A2: |[a,b]| in U`;
then
A3: not |[a,b]| in U by XBOOLE_0:def 5;
then
A4: not |[a,b]| in Ball(|[x,r]|,r) by A1,ZFMISC_1:136;
A5: a <> x or b <> 0 by A3,A1,ZFMISC_1:136;
b >= 0 by A2,Lm1,Th18;
hence thesis by A4,A5,Def5;
end;
assume
A6: |[a,b]| in U\{|[x,0]|};
then
A7: not |[a,b]| in {|[x,0]|} by XBOOLE_0:def 5;
|[a,b]| in U by A6,XBOOLE_0:def 5;
then
A8: |[a,b]| in Ball(|[x,r]|,r) by A7,A1,XBOOLE_0:def 3;
b >= 0 by A6,Lm1,Th18;
hence thesis by A8,Def5;
end;
::<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, r be positive Real;
func +(x,y,r) -> Function of Niemytzki-plane, I[01] means
:Def6:
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);
existence
proof
deffunc F1(Point of TOP-REAL 2) = 1;
deffunc F2(Point of TOP-REAL 2) = |.|[x,y]|-$1.|/r;
defpred P[set] means not $1 in Ball(|[x,y]|, r);
A1: for a being Point of TOP-REAL 2 st a in the carrier of Niemytzki-plane
holds (P[a] implies F1(a) in the carrier of I[01]) & (not P[a] implies F2(a) in
the carrier of I[01])
proof
let a be Point of TOP-REAL 2;
assume a in the carrier of Niemytzki-plane;
thus P[a] implies F1(a) in the carrier of I[01] by BORSUK_1:40,XXREAL_1:1
;
assume not P[a];
then |.a-|[x,y]|.| < r by TOPREAL9:7;
then |.|[x,y]|-a.| < r by TOPRNS_1:27;
then
A2: F2(a) < r/r by XREAL_1:74;
r/r = 1 by XCMPLX_1:60;
hence thesis by A2,BORSUK_1:40,XXREAL_1:1;
end;
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then
A3: the carrier of Niemytzki-plane c= the carrier of TOP-REAL 2;
consider f being Function of Niemytzki-plane, I[01] such that
A4: for a being Point of TOP-REAL 2 st a in the carrier of
Niemytzki-plane holds (P[a] implies f.a = F1(a)) & (not P[a] implies f.a = F2(a
)) from SCH1(A3,A1);
take f;
let a be Real, b be non negative Real;
|[a,b]| in the carrier of Niemytzki-plane by Lm1;
hence thesis by A4;
end;
uniqueness
proof
let f,g be Function of Niemytzki-plane, I[01] such that
A5: for a being Real, b being non negative Real holds
(not |[a,b]| in Ball(|[x,y]|,r) implies f.(|[a,b]|) = 1) & (|[a,b]| in Ball(|[x
,y]|,r) implies f.(|[a,b]|) = |.|[x,y]|-|[a,b]|.|/r) and
A6: for a being Real, b being non negative Real holds
(not |[a,b]| in Ball(|[x,y]|,r) implies g.(|[a,b]|) = 1) & (|[a,b]| in Ball(|[x
,y]|,r) implies g.(|[a,b]|) = |.|[x,y]|-|[a,b]|.|/r);
A7: the carrier of Niemytzki-plane = y>=0-plane by Def3;
now
let p be Point of Niemytzki-plane;
p in y>=0-plane by A7;
then reconsider q = p as Point of TOP-REAL 2;
A8: p = |[q`1,q`2]| by EUCLID:53;
then reconsider q2 = q`2 as non negative Real by A7,Th18;
per cases;
suppose
A9: not |[q`1,q2]| in Ball(|[x,y]|,r);
then f.p = 1 by A5,A8;
hence f.p = g.p by A9,A6,A8;
end;
suppose
A10: |[q`1,q2]| in Ball(|[x,y]|,r);
then f.p = |.|[x,y]|-q.|/r by A5,A8;
hence f.p = g.p by A10,A6,A8;
end;
end;
hence thesis;
end;
end;
theorem Th77:
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]|
proof
let p be Point of TOP-REAL 2;
assume
A1: p`2 >= 0;
let x be Real;
let y be non negative Real;
let r be positive Real;
A2: p = |[p`1,p`2]| by EUCLID:53;
hereby
assume
A3: +(x,y,r).p = 0;
then p in Ball(|[x,y]|,r) by A1,A2,Def6;
then 0 = |.|[x,y]|-p.|/r by A1,A2,A3,Def6;
then 0 * r = |.|[x,y]|-p.|;
hence p = |[x,y]| by TOPRNS_1:28;
end;
assume
A4: p = |[x,y]|;
then p in Ball(|[x,y]|,r) by Th13;
hence +(x,y,r).p = |.|[x,y]|-p.|/r by A4,Def6
.= 0/r by A4,TOPRNS_1:28
.= 0;
end;
theorem Th78:
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
proof
let x be Real;
let y be non negative Real;
let r,a be positive Real;
set f = +(x,y,r);
assume
A1: a <= 1;
then r*a <= r*1 by XREAL_1:64;
then
A2: Ball(|[x,y]|,r*a) c= Ball(|[x,y]|,r) by JORDAN:18;
thus +(x,y,r)"[.0,a.[ c= Ball(|[x,y]|,r*a) /\ y>=0-plane
proof
let u be object;
assume
A3: u in f"[.0,a.[;
then reconsider p = u as Point of Niemytzki-plane;
p in y>=0-plane by Lm1;
then reconsider q = p as Element of TOP-REAL 2;
f.p in [.0,a.[ by A3,FUNCT_2:38;
then
A4: f.p < a by XXREAL_1:3;
A5: p = |[q`1,q`2]| by EUCLID:53;
then
A6: q`2 >= 0 by Lm1,Th18;
then p in Ball(|[x,y]|,r) by A4,A1,A5,Def6;
then f.p = |.|[x,y]|-q.|/r by A5,A6,Def6;
then
A7: |.|[x,y]|-q.| < r*a by A4,XREAL_1:77;
|.|[x,y]|-q.| = |.q-|[x,y]|.| by TOPRNS_1:27;
then p in Ball(|[x,y]|,r*a) by A7,TOPREAL9:7;
hence thesis by Lm1,XBOOLE_0:def 4;
end;
let u be object;
assume
A8: u in Ball(|[x,y]|,r*a) /\ y>=0-plane;
then reconsider p = u as Point of Niemytzki-plane by Lm1,XBOOLE_0:def 4;
reconsider q = p as Element of TOP-REAL 2 by A8;
A9: u in Ball(|[x,y]|,r*a) by A8,XBOOLE_0:def 4;
then
A10: |.q-|[x,y]|.| < r*a by TOPREAL9:7;
A11: |.|[x,y]|-q.| = |.q-|[x,y]|.| by TOPRNS_1:27;
A12: p = |[q`1,q`2]| by EUCLID:53;
u in y>=0-plane by A8,XBOOLE_0:def 4;
then q`2 >= 0 by A12,Th18;
then
A13: f.p = |.|[x,y]|-q.|/r by A2,A9,A12,Def6;
then r*(f.p) = |.|[x,y]|-q.| by XCMPLX_1:87;
then f.p < a by A10,A11,XREAL_1:64;
then f.p in [.0,a.[ by A13,XXREAL_1:3;
hence thesis by FUNCT_2:38;
end;
theorem Th79:
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.]
proof
let p be Point of TOP-REAL 2;
assume
A1: p`2 > 0;
let x be Real;
let a be non negative Real;
let y,r be positive Real;
set f = +(x,y,r);
A2: p = |[p`1,p`2]| by EUCLID:53;
then p in y>=0-plane by A1;
then f.p in [.0,1.] by Lm1,BORSUK_1:40,FUNCT_2:5;
then
A3: f.p <= 1 by XXREAL_1:1;
assume
A4: f.p > a;
then
A5: a < 1 by A3,XXREAL_0:2;
A6: |.|[x,y]|-p.| = |.p-|[x,y]|.| by TOPRNS_1:27;
thus |.|[x,y]|-p.| > r*a
proof
per cases by A3,XXREAL_0:1;
suppose
f.p < 1;
then p in Ball(|[x,y]|,r) by A1,A2,Def6;
then f.p = |.|[x,y]|-p.|/r by A1,A2,Def6;
hence thesis by A4,XREAL_1:79;
end;
suppose
A7: f.p = 1;
now
A8: r/r = 1 by XCMPLX_1:60;
assume
A9: p in Ball(|[x,y]|,r);
then
A10: |.p-|[x,y]|.| < r by TOPREAL9:7;
1 = |.|[x,y]|-p.|/r by A9,A1,A2,A7,Def6;
hence contradiction by A10,A8,A6,XREAL_1:74;
end;
then
A11: |.p-|[x,y]|.| >= r by TOPREAL9:7;
r*1 > r*a by A5,XREAL_1:68;
hence thesis by A11,A6,XXREAL_0:2;
end;
end;
then reconsider r1 = |.|[x,y]|-p.|-r*a as positive Real by XREAL_1:50;
let u be object;
assume
A12: u in Ball(p,|.|[x,y]|-p.|-r*a) /\ y>=0-plane;
then reconsider z = u as Point of Niemytzki-plane by Lm1,XBOOLE_0:def 4;
reconsider q = z as Element of TOP-REAL 2 by A12;
u in Ball(p,|.|[x,y]|-p.|-r*a) by A12,XBOOLE_0:def 4;
then |.q-p.| < r1 by TOPREAL9:7;
then
A13: |.|[x,y]|-q.|+|.q-p.| < |.|[x,y]|-q.|+r1 by XREAL_1:6;
A14: q = |[q`1,q`2]| by EUCLID:53;
then
A15: q`2 >= 0 by Lm1,Th18;
|.|[x,y]|-p.| <= |.|[x,y]|-q.|+|.q-p.| by TOPRNS_1:34;
then |.|[x,y]|-p.| < |.|[x,y]|-q.|+r1 by A13,XXREAL_0:2;
then
A16: |.|[x,y]|-p.|-r1 < |.|[x,y]|-q.|+r1-r1 by XREAL_1:9;
A17: now
assume q in Ball(|[x,y]|,r);
then f.q = |.|[x,y]|-q.|/r by A14,A15,Def6;
hence f.z > a by A16,XREAL_1:81;
end;
f.z in [.0,1.] by BORSUK_1:40;
then
A18: f.z <= 1 by XXREAL_1:1;
not q in Ball(|[x,y]|,r) implies f.q = 1 by A15,A14,Def6;
then f.z in ].a,1.] by A18,A5,A17,XXREAL_1:2;
hence thesis by FUNCT_2:38;
end;
theorem Th80:
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
.]
proof
let p be Point of TOP-REAL 2;
A1: p = |[p`1,p`2]| by EUCLID:53;
assume
A2: p`2 = 0;
then reconsider p9 = p as Point of Niemytzki-plane by A1,Lm1,Th18;
let x be Real;
let a be non negative Real;
let y,r be positive Real;
set f = +(x,y,r);
p in y>=0-plane by A2,A1;
then f.p in [.0,1.] by Lm1,BORSUK_1:40,FUNCT_2:5;
then
A3: f.p <= 1 by XXREAL_1:1;
assume
A4: f.p > a;
then
A5: a < 1 by A3,XXREAL_0:2;
A6: |.|[x,y]|-p.| = |.p-|[x,y]|.| by TOPRNS_1:27;
thus |.|[x,y]|-p.| > r*a
proof
per cases by A3,XXREAL_0:1;
suppose
f.p < 1;
then p in Ball(|[x,y]|,r) by A2,A1,Def6;
then f.p = |.|[x,y]|-p.|/r by A2,A1,Def6;
hence thesis by A4,XREAL_1:79;
end;
suppose
A7: f.p = 1;
now
A8: r/r = 1 by XCMPLX_1:60;
assume
A9: p in Ball(|[x,y]|,r);
then
A10: |.p-|[x,y]|.| < r by TOPREAL9:7;
1 = |.|[x,y]|-p.|/r by A9,A2,A1,A7,Def6;
hence contradiction by A10,A8,A6,XREAL_1:74;
end;
then
A11: |.p-|[x,y]|.| >= r by TOPREAL9:7;
r*1 > r*a by A5,XREAL_1:68;
hence thesis by A11,A6,XXREAL_0:2;
end;
end;
then reconsider r9 = |.|[x,y]|-p.|-r*a as positive Real by XREAL_1:50;
take r1 = r9/2;
thus r1 = (|.|[x,y]|-p.|-r*a)/2;
let u be object;
A12: Ball(|[p`1,r1]|,r1) c= y>=0-plane by Th20;
assume
A13: u in Ball(|[p`1,r1]|,r1) \/ {p};
then u in Ball(|[p`1,r1]|,r1) or u = p9 by ZFMISC_1:136;
then reconsider z = u as Point of Niemytzki-plane by A12,Def3;
reconsider q = z as Element of TOP-REAL 2 by A13;
A14: q = |[q`1,q`2]| by EUCLID:53;
then
A15: q`2 >= 0 by Lm1,Th18;
then
A16: not q in Ball(|[x,y]|,r) implies f.q = 1 by A14,Def6;
per cases by A13,ZFMISC_1:136;
suppose
u = p9;
then f.z in ].a,1.] by A4,A3,XXREAL_1:2;
hence thesis by FUNCT_2:38;
end;
suppose
u in Ball(|[p`1,r1]|,r1);
then |.q-|[p`1,r1]|.| < r1 by TOPREAL9:7;
then
A17: |.q-|[p`1,r1]|.|+|.|[p`1,r1]|-p.| < r1+|.|[p`1,r1]|-p.| by XREAL_1:6;
|.q-p.| <= |.q-|[p`1,r1]|.|+|.|[p`1,r1]|-p.| by TOPRNS_1:34;
then
A18: |.q-p.| < r1+|.|[p`1,r1]|-p.| by A17,XXREAL_0:2;
reconsider r1 as Real;
A19: |.|[0,r1]|.| = |.r1.| by TOPREAL6:23;
A20: |.|[x,y]|-p.| <= |.|[x,y]|-q.|+|.q-p.| by TOPRNS_1:34;
A21: |.r1.| = r1 by ABSVALUE:def 1;
|.|[p`1,r1]|-p.| = |.|[p`1-p`1,r1-0 ]|.| by A2,A1,EUCLID:62;
then |.|[x,y]|-q.|+|.q-p.| < |.|[x,y]|-q.|+(r1+r1)
by A18,A19,A21,XREAL_1:6;
then |.|[x,y]|-p.| < |.|[x,y]|-q.|+(r1+r1) by A20,XXREAL_0:2;
then
A22: |.|[x,y]|-p.|-(r1+r1) < |.|[x,y]|-q.|+(r1+r1)-(r1+r1) by XREAL_1:9;
A23: now
assume q in Ball(|[x,y]|,r);
then f.q = |.|[x,y]|-q.|/r by A14,A15,Def6;
hence f.z > a by A22,XREAL_1:81;
end;
f.z in [.0,1.] by BORSUK_1:40;
then f.z <= 1 by XXREAL_1:1;
then f.z in ].a,1.] by A5,A16,A23,XXREAL_1:2;
hence thesis by FUNCT_2:38;
end;
end;
registration
let x be Real;
let y,r be positive Real;
cluster +(x,y,r) -> continuous;
coherence
proof
set f = +(x,y,r);
consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q
is Real: q > 0} and
A2: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\
y>=0-plane where q is Real: q > 0} by Def3;
A3: dom BB = y>=0-plane by Lm1,PARTFUN1:def 2;
now
let a,b be Real;
assume that
A4: 0 <= a and
a < 1 and
A5: 0 < b and
A6: b <= 1;
f"[.0,b.[ = Ball(|[x,y]|,r*b) /\ y>=0-plane by A5,A6,Th78;
hence f"[.0,b.[ is open by A5,Th28;
now
let c be Element of Niemytzki-plane;
c in y>=0-plane by Lm1;
then reconsider z = c as Point of TOP-REAL 2;
A7: z = |[z`1,z`2]| by EUCLID:53;
assume c in f"].a,1.];
then f.c in ].a,1.] by FUNCT_1:def 7;
then
A8: f.c > a by XXREAL_1:2;
per cases by A7,Lm1,Th18;
suppose
A9: z`2 > 0;
then reconsider r1 = |.|[x,y]|-z.|-r*a as positive Real by A4,A8,Th79
,XREAL_1:50;
reconsider U = Ball(z,r1) /\ y>=0-plane as Subset of Niemytzki-plane
by A7,A9,Th28;
U in {Ball(|[z`1,z`2]|,q) /\ y>=0-plane
where q is Real: q > 0} by A7;
then
A10: U in BB.(|[z`1,z`2]|) by A2,A9;
take U;
|[z`1,z`2]| in y>=0-plane by A9;
hence U in Union BB by A10,A3,CARD_5:2;
c in Ball(z,r1) by Th13;
hence c in U & U c= f"].a,1.] by A4,A8,A9,Lm1,Th79,XBOOLE_0:def 4;
end;
suppose
A11: z`2 = 0;
then consider r1 being positive Real such that
r1 = (|.|[x,y]|-z.|-r*a)/2 and
A12: Ball(|[z`1,r1]|,r1) \/ {z} c= +(x,y,r)"].a,1.] by A4,A8,Th80;
reconsider U = Ball(|[z`1,r1]|,r1) \/ {z} as Subset of
Niemytzki-plane by A7,A11,Th27;
U in {Ball(|[z`1,q]|,q) \/ {|[z`1,0]|}
where q is Real: q > 0} by A7,A11;
then
A13: U in BB.(|[z`1,z`2]|) by A1,A11;
take U;
|[z`1,z`2]| in y>=0-plane by A11;
hence U in Union BB by A13,A3,CARD_5:2;
thus c in U by ZFMISC_1:136;
thus U c= f"].a,1.] by A12;
end;
end;
hence f"].a,1.] is open by YELLOW_9:31;
end;
hence thesis by Th75;
end;
end;
theorem Th81:
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)
proof
let U be Subset of Niemytzki-plane;
let x,y,r;
assume that
A1: y > 0 and
A2: U = Ball(|[x,y]|,r) /\ y>=0-plane;
reconsider y9 = y as positive Real by A1;
take f = +(x,y9,r);
|[x,y9]|`2 = y by EUCLID:52;
hence f.(|[x,y]|) = 0 by Th77;
let a,b be Real;
thus |[a,b]| in U` implies f.(|[a,b]|) = 1
proof
assume
A3: |[a,b]| in U`;
then not |[a,b]| in U by XBOOLE_0:def 5;
then
A4: not |[a,b]| in Ball(|[x,y]|,r) by A2,A3,Lm1,XBOOLE_0:def 4;
b >= 0 by A3,Lm1,Th18;
hence thesis by A4,Def6;
end;
assume
A5: |[a,b]| in U;
then
A6: |[a,b]| in Ball(|[x,y]|,r) by A2,XBOOLE_0:def 4;
b >= 0 by A5,Lm1,Th18;
hence thesis by A6,Def6;
end;
theorem Th82:
Niemytzki-plane is T_1
proof
set X = Niemytzki-plane;
let x,y be Point of X;
A1: the carrier of X = y>=0-plane by Def3;
then
A2: y in y>=0-plane;
x in y>=0-plane by A1;
then reconsider a = x, b = y as Point of TOP-REAL 2 by A2;
assume x <> y;
then |.a-b.| <> 0 by TOPRNS_1:28;
then reconsider r = |.a-b.| as positive Real;
consider q being Point of TOP-REAL 2, U being open Subset of X such that
A3: x in U and
q in U and
A4: for c being Point of TOP-REAL 2 st c in U holds |.c-q.| < r/2 by Th30;
consider p being Point of TOP-REAL 2, V being open Subset of X such that
A5: y in V and
p in V and
A6: for c being Point of TOP-REAL 2 st c in V holds |.c-p.| < r/2 by Th30;
take U,V;
thus U is open & V is open & x in U by A3;
hereby
assume y in U;
then |.b-q.| < r/2 by A4;
then
A7: |.a-q.|+|.b-q.| < (r/2)+r/2 by A3,A4,XREAL_1:8;
|.a-b.| <= |.a-q.|+|.q-b.| by TOPRNS_1:34;
hence contradiction by A7,TOPRNS_1:27;
end;
thus y in V by A5;
assume
A8: x in V;
A9: |.a-b.| <= |.a-p.|+|.p-b.| by TOPRNS_1:34;
|.b-p.| < r/2 by A5,A6;
then |.a-p.|+|.b-p.| < (r/2)+r/2 by A8,A6,XREAL_1:8;
hence contradiction by A9,TOPRNS_1:27;
end;
theorem
Niemytzki-plane is Tychonoff
proof
set X = Niemytzki-plane;
consider B being Neighborhood_System of X such that
A1: for x holds B.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is
Real: r > 0} and
A2: for x,y st y > 0 holds B.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane
where r is Real: r > 0} by Def3;
reconsider uB = Union B as prebasis of X by YELLOW_9:27;
A3: the carrier of X = y>=0-plane by Def3;
now
let x be Point of X;
let V be Subset of X;
assume that
A4: x in V and
A5: V in uB;
V is open by A5,TOPS_2:def 1;
then consider V9 being Subset of X such that
A6: V9 in B.x and
A7: V9 c= V by A4,YELLOW_8:def 1;
x in y>=0-plane by A3;
then reconsider x9 = x as Point of TOP-REAL 2;
A8: x = |[x9`1,x9`2]| by EUCLID:53;
per cases by A3,A8,Th18;
suppose
A9: x9`2 = 0;
then B.x = {Ball(|[x9`1,r]|,r) \/ {|[x9`1,0]|}
where r is Real: r > 0} by A1,A8;
then consider r being Real such that
A10: V9 = Ball(|[x9`1,r]|,r)\/{|[x9`1,0]|} and
A11: r > 0 by A6;
consider f being continuous Function of Niemytzki-plane, I[01] such that
A12: f.(|[x9`1,0]|) = 0 and
A13: for a,b being Real holds (|[a,b]| in V9` implies f.(|[a,
b]|) = 1) & (|[a,b]| in V9\{|[x9`1,0]|} implies f.(|[a,b]|) = |.|[x9`1,0]|-|[a,
b]|.| ^2/(2*r*b)) by A10,A11,Th76;
take f;
thus f.x = 0 by A9,A12,EUCLID:53;
thus f.:V` c= {1}
proof
let u be object;
assume u in f.:V`;
then consider b being Point of X such that
A14: b in V` and
A15: u = f.b by FUNCT_2:65;
b in y>=0-plane by A3;
then reconsider c = b as Element of TOP-REAL 2;
A16: V` c= V9` by A7,SUBSET_1:12;
b = |[c`1,c`2]| by EUCLID:53;
then u = 1 by A16,A14,A13,A15;
hence thesis by TARSKI:def 1;
end;
end;
suppose
A17: x9`2 > 0;
then B.x = {Ball(|[x9`1,x9`2]|,r) /\ y>=0-plane
where r is Real: r > 0} by A2,A8;
then consider r being Real such that
A18: V9 = Ball(|[x9`1,x9`2]|,r)/\y>=0-plane and
A19: r > 0 by A6;
consider f being continuous Function of Niemytzki-plane, I[01] such that
A20: f.(|[x9`1,x9`2]|) = 0 and
A21: for a,b being Real holds (|[a,b]| in V9` implies f.(|[a,
b]|) = 1) & (|[a,b]| in V9 implies f.(|[a,b]|) = |.|[x9`1,x9`2]|-|[a,b]|.|/r)
by A17,A18,A19,Th81;
take f;
thus f.x = 0 by A20,EUCLID:53;
thus f.:V` c= {1}
proof
let u be object;
assume u in f.:V`;
then consider b being Point of X such that
A22: b in V` and
A23: u = f.b by FUNCT_2:65;
b in y>=0-plane by A3;
then reconsider c = b as Element of TOP-REAL 2;
A24: V` c= V9` by A7,SUBSET_1:12;
b = |[c`1,c`2]| by EUCLID:53;
then u = 1 by A24,A22,A21,A23;
hence thesis by TARSKI:def 1;
end;
end;
end;
hence thesis by Th52,Th82;
end;