:: The {N}agata-Smirnov Theorem. {P}art {I}
:: by Karol P\c{a}k
::
:: Received May 31, 2004
:: Copyright (c) 2004-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, XBOOLE_0, PRE_TOPC, METRIC_1, REAL_1, XXREAL_0, CARD_1,
ARYTM_3, COMPLEX1, ARYTM_1, SETFAM_1, NATTRA_1, RCOMP_1, SUBSET_1,
STRUCT_0, TARSKI, ZFMISC_1, PCOMPS_1, FINSET_1, FUNCT_1, CARD_3,
FUNCOP_1, COMPTS_1, RELAT_1, ORDINAL1, RLVECT_3, CARD_5, NEWTON,
FINSEQ_1, PSCOMP_1, ORDINAL2, TOPMETR, TMAP_1, BINOP_1, FUNCT_2,
SETWISEO, COH_SP, FINSOP_1, NAT_1, RELAT_2, NAGATA_1, FUNCT_7;
notations BINOP_1, SETWISEO, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, ORDINAL1, COMPLEX1, RELSET_1, FUNCT_2, FINSEQ_1, ZFMISC_1,
PCOMPS_1, PRE_TOPC, FINSET_1, CARD_1, XCMPLX_0, NUMBERS, XXREAL_0,
XREAL_0, REAL_1, NAT_1, FINSOP_1, VALUED_1, STRUCT_0, TOPS_2, COMPTS_1,
METRIC_1, NEWTON, CARD_3, PROB_1, FUNCOP_1, CANTOR_1, DOMAIN_1, TOPMETR,
PSCOMP_1, BORSUK_1, TMAP_1;
constructors SETWISEO, REAL_1, PROB_1, FUNCOP_1, FINSOP_1, NEWTON, CARD_5,
TOPS_2, COMPTS_1, TMAP_1, CANTOR_1, PCOMPS_1, PSCOMP_1, URYSOHN3,
BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_LAR, STRUCT_0, TOPS_1, COMPTS_1,
METRIC_1, BORSUK_1, TOPMETR, PSCOMP_1, VALUED_0, VALUED_1, FUNCT_2,
CARD_3, FUNCT_1, PRE_TOPC, ZFMISC_1, BINOP_2, NEWTON, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions PCOMPS_1, TARSKI, BINOP_1;
equalities PCOMPS_1, BINOP_1, SUBSET_1, COMPTS_1, STRUCT_0;
expansions PCOMPS_1, TARSKI, COMPTS_1;
theorems FUNCT_1, FUNCT_2, METRIC_1, XREAL_0, XCMPLX_1, ABSVALUE, TOPMETR,
TMAP_1, CARD_1, PCOMPS_1, PCOMPS_2, BORSUK_1, XBOOLE_1, TARSKI, SETFAM_1,
XBOOLE_0, SUBSET_1, TOPS_1, TOPS_2, PRE_TOPC, CARD_3, URYSOHN1, NAT_1,
YELLOW_9, FINSEQ_1, FINSOP_1, SETWISEO, NEWTON, ZFMISC_1, BINOP_1, SEQ_2,
PROB_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, PREPOWER, ORDINAL1,
VALUED_1, JORDAN5A;
schemes FUNCT_1, FRAENKEL, FUNCT_2, NAT_1;
begin
reserve T, T1 for non empty TopSpace;
Lm1: for r,s,t be Real st r>=0 & s>=0 & r+s<t holds r<t & s<t
proof
let r,s,t be Real such that
A1: r>=0 & s>=0 and
A2: r+s<t;
assume r>=t or s>=t;
then r+s>=t+0 or s+r>=t+0 by A1,XREAL_1:7;
hence thesis by A2;
end;
Lm2: for r1,r2,r3,r4 being Real holds |.r1-r4.|<=|.r1-r2.|+|.r2-r3.| +|.r3
-r4.|
proof
let r1,r2,r3,r4 be Real;
r2-r4=(r2-r3)+(r3-r4);
then |.r2-r4.|<=|.r2-r3.|+|.r3-r4.| by COMPLEX1:56;
then
A1: |.r1-r2.|+|.r2-r4.|<=|.r1-r2.|+(|.r2-r3.|+|.r3-r4.|)by XREAL_1:7;
r1-r4=(r1-r2)+(r2-r4);
then |.r1-r4.|<=|.r1-r2.|+|.r2-r4.| by COMPLEX1:56;
hence thesis by A1,XXREAL_0:2;
end;
definition
let T be TopSpace;
let F be Subset-Family of T;
attr F is discrete means
:Def1:
for p being Point of T ex O being open
Subset of T st p in O & for A,B being Subset of T st A in F & B in F holds O
meets A & O meets B implies A=B;
end;
registration
let T be non empty TopSpace;
cluster discrete for Subset-Family of T;
existence
proof
set F={{},the carrier of T};
F c= bool the carrier of T
proof
let f be object;
reconsider ff=f as set by TARSKI:1;
assume f in F;
then f={} or f=the carrier of T by TARSKI:def 2;
then ff c= the carrier of T;
hence thesis;
end;
then reconsider F as Subset-Family of T;
take F;
let p be Point of T;
take O= [#]T;
thus p in O;
now
let A,B be Subset of T;
assume that
A1: A in F and
A2: B in F;
A3: B={} or B=the carrier of T by A2,TARSKI:def 2;
assume O meets A & O meets B;
then
A4: O/\A<>{} & O/\B<>{} by XBOOLE_0:def 7;
A={} or A=the carrier of T by A1,TARSKI:def 2;
hence A=B by A3,A4;
end;
hence thesis;
end;
end;
registration
let T;
cluster empty discrete for Subset-Family of T;
existence
proof
reconsider F={} as Subset-Family of T by XBOOLE_1:2;
take F;
thus F is empty;
let p be Point of T;
take [#]T;
thus thesis;
end;
end;
reserve F,G,H for Subset-Family of T,
A,B,C,D for Subset of T,
O,U for open Subset of T,
p,q for Point of T,
x,y,X for set;
theorem Th1:
for F st (ex A st F={A}) holds F is discrete
proof
let F;
assume ex A st F={A};
then consider A such that
A1: F={A};
now
let p;
take O= [#]T;
thus p in O;
now
let B,C;
assume that
A2: B in F and
A3: C in F;
{B}c={A} by A1,A2,ZFMISC_1:31;
then
A4: B=A by ZFMISC_1:3;
{C}c={A} by A1,A3,ZFMISC_1:31;
hence B=C by A4,ZFMISC_1:3;
end;
hence for B,C st B in F & C in F holds O meets B & O meets C implies B=C;
end;
hence thesis;
end;
theorem Th2:
for F,G st F c= G & G is discrete holds F is discrete
proof
let F,G be Subset-Family of T;
assume that
A1: F c= G and
A2: G is discrete;
now
let p;
thus ex O st p in O & for C,D st C in F & D in F holds O meets C & O
meets D implies C=D
proof
consider U such that
A3: p in U & for C,D st C in G & D in G holds U meets C & U meets D
implies C=D by A2;
take O=U;
thus thesis by A1,A3;
end;
hence
ex O st p in O & for C,D st C in F & D in F holds O meets C & O meets
D implies C=D;
end;
hence thesis;
end;
theorem
for F,G st F is discrete holds F/\G is discrete by Th2,XBOOLE_1:17;
theorem
for F,G st F is discrete holds F\G is discrete by Th2,XBOOLE_1:36;
theorem
for F,G,H st F is discrete & G is discrete & INTERSECTION(F,G)=H holds
H is discrete
proof
let F,G,H;
assume that
A1: F is discrete and
A2: G is discrete and
A3: INTERSECTION(F,G)=H;
now
let p;
consider O such that
A4: p in O and
A5: for A,B being Subset of T st A in F & B in F holds O meets A & O
meets B implies A=B by A1;
consider U such that
A6: p in U and
A7: for A,B being Subset of T st A in G & B in G holds U meets A & U
meets B implies A=B by A2;
A8: now
let A,B;
assume that
A9: A in INTERSECTION(F,G) and
A10: B in INTERSECTION(F,G);
consider af,ag being set such that
A11: af in F and
A12: ag in G and
A13: A=af/\ag by A9,SETFAM_1:def 5;
assume that
A14: (O/\U) meets A and
A15: (O/\U) meets B;
consider bf,bg being set such that
A16: bf in F and
A17: bg in G and
A18: B=bf/\bg by A10,SETFAM_1:def 5;
(O/\U)/\(bf/\bg)<>{} by A18,A15,XBOOLE_0:def 7;
then (O/\U/\bf) /\bg <>{} by XBOOLE_1:16;
then
A19: (O/\bf/\U)/\bg<>{} by XBOOLE_1:16;
then O/\bf <>{};
then
A20: O meets bf by XBOOLE_0:def 7;
(O/\U)/\(af/\ag)<>{} by A13,A14,XBOOLE_0:def 7;
then (O/\U/\af)/\ag<>{} by XBOOLE_1:16;
then
A21: (O/\af/\U)/\ag <> {} by XBOOLE_1:16;
then (O/\af)/\(U/\ag) <> {} by XBOOLE_1:16;
then U/\ag <> {};
then
A22: U meets ag by XBOOLE_0:def 7;
(O/\bf)/\(U/\bg)<>{} by A19,XBOOLE_1:16;
then U/\bg <>{};
then
A23: U meets bg by XBOOLE_0:def 7;
O/\af <>{} by A21;
then O meets af by XBOOLE_0:def 7;
then af=bf by A5,A11,A16,A20;
hence A=B by A7,A12,A13,A17,A18,A22,A23;
end;
set Q=O/\U;
p in Q by A4,A6,XBOOLE_0:def 4;
hence ex Q being open Subset of T st p in Q & for A,B being Subset of T st
A in H & B in H holds Q meets A & Q meets B implies A=B by A3,A8;
end;
hence thesis;
end;
theorem Th6:
for F,A,B st F is discrete & A in F & B in F holds A=B or A misses B
proof
let F,A,B;
assume that
A1: F is discrete and
A2: A in F & B in F;
assume that
A3: A<>B and
A4: A meets B;
A/\B <> {}T by A4,XBOOLE_0:def 7;
then consider p such that
A5: p in (A /\ B) by PRE_TOPC:12;
consider O such that
A6: p in O and
A7: for C,D st C in F & D in F holds O meets C & O meets D implies C=D
by A1;
A8: {p}c=O by A6,ZFMISC_1:31;
p in B by A5,XBOOLE_0:def 4;
then {p} c= B by ZFMISC_1:31;
then {p} c=O/\B by A8,XBOOLE_1:19;
then
A9: p in O/\B by ZFMISC_1:31;
p in A by A5,XBOOLE_0:def 4;
then {p}c=A by ZFMISC_1:31;
then {p}c=O/\A by A8,XBOOLE_1:19;
then
A10: p in O/\A by ZFMISC_1:31;
O meets A & O meets B implies A=B by A2,A7;
hence contradiction by A3,A10,A9,XBOOLE_0:4;
end;
theorem Th7:
F is discrete implies for p ex O st p in O & INTERSECTION({O},F)\
{{}} is trivial
proof
assume
A1: F is discrete;
let p;
consider O such that
A2: p in O and
A3: for C,D st C in F & D in F holds O meets C & O meets D implies C=D
by A1;
set I=INTERSECTION({O},F);
A4: for f,g being set st f in I & g in I holds f=g or f={} or g={}
proof
let f,g be set;
assume that
A5: f in I and
A6: g in I;
consider o1,f1 being set such that
A7: o1 in {O} and
A8: f1 in F and
A9: f= o1 /\ f1 by A5,SETFAM_1:def 5;
consider o2,g1 being set such that
A10: o2 in {O} and
A11: g1 in F and
A12: g= o2 /\ g1 by A6,SETFAM_1:def 5;
{o2}c={O} by A10,ZFMISC_1:31;
then
A13: o2=O by ZFMISC_1:3;
{o1}c={O} by A7,ZFMISC_1:31;
then
A14: o1=O by ZFMISC_1:3;
then O meets f1 & O meets g1 or f={} or g={} by A9,A12,A13,XBOOLE_0:def 7;
hence thesis by A3,A8,A9,A11,A12,A14,A13;
end;
A15: for f being set st f<>{} & f in I holds I c={{},f}
proof
let f be set;
assume
A16: f<>{} & f in I;
now
let g be object;
assume g in I;
then f=g or g={} by A4,A16;
hence g in {{},f} by TARSKI:def 2;
end;
hence thesis;
end;
now
per cases;
suppose
I\{{}}<>{};
then consider f being object such that
A17: f in I\{{}} by XBOOLE_0:def 1;
f <>{} by A17,ZFMISC_1:56;
then
A18: I c={{},f} by A15,A17;
now
let g be object;
assume g in I;
then {g} c={{},f} by A18,ZFMISC_1:31;
then g={} or g =f by ZFMISC_1:19;
then g in {{}} or g in {f} by ZFMISC_1:31;
hence g in {{}}\/{f} by XBOOLE_0:def 3;
end;
then I c= {{}}\/{f};
then I\{{}}c={f} by XBOOLE_1:43;
then I\{{}}={} or I\{{}}={f} by ZFMISC_1:33;
hence I\{{}} is trivial;
end;
suppose
I\{{}}={};
hence I\{{}} is trivial;
end;
end;
hence thesis by A2;
end;
theorem
F is discrete iff (for p ex O st p in O & INTERSECTION({O},F)\{{}} is
trivial) & for A,B st A in F & B in F holds A=B or A misses B
proof
now
let F;
(for p ex O st p in O & INTERSECTION({O},F)\{{}} is trivial) & (for A,
B st A in F & B in F holds A=B or A misses B) implies F is discrete
proof
assume that
A1: for p ex O st p in O & INTERSECTION({O},F)\{{}} is trivial and
A2: for A,B st A in F & B in F holds A=B or A misses B;
assume not F is discrete;
then consider p such that
A3: for O holds not p in O or not (for A,B st A in F & B in F holds
O meets A & O meets B implies A=B);
consider O such that
A4: p in O and
A5: INTERSECTION({O},F)\{{}} is trivial by A1;
consider A,B such that
A6: A in F and
A7: B in F and
A8: O meets A and
A9: O meets B and
A10: A<>B by A3,A4;
A11: O/\B<>{} by A9,XBOOLE_0:def 7;
set I=INTERSECTION({O},F);
consider a being object such that
A12: I\{{}}={} or I\{{}}={a} by A5,ZFMISC_1:131;
A13: O in {O} by ZFMISC_1:31;
then O/\B in I by A7,SETFAM_1:def 5;
then O/\B in I\{{}} by A11,ZFMISC_1:56;
then {O/\B} c= {a} by A12,ZFMISC_1:31;
then
A14: O/\B=a by ZFMISC_1:3;
A15: O/\A<>{} by A8,XBOOLE_0:def 7;
then consider f being object such that
A16: f in O/\A by XBOOLE_0:def 1;
A17: f in A by A16,XBOOLE_0:def 4;
O/\A in I by A6,A13,SETFAM_1:def 5;
then O/\A in I\{{}} by A15,ZFMISC_1:56;
then {O/\A}c={a} by A12,ZFMISC_1:31;
then O/\A=a by ZFMISC_1:3;
then f in B by A14,A16,XBOOLE_0:def 4;
then
A18: f in A/\B by A17,XBOOLE_0:def 4;
A misses B by A2,A6,A7,A10;
hence thesis by A18,XBOOLE_0:def 7;
end;
hence
F is discrete iff (for p ex O st p in O & INTERSECTION({O},F)\{{}} is
trivial)& for A,B st A in F & B in F holds A=B or A misses B by Th6,Th7;
end;
hence thesis;
end;
Lm3: for O,A holds O meets Cl A implies O meets A
proof
let O,A;
O misses A implies O misses Cl A
proof
assume O misses A;
then A c= O` by SUBSET_1:23;
then Cl A c=O` by TOPS_1:5;
hence thesis by SUBSET_1:23;
end;
hence thesis;
end;
registration
let T;
let F be discrete Subset-Family of T;
cluster clf F -> discrete;
coherence
proof
thus clf F is discrete
proof
let p;
consider O such that
A1: p in O and
A2: for A,B st A in F & B in F holds O meets A & O meets B implies A
=B by Def1;
now
let A,B;
assume that
A3: A in clf F and
A4: B in clf F;
consider C such that
A5: A = Cl C and
A6: C in F by A3,PCOMPS_1:def 2;
assume that
A7: O meets A and
A8: O meets B;
consider D such that
A9: B = Cl D and
A10: D in F by A4,PCOMPS_1:def 2;
A11: O meets D by A9,A8,Lm3;
O meets C by A5,A7,Lm3;
hence A=B by A2,A5,A6,A9,A10,A11;
end;
hence thesis by A1;
end;
end;
end;
Lm4: for F for A st A in F holds Cl A c= Cl union F
proof
let F;
let A;
assume A in F;
then for f being object st f in A holds f in union F by TARSKI:def 4;
then A c= union F;
hence thesis by PRE_TOPC:19;
end;
theorem
for F st F is discrete holds for A,B st A in F & B in F holds Cl(A/\B)
=Cl A /\ Cl B
proof
let F such that
A1: F is discrete;
let A,B such that
A2: A in F & B in F;
now
per cases by A1,A2,Th6;
suppose
A misses B;
then
A3: A/\B ={}T by XBOOLE_0:def 7;
(Cl A /\ Cl B)={}
proof
assume (Cl A /\ Cl B)<>{};
then consider x being object such that
A4: x in (Cl A /\ Cl B) by XBOOLE_0:def 1;
consider O such that
A5: x in O and
A6: for A,B st A in F & B in F holds O meets A & O meets B
implies A=B by A1,A4;
x in Cl A by A4,XBOOLE_0:def 4;
then
A7: O meets A by A5,PRE_TOPC:def 7;
x in Cl B by A4,XBOOLE_0:def 4;
then O meets B by A5,PRE_TOPC:def 7;
then A=B by A2,A6,A7;
hence thesis by A3,A7,XBOOLE_1:65;
end;
hence thesis by A3,PRE_TOPC:22;
end;
suppose
A=B;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for F st F is discrete holds Cl union(F) = union (clf F)
proof
let F;
assume
A1: F is discrete;
A2: Cl union(F) c= union (clf F)
proof
let x be object;
assume
A3: x in Cl union(F);
then consider O such that
A4: x in O and
A5: for A,B st A in F & B in F holds O meets A & O meets B implies A=
B by A1;
not O misses union(F) by A3,A4,PRE_TOPC:def 7;
then consider f being object such that
A6: f in O and
A7: f in union(F) by XBOOLE_0:3;
consider AF being set such that
A8: f in AF and
A9: AF in F by A7,TARSKI:def 4;
reconsider AF as Subset of T by A9;
A10: O meets AF by A6,A8,XBOOLE_0:3;
for D st D is open & x in D holds not D misses AF
proof
assume ex D st D is open & x in D & D misses AF;
then consider D such that
A11: D is open and
A12: x in D and
A13: D misses AF;
x in D/\O by A4,A12,XBOOLE_0:def 4;
then (D/\O) meets union(F) by A3,A11,PRE_TOPC:def 7;
then consider y being object such that
A14: y in (D/\O) and
A15: y in union(F) by XBOOLE_0:3;
consider BF being set such that
A16: y in BF and
A17: BF in F by A15,TARSKI:def 4;
y in D by A14,XBOOLE_0:def 4;
then y in D/\BF by A16,XBOOLE_0:def 4;
then
A18: D meets BF by XBOOLE_0:def 7;
y in O by A14,XBOOLE_0:def 4;
then y in O/\BF by A16,XBOOLE_0:def 4;
then O meets BF by XBOOLE_0:def 7;
hence contradiction by A5,A9,A10,A13,A17,A18;
end;
then
A19: x in Cl AF by A3,PRE_TOPC:def 7;
Cl AF in clf F by A9,PCOMPS_1:def 2;
hence thesis by A19,TARSKI:def 4;
end;
union (clf F)c=Cl union(F)
proof
let f be object;
assume f in union (clf F);
then consider Af being set such that
A20: f in Af and
A21: Af in clf F by TARSKI:def 4;
reconsider Af as Subset of T by A21;
ex A st Cl A =Af & A in F by A21,PCOMPS_1:def 2;
then Af c= Cl union F by Lm4;
hence thesis by A20;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th11:
for F st F is discrete holds F is locally_finite
proof
let F;
assume
A1: F is discrete;
for p ex A st p in A & A is open & { D: D in F & D meets A} is finite
proof
let p;
consider U such that
A2: p in U and
A3: for A,B st A in F & B in F holds U meets A & U meets B implies A=B
by A1;
set SF={ D: D in F & D meets U };
take O=U;
SF<>{} implies ex A st SF={A}
proof
assume SF<>{};
then consider a being object such that
A4: a in SF by XBOOLE_0:def 1;
consider D such that
A5: a=D and
A6: D in F & D meets O by A4;
now
let b be object;
assume b in SF;
then ex C st b=C & C in F & C meets O;
then b=D by A3,A6;
hence b in {D} by TARSKI:def 1;
end;
then
A7: SF c= {D};
{D} c=SF by A4,A5,ZFMISC_1:31;
then SF={D} by A7,XBOOLE_0:def 10;
hence thesis;
end;
hence thesis by A2;
end;
hence thesis;
end;
definition
let T be TopSpace;
mode FamilySequence of T
is sequence of bool bool(the carrier of T) qua non empty set;
end;
reserve Un for FamilySequence of T,
r,r1,r2 for Real,
n for Element of NAT;
definition
let T,Un,n;
redefine func Un.n -> Subset-Family of T; :: redefines . (FUNCT_1, definition)
coherence
proof
Un.n c= bool(the carrier of T);
hence thesis;
end;
end;
definition
let T,Un;
redefine func Union Un ->Subset-Family of T; :: redefines Union (CARD_3, definition)
coherence
proof
Union Un c= bool(the carrier of T);
hence thesis;
end;
end;
definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
attr Un is sigma_discrete means
:Def2:
for n being Element of NAT holds Un.n is discrete;
end;
Lm5: ex Un being FamilySequence of T st Un is sigma_discrete
proof
set C={the carrier of T};
the carrier of T in bool the carrier of T by ZFMISC_1:def 1;
then C c= bool the carrier of T by ZFMISC_1:31;
then reconsider
f = NAT --> C as sequence of bool bool the carrier of T by FUNCOP_1:45;
take f;
now
let n;
the carrier of T is Subset of T by ZFMISC_1:def 1;
hence f.n is discrete by Th1,FUNCOP_1:7;
end;
hence thesis;
end;
registration
let T be non empty TopSpace;
cluster sigma_discrete for FamilySequence of T;
existence by Lm5;
end;
definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
attr Un is sigma_locally_finite means
for n being Element of NAT holds Un.n is locally_finite;
end;
definition
let T;
let F be Subset-Family of T;
attr F is sigma_discrete means
ex f being sigma_discrete FamilySequence of T st F = Union f;
end;
registration
let T be non empty TopSpace;
cluster sigma_locally_finite for FamilySequence of T;
existence
proof
thus ex Un being FamilySequence of T st Un is sigma_locally_finite
proof
consider Un being FamilySequence of T such that
A1: Un is sigma_discrete by Lm5;
take Un;
for n holds Un.n is locally_finite by Th11,A1;
hence thesis;
end;
end;
end;
theorem
for Un st Un is sigma_discrete holds Un is sigma_locally_finite
by Th11;
theorem
for A being uncountable set ex F being Subset-Family of 1TopSp([:A,A:]
) st F is locally_finite & F is not sigma_discrete
proof
let A be uncountable set;
set TS=1TopSp([:A,A:]);
set F = {[:{a},A:] \/ [:A,{a}:] where a is Element of A: a in A};
F c= bool [:A,A:]
proof
let f be object;
assume f in F;
then consider a being Element of A such that
A1: f = [:{a},A:] \/ [:A,{a}:] and
a in A;
[:{a},A:] c=[:A,A:] & [:A,{a}:] c= [:A,A:] by ZFMISC_1:96;
then [:{a},A:] \/ [:A,{a}:] c= [:A,A:] by XBOOLE_1:8;
hence thesis by A1;
end;
then reconsider F as Subset-Family of TS;
take F;
for z being Point of TS ex Z being Subset of TS st z in Z & Z is open &
{O where O is Subset of TS: O in F & O meets Z } is finite
proof
let z be Point of TS;
set Z={z};
reconsider Z as Subset of TS;
consider x,y being object such that
x in A and
y in A and
A2: z=[x,y] by ZFMISC_1:def 2;
set yAAy={[:{y},A:]\/[:A,{y}:]};
set xAAx={[:{x},A:]\/[:A,{x}:]};
set UZ={O where O is Subset of TS: O in F & O meets Z };
A3: UZ c= xAAx \/ yAAy
proof
let U be object;
assume U in UZ;
then consider O being Subset of TS such that
A4: U=O and
A5: O in F and
A6: O meets Z;
consider u being object such that
A7: u in O and
A8: u in Z by A6,XBOOLE_0:3;
consider a being Element of A such that
A9: O=[:{a},A:] \/ [:A,{a}:] and
a in A by A5;
now
per cases by A9,A7,XBOOLE_0:def 3;
suppose
u in [:{a},A:];
then [x,y] in [:{a},A:] by A2,A8,TARSKI:def 1;
then x in {a} by ZFMISC_1:87;
then x=a by TARSKI:def 1;
then O in xAAx by A9,TARSKI:def 1;
hence O in xAAx \/ yAAy by XBOOLE_0:def 3;
end;
suppose
u in [:A,{a}:];
then [x,y] in [:A,{a}:] by A2,A8,TARSKI:def 1;
then y in {a} by ZFMISC_1:87;
then y=a by TARSKI:def 1;
then O in yAAy by A9,TARSKI:def 1;
hence O in xAAx \/ yAAy by XBOOLE_0:def 3;
end;
end;
hence thesis by A4;
end;
z in Z & Z is open by PRE_TOPC:def 2,ZFMISC_1:31;
hence thesis by A3;
end;
hence F is locally_finite;
F is not sigma_discrete
proof
consider a being object such that
A10: a in A by XBOOLE_0:def 1;
reconsider a as Element of A by A10;
set aAAa=[:{a},A:]\/[:A,{a}:];
A11: card A c= card F
proof
deffunc D(object)=[:{$1},A:]\/[:A,{$1}:];
consider d being Function such that
A12: dom d = A & for x being object st x in A holds d.x = D(x) from
FUNCT_1:sch 3;
for a1,a2 being object st a1 in dom d & a2 in dom d & d.a1=d.a2
holds a1= a2
proof
let a1,a2 be object;
assume that
A13: a1 in dom d and
A14: a2 in dom d and
A15: d.a1=d.a2;
a1 in {a1} by ZFMISC_1:31;
then
A16: [a1,a1] in [:{a1},A:] by A12,A13,ZFMISC_1:87;
D(a1)=d.a1 & D(a2)=d.a2 by A12,A13,A14;
then [a1,a1] in [:{a2},A:]\/[:A,{a2}:] by A15,A16,XBOOLE_0:def 3;
then [a1,a1] in [:{a2},A:] or [a1,a1] in [:A,{a2}:] by XBOOLE_0:def 3;
then
A17: a1 in {a2} by ZFMISC_1:87;
assume a1<>a2;
hence thesis by A17,TARSKI:def 1;
end;
then
A18: d is one-to-one by FUNCT_1:def 4;
rng d c= F
proof
let AA be object;
assume AA in rng d;
then consider a being object such that
A19: a in dom d and
A20: AA = d.a by FUNCT_1:def 3;
reconsider a as Element of A by A12,A19;
AA=[:{a},A:]\/[:A,{a}:] by A12,A20;
hence thesis;
end;
hence thesis by A12,A18,CARD_1:10;
end;
assume F is sigma_discrete;
then consider f being sigma_discrete FamilySequence of TS such that
A21: F = Union f;
defpred F1[object,object] means
($2 in f.$1 & f.$1 is non empty )or($2=aAAa & f.
$1 is empty);
A22: for k being object st k in NAT ex f being object st f in F & F1[k,f]
proof
let k be object;
assume k in NAT;
then reconsider k as Element of NAT;
now
per cases;
suppose
A23: f.k is empty;
aAAa in F;
hence ex A being set st A in F & F1[k,A] by A23;
end;
suppose
f.k is non empty;
then consider A being object such that
A24: A in f.k by XBOOLE_0:def 1;
A in F by A21,A24,PROB_1:12;
hence ex A being set st A in F & F1[k,A] by A24;
end;
end;
hence thesis;
end;
consider Df being sequence of F such that
A25: for k being object st k in NAT holds F1[k,Df.k] from FUNCT_2:sch 1(
A22 );
A26: for n being Element of NAT,AD,BD being Element of F st F1[n,AD] & F1[
n,BD] holds AD=BD
proof
let n be Element of NAT,AD,BD be Element of F;
assume that
A27: F1[n,AD] and
A28: F1[n,BD];
now
A29: f.n is discrete by Def2;
BD in F by A21,A28,PROB_1:12;
then consider b being Element of A such that
A30: BD=[:{b},A:] \/ [:A,{b}:] and
b in A;
AD in F by A21,A27,PROB_1:12;
then consider a being Element of A such that
A31: AD=[:{a},A:] \/ [:A,{a}:] and
a in A;
b in {b} by TARSKI:def 1;
then [a,b] in [:A,{b}:] by ZFMISC_1:87;
then
A32: [a,b] in BD by A30,XBOOLE_0:def 3;
a in {a} by TARSKI:def 1;
then [a,b] in[:{a},A:] by ZFMISC_1:87;
then [a,b] in AD by A31,XBOOLE_0:def 3;
then AD meets BD by A32,XBOOLE_0:3;
hence thesis by A27,A28,A29,Th6;
end;
hence thesis;
end;
A33: F c=Df.:NAT
proof
let cAAc be object;
assume
A34: cAAc in F;
then consider k being Nat such that
A35: cAAc in f.k by A21,PROB_1:12;
A36: k in NAT by ORDINAL1:def 12;
F1[k,Df.k] by A25,A36;
then
A37: cAAc =Df.k by A26,A34,A35,A36;
dom Df = NAT by A34,FUNCT_2:def 1;
hence thesis by A37,FUNCT_1:def 6,A36;
end;
A38: not card A c= omega by CARD_3:def 14;
then card NAT in card A by CARD_1:4,47;
then card NAT c= card F by A11,CARD_1:3;
then card NAT c< card F by A11,A38,CARD_1:47,XBOOLE_0:def 8;
then
A39: card (Df.:NAT) c< card F by CARD_1:67,XBOOLE_1:59;
then card (Df.:NAT)c=card F by XBOOLE_0:def 8;
then card (Df.:NAT) in card F by A39,CARD_1:3;
then F\(Df.:NAT)<>{} by CARD_1:68;
hence contradiction by A33,XBOOLE_1:37;
end;
hence thesis;
end;
definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
attr Un is Basis_sigma_discrete means
Un is sigma_discrete & Union Un is Basis of T;
end;
definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
attr Un is Basis_sigma_locally_finite means
Un is sigma_locally_finite & Union Un is Basis of T;
end;
theorem Th14:
for r being Real, PM be non empty MetrSpace for x being
Element of PM holds [#]PM\cl_Ball(x,r) in Family_open_set(PM)
proof
let r be Real;
reconsider r9=r as Real;
let PM be non empty MetrSpace;
let x be Element of PM;
now
let y be Element of PM;
set r1=dist(x,y)-r9;
A1: Ball(y,r1) c= [#]PM\cl_Ball(x,r)
proof
assume not Ball(y,r1) c= [#]PM\cl_Ball(x,r);
then consider z being object such that
A2: z in Ball(y,r1) and
A3: not z in [#]PM\cl_Ball(x,r);
reconsider z as Element of PM by A2;
not (z in [#]PM & not z in cl_Ball(x,r)) by A3,XBOOLE_0:def 5;
then
A4: dist(x,z)<=r9 by METRIC_1:12;
dist(y,z)<r1 by A2,METRIC_1:11;
then dist(y,z) + dist(x,z)< r1 + r9 by A4,XREAL_1:8;
then dist(x,z)+dist(z,y)< r1 + r9;
hence thesis by METRIC_1:4;
end;
assume y in [#]PM\cl_Ball(x,r);
then not y in cl_Ball(x,r) by XBOOLE_0:def 5;
then r9+0<r9+r1 by METRIC_1:12;
then r9-r9<r1-0 by XREAL_1:21;
hence ex r2 st r2>0 & Ball(y,r2) c= [#]PM\cl_Ball(x,r) by A1;
end;
hence thesis by PCOMPS_1:def 4;
end;
theorem
for T st T is metrizable holds T is regular & T is T_1
proof
let T;
assume T is metrizable;
then consider
metr being Function of [:the carrier of T,the carrier of T:],REAL
such that
A1: metr is_metric_of (the carrier of T) and
A2: Family_open_set( SpaceMetr (the carrier of T,metr)) = the topology
of T;
set PM = SpaceMetr(the carrier of T,metr);
reconsider PM as non empty MetrSpace by A1,PCOMPS_1:36;
set TPM = TopSpaceMetr PM;
A3: for p being Element of T for D being Subset of T st D <> {} & D is
closed & p in D` ex A,B being Subset of T st A is open & B is open & p in A & D
c= B & A misses B
proof
let p be Element of T;
let D be Subset of T;
assume that
D<>{} and
A4: D is closed and
A5: p in D`;
A6: [#]T\D in the topology of T by A4,A5,PRE_TOPC:def 2;
reconsider p as Element of PM by A1,PCOMPS_2:4;
A7: D misses D` by XBOOLE_1:79;
reconsider D as Subset of TPM by A1,PCOMPS_2:4;
[#]TPM\D in Family_open_set(PM) by A1,A2,A6,PCOMPS_2:4;
then [#]TPM\D is open by PRE_TOPC:def 2;
then
A8: D is closed by PRE_TOPC:def 3;
A9: not p in D by A5,A7,XBOOLE_0:3;
ex r1 st r1>0 & Ball(p,r1) misses D
proof
assume
A10: for r1 st r1>0 holds Ball(p,r1) meets D;
now
let A be Subset of TPM;
assume that
A11: A is open and
A12: p in A;
A in Family_open_set(PM) by A11,PRE_TOPC:def 2;
then consider r2 such that
A13: r2>0 and
A14: Ball(p,r2) c= A by A12,PCOMPS_1:def 4;
Ball(p,r2) meets D by A10,A13;
then ex x being object st x in Ball(p,r2) & x in D by XBOOLE_0:3;
hence A meets D by A14,XBOOLE_0:3;
end;
then p in Cl D by PRE_TOPC:def 7;
hence thesis by A8,A9,PRE_TOPC:22;
end;
then consider r1 such that
A15: r1>0 and
A16: Ball(p,r1) misses D;
set r2=r1/2;
A17: r2<r2+r2 by A15,XREAL_1:29;
A18: D c= [#]PM\cl_Ball(p,r2)
proof
assume not D c= [#]PM\cl_Ball(p,r2);
then consider x being object such that
A19: x in D and
A20: not x in [#]PM\cl_Ball(p,r2);
reconsider x as Element of PM by A19;
x in cl_Ball(p,r2) by A20,XBOOLE_0:def 5;
then dist(p,x) <= r2 by METRIC_1:12;
then dist(p,x) < r1 by A17,XXREAL_0:2;
then x in Ball(p,r1) by METRIC_1:11;
hence thesis by A16,A19,XBOOLE_0:3;
end;
set r4=r2/2;
A21: r2 > 0 by A15,XREAL_1:139;
then
A22: r4 < r4+r4 by XREAL_1:29;
A23: Ball(p,r4) misses [#]PM\cl_Ball(p,r2)
proof
assume Ball(p,r4) meets [#]PM\cl_Ball(p,r2);
then consider x being object such that
A24: x in Ball(p,r4) and
A25: x in [#]PM\cl_Ball(p,r2) by XBOOLE_0:3;
reconsider x as Element of PM by A24;
not x in cl_Ball(p,r2) by A25,XBOOLE_0:def 5;
then
A26: dist(p,x)>r2 by METRIC_1:12;
dist(p,x)<r4 by A24,METRIC_1:11;
hence thesis by A22,A26,XXREAL_0:2;
end;
set A=Ball(p,r4);
set B = [#]PM\cl_Ball(p,r2);
A27: B in Family_open_set(PM) & A in Family_open_set(PM) by Th14,PCOMPS_1:29;
then reconsider A,B as Subset of T by A2;
take A,B;
r4>0 by A21,XREAL_1:139;
then dist(p,p)<r4 by METRIC_1:1;
hence thesis by A2,A18,A23,A27,METRIC_1:11,PRE_TOPC:def 2;
end;
for p,q being Point of T st not p = q ex A,B being Subset of T st A is
open & B is open & p in A & not q in A & q in B & not p in B
proof
let p,q be Point of T;
assume
A28: not p=q;
reconsider p,q as Element of TPM by A1,PCOMPS_2:4;
TPM is T_2 by PCOMPS_1:34;
then consider A,B being Subset of TPM such that
A29: A is open and
A30: B is open and
A31: p in A & q in B and
A32: A misses B by A28,PRE_TOPC:def 10;
reconsider A,B as Subset of T by A1,PCOMPS_2:4;
A in the topology of T by A2,A29,PRE_TOPC:def 2;
then
A33: A is open by PRE_TOPC:def 2;
B in the topology of T by A2,A30,PRE_TOPC:def 2;
then
A34: B is open by PRE_TOPC:def 2;
( not q in A)& not p in B by A31,A32,XBOOLE_0:3;
hence thesis by A31,A33,A34;
end;
hence thesis by A3,URYSOHN1:def 7;
end;
theorem
for T st T is metrizable ex Un being FamilySequence of T st Un is
Basis_sigma_locally_finite
proof
let T;
assume
A1: T is metrizable;
then consider
metr being Function of [:the carrier of T,the carrier of T:],REAL
such that
A2: metr is_metric_of (the carrier of T) and
A3: Family_open_set( SpaceMetr (the carrier of T,metr)) = the topology
of T;
set PM = SpaceMetr(the carrier of T,metr);
reconsider PM as non empty MetrSpace by A2,PCOMPS_1:36;
deffunc BALL(Element of NAT)={Ball(x, 1/(2 |^ $1)) where x is Element of PM:
x is Element of PM};
defpred E[Element of NAT,set] means $2 = BALL($1);
A4: for k being Element of NAT ex y being Subset-Family of T st E[k,y]
proof
let k be Element of NAT;
set Ak=BALL(k);
Ak c= bool the carrier of T
proof
let B be object;
assume B in Ak;
then
ex x being Element of PM st B=Ball(x,1/(2 |^ k)) & x is Element of PM;
then B in Family_open_set(PM) by PCOMPS_1:29;
hence thesis by A3;
end;
hence thesis;
end;
consider FB being sequence of bool bool (the carrier of T) such that
A5: for k being Element of NAT holds E[k,FB.k] from FUNCT_2:sch 3(A4);
defpred P[object,object] means
ex W being Subset-Family of T st W = $2 & W is open
& W is Cover of T & W is_finer_than FB.$1 & W is locally_finite;
set TPM = TopSpaceMetr PM;
A6: [#]T=[#]TPM by A2,PCOMPS_2:4;
A7: for n ex PP being Subset-Family of T st PP is_finer_than FB.n & PP is
Cover of T & PP is open & PP is locally_finite
proof
let n;
[#]TPM c= union (FB.n)
proof
let x be object;
assume x in [#]TPM;
then reconsider x9=x as Element of PM;
dist(x9,x9) = 0 & 2|^n > 0 by METRIC_1:1,NEWTON:83;
then dist(x9,x9)<1/(2|^n) by XREAL_1:139;
then
A8: x9 in Ball(x9,1/(2|^ n)) by METRIC_1:11;
Ball(x9,1/(2|^ n)) in BALL(n);
then Ball(x9,1/(2|^ n)) in FB.n by A5;
hence thesis by A8,TARSKI:def 4;
end;
then
A9: FB.n is Cover of T by A6,SETFAM_1:def 11;
for U being Subset of T holds U in (FB.n) implies U is open
proof
let U be Subset of T;
assume U in (FB.n);
then U in BALL(n) by A5;
then ex x being Element of PM st U = Ball(x,1/(2|^ n)) & x is Element of
PM;
then U in the topology of T by A3,PCOMPS_1:29;
hence thesis by PRE_TOPC:def 2;
end;
then (FB.n) is open by TOPS_2:def 1;
then ex PP being Subset-Family of T st PP is open & PP is Cover of T & PP
is_finer_than (FB.n) & PP is locally_finite by A1,A9,PCOMPS_2:6;
hence thesis;
end;
A10: for k being object st k in NAT
ex y being object st y in bool bool the carrier of T & P[k,y]
proof
let k be object;
assume k in NAT;
then reconsider k as Element of NAT;
ex PP being Subset-Family of T st PP is_finer_than FB.k & PP is Cover
of T & PP is open & PP is locally_finite by A7;
hence thesis;
end;
consider UC being FamilySequence of T such that
A11: for x being object st x in NAT holds P[x,UC.x] from FUNCT_2:sch 1(A10);
A12: for A being Subset of T st A is open for p being Point of T st p in A
ex B being Subset of T st B in Union UC & p in B & B c= A
proof
let A;
assume A is open;
then
A13: A in Family_open_set(PM) by A3,PRE_TOPC:def 2;
let p;
assume
A14: p in A;
then reconsider p as Element of PM by A13;
consider r1 such that
A15: r1>0 and
A16: Ball(p,r1) c=A by A14,A13,PCOMPS_1:def 4;
consider n being Nat such that
A17: 1/(2|^ n)<=r1 by A15,PREPOWER:92;
A18: P[n+1,UC.(n+1)] by A11;
then union (UC.(n+1)) = the carrier of T by SETFAM_1:45;
then consider B being set such that
A19: p in B and
A20: B in (UC.(n+1)) by TARSKI:def 4;
reconsider B as Subset of PM by A2,A20,PCOMPS_2:4;
consider B1 being set such that
A21: B1 in FB.(n+1) and
A22: B c= B1 by A18,A20,SETFAM_1:def 2;
B1 in BALL(n+1) by A5,A21;
then consider q being Element of PM such that
A23: B1=Ball(q,(1/(2|^(n+1)))) and
q is Element of PM;
A24: dist(q,p)<1/(2|^(n+1)) by A19,A22,A23,METRIC_1:11;
now
let r be Element of PM;
assume r in B;
then dist(q,r)<1/(2|^(n+1)) by A22,A23,METRIC_1:11;
then
dist(p,r)<=dist(q,p)+dist(q,r) & dist(q,p)+dist(q,r)<1/(2|^(n+1))+1
/(2|^(n+1 )) by A24,METRIC_1:4,XREAL_1:8;
then dist(p,r)<2*(1/(2|^(n+1))) by XXREAL_0:2;
then dist(p,r)<(1/(2|^n * 2))*2 by NEWTON:6;
then dist(p,r)<(1/(2|^n)) by XCMPLX_1:92;
then dist(p,r)<r1 by A17,XXREAL_0:2;
hence r in Ball(p,r1) by METRIC_1:11;
end;
then
A25: B c= Ball(p,r1);
B in Union UC by A20,PROB_1:12;
hence thesis by A16,A19,A25,XBOOLE_1:1;
end;
for n holds UC.n is locally_finite
proof
let n;
P[n,UC.n] by A11;
hence thesis;
end;
then
A26: UC is sigma_locally_finite;
Union UC c= the topology of T
proof
let u be object;
assume u in Union UC;
then consider k being Nat such that
A27: u in UC.k by PROB_1:12;
A28: k in NAT by ORDINAL1:def 12;
reconsider u9=u as Subset of T by A27;
P[k,UC.k] by A11,A28;
then u9 is open by A27,TOPS_2:def 1;
hence thesis by PRE_TOPC:def 2;
end;
then Union UC is Basis of T by A12,YELLOW_9:32;
then UC is Basis_sigma_locally_finite by A26;
hence thesis;
end;
Lm6: for U,A st A is closed holds U\A is open
proof
let U,A;
A1: U/\([#]T\A)=U/\A`;
assume A is closed;
hence thesis by A1,SUBSET_1:13;
end;
theorem Th17:
for U being sequence of bool(the carrier of T) st (for n
holds U.n is open) holds Union U is open
proof
let U be sequence of bool(the carrier of T);
assume
A1: for n holds U.n is open;
rng U c= the topology of T
proof
let u be object;
assume u in rng U;
then consider k being object such that
A2: k in dom U and
A3: u = U.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A2;
U.k is open by A1;
hence thesis by A3,PRE_TOPC:def 2;
end;
then union(rng U) in the topology of T by PRE_TOPC:def 1;
then Union U in the topology of T by CARD_3:def 4;
hence thesis by PRE_TOPC:def 2;
end;
theorem Th18:
(for A,U st A is closed & U is open & A c=U ex W being sequence of
bool(the carrier of T) st A c= Union W & Union W c= U & (for n holds Cl
(W.n) c= U & W.n is open )) implies T is normal
proof
assume
A1: for A,U st A is closed & U is open & A c=U ex W being sequence of
bool(the carrier of T) st A c= Union W & Union W c= U & for n holds Cl (W.
n) c= U & W.n is open;
for A, B being Subset of T st A <> {} & B <> {} & A is closed & B is
closed & A misses B ex UA,WB being Subset of T st UA is open & WB is open & A
c=UA & B c= WB & UA misses WB
proof
let A,B be Subset of T;
assume that
A <> {} and
B <> {} and
A2: A is closed & B is closed and
A3: A misses B;
set W=[#]T\B;
A c=B` by A3,SUBSET_1:23;
then consider Wn being sequence of bool(the carrier of T) such that
A4: A c= Union Wn and
Union Wn c= W and
A5: for n holds Cl (Wn.n) c= W & (Wn.n) is open by A1,A2;
set U= [#]T\A;
B c= A` by A3,SUBSET_1:23;
then consider Un being sequence of bool(the carrier of T) such that
A6: B c= Union Un and
Union Un c= U and
A7: for n holds Cl (Un.n) c= U & (Un.n) is open by A1,A2;
deffunc UW(Nat) =Un.$1\union{Cl (Wn.k) where k is Element of
NAT: k in Seg $1\/{0}};
defpred E2[Element of NAT,set] means $2 = UW($1);
A8: for k being Element of NAT ex y being Subset of T st E2[k,y];
consider FUW being sequence of bool the carrier of T such that
A9: for k being Element of NAT holds E2[k,FUW.k] from FUNCT_2:sch 3(
A8);
for n holds FUW.n is open
proof
let n;
set CLn={Cl (Wn.k) where k is Element of NAT: k in Seg n\/{0}};
now
let C be object;
assume C in CLn;
then ex k being Element of NAT st C=Cl (Wn.k) & k in Seg n\/{ 0};
hence C in bool the carrier of T;
end;
then reconsider CLn as Subset-Family of T by TARSKI:def 3;
deffunc CL(Element of NAT)=Cl(Wn.$1);
A10: Seg n\/{0} is finite;
A11: {CL(k) where k is Element of NAT: k in Seg n\/{0}} is finite from
FRAENKEL:sch 21(A10);
now
let A;
assume A in CLn;
then ex k being Element of NAT st A=Cl(Wn.k) & k in Seg n\/{0 };
hence A is closed;
end;
then
A12: CLn is closed by TOPS_2:def 2;
Un.n is open by A7;
then Un.n\union CLn is open by A11,A12,Lm6,TOPS_2:21;
hence thesis by A9;
end;
then
A13: Union FUW is open by Th17;
A14: for n holds B misses Cl (Wn.n)
proof
let n;
Cl (Wn.n) c= W by A5;
hence thesis by XBOOLE_1:63,79;
end;
now
let b be object;
assume that
A15: b in B and
A16: not b in Union FUW;
consider k being Nat such that
A17: b in Un.k by A6,A15,PROB_1:12;
A18: k in NAT by ORDINAL1:def 12;
not b in union{Cl (Wn.m) where m is Element of NAT: m in Seg k\/{0} }
proof
assume
b in union{Cl (Wn.m) where m is Element of NAT: m in Seg k\/{ 0}};
then consider CL being set such that
A19: b in CL and
A20: CL in {Cl (Wn.m) where m is Element of NAT: m in Seg k\/{0}}
by TARSKI:def 4;
consider m being Element of NAT such that
A21: CL=Cl(Wn.m) and
m in Seg k\/{0} by A20;
B meets Cl(Wn.m) by A15,A19,A21,XBOOLE_0:3;
hence contradiction by A14;
end;
then b in UW(k) by A17,XBOOLE_0:def 5;
then b in FUW.k by A9,A18;
hence contradiction by A16,PROB_1:12;
end;
then
A22: B c= Union FUW;
deffunc WU(Nat) =Wn.$1\union{Cl (Un.k) where k is Element of
NAT: k in Seg $1\/{0}};
defpred E1[Element of NAT,set] means $2=WU($1);
A23: for k being Element of NAT ex y being Subset of T st E1[k,y];
consider FWU being sequence of bool the carrier of T such that
A24: for k being Element of NAT holds E1[k,FWU.k] from FUNCT_2:sch 3(
A23);
A25: Union FUW misses Union FWU
proof
assume Union FUW meets Union FWU;
then consider f being object such that
A26: f in Union FUW and
A27: f in Union FWU by XBOOLE_0:3;
consider n being Nat such that
A28: f in FUW.n by A26,PROB_1:12;
consider k being Nat such that
A29: f in FWU.k by A27,PROB_1:12;
A30: n>=k implies FUW.n misses FWU.k
proof
assume that
A31: n>=k and
A32: FUW.n meets FWU.k;
consider w being object such that
A33: w in FUW.n and
A34: w in FWU.k by A32,XBOOLE_0:3;
A35: k in NAT by ORDINAL1:def 12;
A36: n in NAT by ORDINAL1:def 12;
w in Wn.k\union{Cl(Un.l) where l is Element of NAT: l in Seg k\/{
0} } by A24,A34,A35;
then
A37: w in Wn.k by XBOOLE_0:def 5;
k = 0 or k in Seg k by FINSEQ_1:3;
then k in {0} or k in Seg k & Seg k c= Seg n by A31,FINSEQ_1:5
,TARSKI:def 1;
then k in Seg n\/{0} by XBOOLE_0:def 3;
then
A38: Wn.k c= Cl(Wn.k) & Cl(Wn.k) in {Cl (Wn.l) where l is Element of
NAT: l in Seg n\/{0}} by PRE_TOPC:18;
w in Un.n\union{Cl(Wn.l) where l is Element of NAT: l in Seg n\/{
0} } by A9,A33,A36;
then
not w in union{Cl(Wn.l) where l is Element of NAT: l in Seg n\/{0
}} by XBOOLE_0:def 5;
hence contradiction by A37,A38,TARSKI:def 4;
end;
n<=k implies FUW.n misses FWU.k
proof
assume that
A39: n<=k and
A40: FUW.n meets FWU.k;
consider u being object such that
A41: u in FUW.n and
A42: u in FWU.k by A40,XBOOLE_0:3;
A43: n in NAT by ORDINAL1:def 12;
A44: k in NAT by ORDINAL1:def 12;
u in Un.n\union{Cl(Wn.l) where l is Element of NAT: l in Seg n\/{
0} } by A9,A41,A43;
then
A45: u in Un.n by XBOOLE_0:def 5;
n = 0 or n in Seg n by FINSEQ_1:3;
then n in {0} or n in Seg n & Seg n c= Seg k by A39,FINSEQ_1:5
,TARSKI:def 1;
then n in Seg k\/{0} by XBOOLE_0:def 3;
then
A46: Un.n c= Cl(Un.n) & Cl(Un.n) in {Cl (Un.l) where l is Element of
NAT: l in Seg k\/{0}} by PRE_TOPC:18;
u in Wn.k\union{Cl(Un.l) where l is Element of NAT: l in Seg k\/{
0} } by A24,A42,A44;
then
not u in union{Cl(Un.l) where l is Element of NAT: l in Seg k\/{0
}} by XBOOLE_0:def 5;
hence contradiction by A45,A46,TARSKI:def 4;
end;
hence contradiction by A28,A29,A30,XBOOLE_0:3;
end;
for n holds FWU.n is open
proof
let n;
set CLn={Cl (Un.k) where k is Element of NAT: k in Seg n\/{0}};
now
let C be object;
assume C in CLn;
then ex k being Element of NAT st C=Cl (Un.k) & k in Seg n\/{ 0};
hence C in bool the carrier of T;
end;
then reconsider CLn as Subset-Family of T by TARSKI:def 3;
deffunc CL(Element of NAT)=Cl(Un.$1);
A47: Seg n\/{0} is finite;
A48: {CL(k) where k is Element of NAT : k in Seg n\/{0}} is finite from
FRAENKEL:sch 21(A47);
now
let A;
assume A in CLn;
then ex k being Element of NAT st A=Cl(Un.k) & k in Seg n\/{0 };
hence A is closed;
end;
then
A49: CLn is closed by TOPS_2:def 2;
Wn.n is open by A5;
then Wn.n\union CLn is open by A48,A49,Lm6,TOPS_2:21;
hence thesis by A24;
end;
then
A50: Union FWU is open by Th17;
A51: for n holds A misses Cl (Un.n)
proof
let n;
Cl (Un.n) c= U by A7;
hence thesis by XBOOLE_1:63,79;
end;
now
let a be object;
assume that
A52: a in A and
A53: not a in Union FWU;
consider k being Nat such that
A54: a in Wn.k by A4,A52,PROB_1:12;
A55: k in NAT by ORDINAL1:def 12;
not a in union{Cl (Un.m) where m is Element of NAT: m in Seg k\/{0} }
proof
assume
a in union{Cl (Un.m) where m is Element of NAT: m in Seg k\/{ 0}};
then consider CL being set such that
A56: a in CL and
A57: CL in {Cl (Un.m) where m is Element of NAT: m in Seg k\/{0}}
by TARSKI:def 4;
consider m being Element of NAT such that
A58: CL=Cl(Un.m) and
m in Seg k\/{0} by A57;
A meets Cl(Un.m) by A52,A56,A58,XBOOLE_0:3;
hence contradiction by A51;
end;
then a in WU(k) by A54,XBOOLE_0:def 5;
then a in FWU.k by A24,A55;
hence contradiction by A53,PROB_1:12;
end;
then A c= Union FWU;
hence thesis by A22,A25,A13,A50;
end;
hence thesis;
end;
theorem Th19:
for T st T is regular for Bn being FamilySequence of T st (Union
Bn) is Basis of T holds for U being Subset of T,p being Point of T st U is open
& p in U ex O being Subset of T st p in O & Cl O c= U & O in Union Bn
proof
let T;
assume
A1: T is regular;
let Bn be FamilySequence of T;
assume
A2: (Union Bn) is Basis of T;
for U,p st U is open & p in U ex O being Subset of T st p in O & Cl O c=
U & O in Union Bn
proof
let U,p;
assume that
U is open and
A3: p in U;
now
per cases;
suppose
A4: U=the carrier of T;
consider O being Subset of T such that
A5: O in Union Bn & p in O and
O c= U by A2,A3,YELLOW_9:31;
take O;
Cl O c= U by A4;
hence thesis by A5;
end;
suppose
U<>the carrier of T;
then U c< the carrier of T by XBOOLE_0:def 8;
then
A6: U`<>{} by XBOOLE_1:105;
p in U`` by A3;
then consider W,V being Subset of T such that
A7: W is open and
A8: V is open and
A9: p in W and
A10: U` c= V and
A11: W misses V by A1,A6;
consider O being Subset of T such that
A12: O in Union Bn & p in O and
A13: O c= W by A2,A7,A9,YELLOW_9:31;
W c=V` by A11,SUBSET_1:23;
then O c=V` by A13;
then Cl O c= Cl V` by PRE_TOPC:19;
then
A14: Cl O c= V` by A8,PRE_TOPC:22;
take O;
V` c= U by A10,SUBSET_1:17;
hence thesis by A12,A14,XBOOLE_1:1;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem
for T st T is regular & ex Bn being FamilySequence of T st Bn is
Basis_sigma_locally_finite holds T is normal
proof
let T;
assume that
A1: T is regular and
A2: ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite;
consider Bn being FamilySequence of T such that
A3: Bn is Basis_sigma_locally_finite by A2;
A4: Union Bn is Basis of T by A3;
A5: Bn is sigma_locally_finite by A3;
for A,U st A is closed & U is open & A c=U ex W being sequence of
bool(the carrier of T) st A c= Union W & Union W c= U & for n holds Cl (W.n) c=
U & W.n is open
proof
let A,U;
assume that
A is closed and
U is open and
A6: A c=U;
deffunc B(object)=union{O where O is Subset of T: O in Bn.$1 & Cl O c=U};
A7: for k being object st k in NAT holds B(k) in bool the carrier of T
proof
let k be object;
assume k in NAT;
then reconsider k as Element of NAT;
now
let bu be object;
assume bu in B(k);
then consider b being set such that
A8: bu in b and
A9: b in {O where O is Subset of T: O in Bn.k & Cl O c=U} by TARSKI:def 4;
ex O being Subset of T st b=O & O in Bn.k & Cl O c=U by A9;
hence bu in the carrier of T by A8;
end;
then B(k) c= the carrier of T;
hence thesis;
end;
consider BU being sequence of bool (the carrier of T) such that
A10: for k being object st k in NAT holds BU.k= B(k) from FUNCT_2:sch 2(
A7);
A11: now
let n;
set BUn={O where O is Subset of T: O in Bn.n & Cl O c=U};
BUn c= bool the carrier of T
proof
let b be object;
assume b in BUn;
then ex O being Subset of T st b=O & O in Bn.n & Cl O c=U;
hence thesis;
end;
then reconsider BUn as Subset-Family of T;
A12: BUn c=Bn.n
proof
let b be object;
assume b in BUn;
then ex O being Subset of T st b=O & O in Bn.n & Cl O c=U;
hence thesis;
end;
Bn.n is locally_finite by A5;
then
A13: Cl union(BUn)= union(clf BUn) by A12,PCOMPS_1:9,20;
A14: Cl union(BUn)c=U
proof
let ClBu be object;
assume ClBu in Cl union(BUn);
then consider ClB being set such that
A15: ClBu in ClB and
A16: ClB in clf BUn by A13,TARSKI:def 4;
reconsider ClB as Subset of T by A16;
consider B being Subset of T such that
A17: Cl B =ClB and
A18: B in BUn by A16,PCOMPS_1:def 2;
ex Q being Subset of T st B=Q & Q in Bn.n & Cl Q c=U by A18;
hence thesis by A15,A17;
end;
BUn c= the topology of T
proof
let B be object;
assume B in BUn;
then consider Q being Subset of T such that
A19: B=Q and
A20: Q in Bn.n and
Cl Q c=U;
A21: Union Bn c= the topology of T by A4,TOPS_2:64;
Q in Union Bn by A20,PROB_1:12;
hence thesis by A19,A21;
end;
then union BUn in the topology of T by PRE_TOPC:def 1;
then union BUn is open by PRE_TOPC:def 2;
hence BU.n is open & Cl (BU.n) c=U by A10,A14;
end;
A22: Union BU c= U
proof
let bu be object;
assume bu in Union BU;
then consider k being Nat such that
A23: bu in BU.k by PROB_1:12;
A24: k in NAT by ORDINAL1:def 12;
bu in union {O where O is Subset of T: O in Bn.k & Cl O c=U}
by A10,A23,A24;
then consider b being set such that
A25: bu in b and
A26: b in {O where O is Subset of T: O in Bn.k & Cl O c=U} by TARSKI:def 4;
consider O being Subset of T such that
A27: b=O and
O in Bn.k and
A28: Cl O c=U by A26;
O c= Cl O by PRE_TOPC:18;
then b c= U by A27,A28;
hence thesis by A25;
end;
for a being object st a in A holds a in Union BU
proof
let a be object;
assume a in A;
then consider Q being Subset of T such that
A29: a in Q and
A30: Cl Q c= U and
A31: Q in Union Bn by A1,A4,A6,Th19;
consider k being Nat such that
A32: Q in Bn.k by A31,PROB_1:12;
A33: k in NAT by ORDINAL1:def 12;
Q in {O where O is Subset of T: O in Bn.k & Cl O c=U} by A30,A32;
then a in B(k) by A29,TARSKI:def 4;
then a in BU.k by A10,A33;
hence thesis by PROB_1:12;
end;
then A c= Union BU;
hence thesis by A22,A11;
end;
hence thesis by Th18;
end;
Lm7: for r being Real,A being Point of RealSpace st r>0 holds A in Ball(A,r)
proof
let r be Real,A be Point of RealSpace;
reconsider A9=A as Real;
A1: |.A9-A9.|=0 by ABSVALUE:2;
assume r>0;
then dist(A,A)<r by A1,TOPMETR:11;
hence thesis by METRIC_1:11;
end;
definition
let T;
let F,G be RealMap of T;
redefine func F+G -> RealMap of T means :: redefines + (VALUED_1, definition)
:Def7:
for t being Element of T holds it.t=F.t+G.t;
coherence
proof
F+G is Function of the carrier of T,REAL;
hence thesis;
end;
compatibility
proof
let m be RealMap of T;
thus m = F+G implies for p being Element of T holds m.p = F.p+G.p by
VALUED_1:1;
A1: dom (F+G) = dom F /\ dom G by VALUED_1:def 1
.= (the carrier of T) /\ dom G by FUNCT_2:def 1
.= (the carrier of T) /\ the carrier of T by FUNCT_2:def 1;
assume
A2: for p being Element of T holds m.p = F.p+G.p;
A3: now
let x be object;
assume
A4: x in dom m;
hence m.x = (F.x)+(G.x) by A2
.= (F+G).x by A1,A4,VALUED_1:def 1;
end;
dom m = the carrier of T by FUNCT_2:def 1;
hence thesis by A1,A3,FUNCT_1:2;
end;
end;
theorem
for f being RealMap of T st f is continuous for F being RealMap of [:T
,T:] st for x,y being Element of T holds F.(x,y)=|.f.x-f.y.| holds F is
continuous
proof
let f be RealMap of T such that
A1: f is continuous;
set TT= [:T,T:];
set cT= the carrier of T;
reconsider f9=f as Function of T,R^1 by TOPMETR:17;
let F be RealMap of [:T,T:] such that
A2: for x,y being Element of T holds F.(x,y)=|.f.x-f.y.|;
reconsider F9=F as Function of [:T,T:],R^1 by TOPMETR:17;
A3: f9 is continuous by A1,JORDAN5A:27;
now
let tt be Point of TT;
tt in the carrier of TT;
then tt in [:cT,cT:] by BORSUK_1:def 2;
then consider t1,t2 being object such that
A4: t1 in cT & t2 in cT and
A5: [t1,t2]=tt by ZFMISC_1:def 2;
reconsider t1,t2 as Point of T by A4;
for R being Subset of R^1 st R is open & F9.tt in R ex H being Subset
of TT st H is open & tt in H & F9.:H c= R
proof
reconsider ft1=f.t1,ft2=f.t2 as Point of RealSpace by METRIC_1:def 13;
reconsider Ftt=F.tt as Point of RealSpace by METRIC_1:def 13;
let R be Subset of R^1;
assume R is open & F9.tt in R;
then consider r being Real such that
A6: r>0 and
A7: Ball(Ftt,r) c= R by TOPMETR:15,def 6;
reconsider r9=r as Real;
reconsider A=Ball(ft1,r9/2),B=Ball(ft2,r9/2) as Subset of R^1 by
METRIC_1:def 13,TOPMETR:17;
A8: A is open & f9 is_continuous_at t1 by A3,TMAP_1:50,TOPMETR:14,def 6;
f.t1 in A by A6,Lm7,XREAL_1:139;
then consider T1 being Subset of T such that
A9: T1 is open and
A10: t1 in T1 and
A11: f9.:T1 c= A by A8,TMAP_1:43;
A12: B is open & f9 is_continuous_at t2 by A3,TMAP_1:50,TOPMETR:14,def 6;
f.t2 in B by A6,Lm7,XREAL_1:139;
then consider T2 being Subset of T such that
A13: T2 is open and
A14: t2 in T2 and
A15: f9.:T2 c= B by A12,TMAP_1:43;
F.tt = F.(t1,t2) by A5;
then
A16: |.f9.t1-f9.t2.|=F.tt by A2;
A17: F.:[:T1,T2:]c= R
proof
let Fxy be object;
assume Fxy in F.:[:T1,T2:];
then consider xy being object such that
xy in dom F and
A18: xy in [:T1,T2:] and
A19: Fxy = F.xy by FUNCT_1:def 6;
consider x,y being object such that
A20: x in T1 and
A21: y in T2 and
A22: xy=[x,y] by A18,ZFMISC_1:def 2;
reconsider x,y as Point of T by A20,A21;
reconsider fx=f.x,fy=f.y as Point of RealSpace by METRIC_1:def 13;
y in cT;
then y in dom f by FUNCT_2:def 1;
then f.y in f.:T2 by A21,FUNCT_1:def 6;
then
A23: dist(fy,ft2)<r9/2 by A15,METRIC_1:11;
reconsider Fxy1=F.[x,y] as Point of RealSpace by METRIC_1:def 13;
A24: |.f.x-f.y.|=F.(x,y) by A2;
then F.[x,y]<=|.f.x-f.t1.|+F.tt+|.f.t2-f.y.| by A16,Lm2;
then F.[x,y]<=|.f.x-f.t1.|+F.tt+dist(ft2,fy) by TOPMETR:11;
then
A25: F.[x,y]+0<=F.tt+dist(fx,ft1)+dist(ft2,fy) by TOPMETR:11;
F.tt<=|.f.t1-f.x.|+F.[x,y]+|.f.y-f.t2.| by A16,A24,Lm2;
then F.tt<=dist(fx,ft1)+F.[x,y]+|.f.y-f.t2.| by TOPMETR:11;
then
A26: F.tt<=F.[x,y]+dist(fx,ft1)+dist(fy,ft2) by TOPMETR:11;
x in cT;
then x in dom f by FUNCT_2:def 1;
then f.x in f.:T1 by A20,FUNCT_1:def 6;
then dist(fx,ft1)<r9/2 by A11,METRIC_1:11;
then
A27: dist(fx,ft1)+dist(fy,ft2)<r9/2+r9/2 by A23,XREAL_1:8;
then F.[x,y]+(dist(fx,ft1)+dist(fy,ft2))<F.[x,y]+r9 by XREAL_1:8;
then F.tt < -(-F.[x,y]-r9) by A26,XXREAL_0:2;
then -F.tt-0 > -r9-F.[x,y] by XREAL_1:26;
then
A28: -F.tt+F.[x,y] > -r9+0 by XREAL_1:21;
F.tt+(dist(fx,ft1)+dist(ft2,fy))<F.tt+r9 by A27,XREAL_1:8;
then F.[x,y]+0<F.tt+r9 by A25,XXREAL_0:2;
then F.[x,y]-F.tt < r9-0 by XREAL_1:21;
then |.F.[x,y]-F.tt.|<r9 by A28,SEQ_2:1;
then dist(Ftt,Fxy1)<r9 by TOPMETR:11;
then Fxy1 in Ball(Ftt,r) by METRIC_1:11;
hence thesis by A7,A19,A22;
end;
tt in [:T1,T2:] by A5,A10,A14,ZFMISC_1:def 2;
hence thesis by A9,A13,A17,BORSUK_1:6;
end;
hence F9 is_continuous_at tt by TMAP_1:43;
end;
then F9 is continuous by TMAP_1:50;
hence thesis by JORDAN5A:27;
end;
theorem Th22:
for F,G being RealMap of T st F is continuous & G is continuous
holds F + G is continuous
proof
let F,G be RealMap of T such that
A1: F is continuous and
A2: G is continuous;
reconsider F9=F,G9=G,FG9=F+G as Function of T,R^1 by TOPMETR:17;
A3: G9 is continuous by A2,JORDAN5A:27;
A4: F9 is continuous by A1,JORDAN5A:27;
now
let t be Point of T;
for R being Subset of R^1 st R is open & FG9.t in R ex H being Subset
of T st H is open & t in H & FG9.:H c= R
proof
reconsider Ft=F.t, Gt=G.t,FGt=(F+G).t as Point of RealSpace by
METRIC_1:def 13;
let R be Subset of R^1;
assume R is open & FG9.t in R;
then consider r being Real such that
A5: r>0 and
A6: Ball(FGt,r) c= R by TOPMETR:15,def 6;
reconsider r9=r as Real;
reconsider A=Ball(Ft,r9/2),B=Ball(Gt,r9/2) as Subset of R^1 by
METRIC_1:def 13,TOPMETR:17;
A7: A is open & F9 is_continuous_at t by A4,TMAP_1:50,TOPMETR:14,def 6;
F9.t in A by A5,Lm7,XREAL_1:139;
then consider AT being Subset of T such that
A8: AT is open and
A9: t in AT and
A10: F9.:AT c= A by A7,TMAP_1:43;
A11: B is open & G9 is_continuous_at t by A3,TMAP_1:50,TOPMETR:14,def 6;
G.t in B by A5,Lm7,XREAL_1:139;
then consider BT being Subset of T such that
A12: BT is open and
A13: t in BT and
A14: G9.:BT c= B by A11,TMAP_1:43;
A15: (F+G).:(AT/\BT) c= R
proof
let FGx be object;
assume FGx in (F+G).:(AT/\BT);
then consider x being object such that
A16: x in dom (F+G) and
A17: x in AT/\BT and
A18: FGx=(F+G).x by FUNCT_1:def 6;
reconsider x as Point of T by A16;
reconsider Fx=F.x,Gx=G.x,FGx9=(F+G).x as Point of RealSpace by
METRIC_1:def 13;
dom G = the carrier of T & x in BT by A17,FUNCT_2:def 1,XBOOLE_0:def 4;
then G.x in G.:BT by FUNCT_1:def 6;
then dist(Gx,Gt)<r9/2 by A14,METRIC_1:11;
then
A19: |.G.x-G.t.|<r9/2 by TOPMETR:11;
then
A20: -r9/2<G.x-G.t by SEQ_2:1;
dom F = the carrier of T & x in AT by A17,FUNCT_2:def 1,XBOOLE_0:def 4;
then F.x in F.:AT by FUNCT_1:def 6;
then dist(Fx,Ft)<r9/2 by A10,METRIC_1:11;
then
A21: |.F.x-F.t.|<r9/2 by TOPMETR:11;
then -r9/2<F.x-F.t by SEQ_2:1;
then -r9/2 +(-r9/2)<(F.x-F.t)+(G.x-G.t) by A20,XREAL_1:8;
then
A22: -r9<(F.x+G.x)-(F.t+G.t);
A23: G.x-G.t<r9/2 by A19,SEQ_2:1;
F.x-F.t<r9/2 by A21,SEQ_2:1;
then (F.x-F.t)+(G.x-G.t)<r9/2+r9/ 2 by A23,XREAL_1:8;
then |.(F.x+G.x)-(F.t+G.t).|< r9 by A22,SEQ_2:1;
then |.(F+G).x-(F.t+G.t).|< r9 by Def7;
then |.(F+G).x-(F+G).t.|< r9 by Def7;
then dist(FGt,FGx9)<r9 by TOPMETR:11;
then FGx9 in Ball(FGt,r) by METRIC_1:11;
hence thesis by A6,A18;
end;
t in AT/\BT by A9,A13,XBOOLE_0:def 4;
hence thesis by A8,A12,A15;
end;
hence FG9 is_continuous_at t by TMAP_1:43;
end;
then FG9 is continuous by TMAP_1:50;
hence thesis by JORDAN5A:27;
end;
theorem Th23:
for ADD being BinOp of Funcs(the carrier of T,REAL) st (for f1,
f2 being RealMap of T holds ADD.(f1,f2)=f1+f2) holds ADD is having_a_unity &
ADD is commutative associative
proof
set F=Funcs(the carrier of T,REAL);
let ADD be BinOp of Funcs(the carrier of T,REAL) such that
A1: for f1,f2 being RealMap of T holds ADD.(f1,f2)=f1+f2;
ex map9 be Element of F st map9 is_a_unity_wrt ADD
proof
reconsider map0 = (the carrier of T) --> In(0,REAL) as RealMap of T;
reconsider map09=map0 as Element of F by FUNCT_2:8;
take map09;
now
let f be Element of F;
now
let x be Element of T;
(f+map09).x=f.x+map09.x by Def7;
then (f+map09).x=f.x+0 by FUNCOP_1:7;
hence (f+map09).x=f.x;
end;
then f+map09=f by FUNCT_2:63;
hence ADD.(map0,f)=f & ADD.(f,map0)=f by A1;
end;
hence thesis by BINOP_1:3;
end;
hence ADD is having_a_unity by SETWISEO:def 2;
thus ADD is commutative
proof
let f1,f2 be Element of F;
ADD.(f1,f2)=f1+f2 by A1;
hence thesis by A1;
end;
thus ADD is associative
proof
let f1,f2,f3 be Element of F;
reconsider ADD12=ADD.(f1,f2),ADD23=ADD.(f2,f3) as RealMap of T by
FUNCT_2:66;
A2: ADD12+f3=ADD.(ADD12,f3) by A1;
now
let t be Element of T;
(f1+(f2+f3)).t=f1.t+(f2+f3).t & (f2+f3).t =f2.t+f3.t by Def7;
then (f1+(f2+f3)).t=(f1.t+f2.t)+f3.t;
then (f1+(f2+f3)).t=(f1+f2).t+f3.t by Def7;
hence (f1+(f2+f3)).t=((f1+f2)+f3).t by Def7;
end;
then
A3: f1+(f2+f3)=(f1+f2)+f3 by FUNCT_2:63;
f1+(f2+f3)=f1+ADD23 by A1;
then f1+ADD23=ADD12+f3 by A1,A3;
hence thesis by A1,A2;
end;
end;
theorem Th24:
for ADD being BinOp of Funcs(the carrier of T,REAL) st (for f1,
f2 being RealMap of T holds ADD.(f1,f2)=f1+f2) for map9 being Element of Funcs(
the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds map9 is continuous
proof
let ADD be BinOp of Funcs(the carrier of T,REAL) such that
A1: for f1,f2 being RealMap of T holds ADD.(f1,f2)=f1+f2;
set F=Funcs(the carrier of T,REAL);
let map9 be Element of F such that
A2: map9 is_a_unity_wrt ADD;
A3: for x be Point of T holds map9.x=0
proof
assume ex x be Point of T st map9.x<>0;
then consider x be Point of T such that
A4: map9.x<>0;
ADD.(map9,map9)=map9 by A2,BINOP_1:3;
then map9+map9=map9 by A1;
then map9.x + map9.x = map9.x by Def7;
hence thesis by A4;
end;
reconsider map99=map9 as Function of T,R^1 by TOPMETR:17;
for A being Subset of T holds map99.:(Cl A) c= Cl(map99.:A qua Subset of R^1)
proof
let A be Subset of T;
let mCla be object;
assume mCla in map99.:(Cl A);
then
A5: ex Cla being object st Cla in dom map9 & Cla in Cl A & mCla=map99.Cla by
FUNCT_1:def 6;
then A <>{}T by PRE_TOPC:22;
then consider a being object such that
A6: a in A by XBOOLE_0:def 1;
reconsider a as Element of T by A6;
dom map9=the carrier of T & map9.a =0 by A3,FUNCT_2:def 1;
then 0 in map9.:A by A6,FUNCT_1:def 6;
then
A7: mCla in map9.:A by A3,A5;
map99.:A c= Cl(map99.:A) by PRE_TOPC:18;
hence thesis by A7;
end;
then map99 is continuous by TOPS_2:45;
hence thesis by JORDAN5A:27;
end;
definition
let A,B be non empty set;
let F be Function of A,Funcs(A,B);
func F Toler -> Function of A,B means
:Def8:
for p be Element of A holds it. p=F.p.p;
existence
proof
deffunc IT(Element of A)=F.$1.$1;
defpred P[Element of A,set] means $2 = IT($1);
A1: for x being Element of A ex y being Element of B st P[x,y]
proof
let x be Element of A;
reconsider Funx=F.x as Function of A,B by FUNCT_2:66;
Funx.x in B;
hence thesis;
end;
consider F be Function of A,B such that
A2: for x being Element of A holds P[x,F.x] from FUNCT_2:sch 3(A1);
take F;
thus thesis by A2;
end;
uniqueness
proof
now
let IT1,IT2 be Function of A,B such that
A3: for x being Element of A holds IT1.x=F.x.x & for x being Element
of A holds IT2.x=F.x.x;
now
let x be Element of A;
IT1.x=F.x.x by A3;
hence IT1.x=IT2.x by A3;
end;
hence IT1=IT2 by FUNCT_2:63;
end;
hence thesis;
end;
end;
theorem
for ADD being BinOp of Funcs(the carrier of T,REAL) st (for f1,f2
being RealMap of T holds ADD.(f1,f2)=f1+f2) for F being FinSequence of Funcs(
the carrier of T,REAL) st for n st 0 <> n & n <= len F holds F.n is continuous
RealMap of T holds ADD "**" F is continuous RealMap of T
proof
let ADD be BinOp of Funcs(the carrier of T,REAL) such that
A1: for f1,f2 being RealMap of T holds ADD.(f1,f2)=f1+f2;
set Fu=Funcs(the carrier of T,REAL);
let F be FinSequence of Funcs(the carrier of T,REAL) such that
A2: for n st 0 <> n & n <= len F holds F.n is continuous RealMap of T;
reconsider ADDF = ADD "**" F as RealMap of T by FUNCT_2:66;
now
per cases;
suppose
A3: len F=0;
A4: ADD is having_a_unity by A1,Th23;
then ex x be Element of Fu st x is_a_unity_wrt ADD by SETWISEO:def 2;
then
A5: the_unity_wrt ADD is_a_unity_wrt ADD by BINOP_1:def 8;
ADDF = the_unity_wrt ADD by A3,A4,FINSOP_1:def 1;
hence thesis by A1,A5,Th24;
end;
suppose
A6: len F<>0;
A7: len F >=1
proof
assume len F < 1;
then len F <1+0;
hence thesis by A6,NAT_1:13;
end;
then consider f be sequence of Fu such that
A8: f.1 = F.1 and
A9: for n being Nat st 0 <> n & n < len F holds f.(n+1) = ADD.(f.n,F.(n+1))
and
A10: ADD "**" F = f.(len F) by FINSOP_1:1;
defpred Con[Nat] means $1<=len F implies f.$1 is continuous RealMap of T;
A11: for n be Nat st n>=1 holds Con[n] implies Con[n+1]
proof
let n be Nat such that
A12: n>=1 and
A13: Con[n];
assume
A14: n+1<=len F;
reconsider n as Element of NAT by ORDINAL1:def 12;
A15: n+0<n+1 by XREAL_1:8;
then n<len F by A14,XXREAL_0:2;
then
A16: f.(n+1)=ADD.(f.n,F.(n+1)) by A9,A12;
1+0<=n+1 by A12,XREAL_1:8;
then (n+1) in Seg len F by A14,FINSEQ_1:1;
then n+1 in dom F by FINSEQ_1:def 3;
then F.(n+1) in rng F by FUNCT_1:def 3;
then reconsider fn=f.n,Fn1=F.(n+1) as RealMap of T by FUNCT_2:66;
Fn1 is continuous by A2,A14;
then fn+Fn1 is continuous by A13,A14,A15,Th22,XXREAL_0:2;
hence thesis by A1,A16;
end;
A17: Con[1] by A2,A8;
for n be Nat st n>=1 holds Con[n] from NAT_1:sch 8(A17,A11);
hence thesis by A7,A10;
end;
end;
hence thesis;
end;
theorem
for F be Function of the carrier of T,Funcs(the carrier of T,the
carrier of T1) st for p be Point of T holds F.p is continuous Function of T,T1
for S be Function of the carrier of T,bool the carrier of T st for p be Point
of T holds p in S.p & S.p is open & for p,q be Point of T st p in S.q holds F.p
.p=F.q.p holds F Toler is continuous
proof
let F be Function of the carrier of T,Funcs(the carrier of T,the carrier of
T1) such that
A1: for p holds F.p is continuous Function of T,T1;
let S be Function of the carrier of T,bool the carrier of T such that
A2: for p holds p in S.p & S.p is open & for p,q st p in S.q holds F.p.p
=F.q.p;
now
let t be Point of T;
for R being Subset of T1 st R is open & (F Toler).t in R ex H being
Subset of T st H is open & t in H & (F Toler).:H c= R
proof
reconsider Ft=F.t as Function of T,T1 by A1;
let R be Subset of T1 such that
A3: R is open and
A4: (F Toler).t in R;
Ft is continuous by A1;
then
A5: Ft is_continuous_at t by TMAP_1:50;
Ft.t in R by A4,Def8;
then consider A being Subset of T such that
A6: A is open & t in A and
A7: Ft.:A c= R by A3,A5,TMAP_1:43;
set H=A/\S.t;
A8: (F Toler).:H c= R
proof
let FSh be object;
assume FSh in (F Toler).:H;
then consider h being object such that
A9: h in dom (F Toler) and
A10: h in H and
A11: FSh=(F Toler).h by FUNCT_1:def 6;
reconsider h9=h as Point of T by A9;
h9 in S.t & FSh=F.h9.h9 by A10,A11,Def8,XBOOLE_0:def 4;
then
A12: FSh=Ft.h9 by A2;
A13: the carrier of T =dom Ft by FUNCT_2:def 1;
h9 in A by A10,XBOOLE_0:def 4;
then FSh in Ft.:A by A12,A13,FUNCT_1:def 6;
hence thesis by A7;
end;
take H;
S.t is open & t in S.t by A2;
hence thesis by A6,A8,XBOOLE_0:def 4;
end;
hence F Toler is_continuous_at t by TMAP_1:43;
end;
hence thesis by TMAP_1:50;
end;
reserve m for Function of [:the carrier of T,the carrier of T:],REAL;
definition
let X,r;
let f be Function of X,REAL;
deffunc M(Element of X)=min(r,f.$1);
func min(r,f) -> Function of X,REAL means
:Def9:
for x st x in X holds it.x = min(r,f.x);
existence
proof
defpred P[object,object] means
ex a being Element of X st a = $1 & $2 = M(a);
A1: for x being object st x in X ex y being object st y in REAL & P[x,y]
proof
let x be object;
assume x in X;
then reconsider x as Element of X;
min(r,f.x) is Element of REAL by XREAL_0:def 1;
hence thesis;
end;
consider Min being Function of X,REAL such that
A2: for x being object st x in X holds P[x,Min.x] from FUNCT_2:sch 1(A1);
take Min;
let x;
assume x in X;
then P[x,Min.x] by A2;
hence thesis;
end;
uniqueness
proof
let M1,M2 be Function of X,REAL;
assume that
A3: for x st x in X holds M1.x=min(r,f.x) and
A4: for x st x in X holds M2.x=min(r,f.x);
now
let x being object such that
A5: x in X;
reconsider y = x as Element of X by A5;
M1.x=M(y) by A3,A5;
hence M1.x=M2.x by A4,A5;
end;
hence M1=M2 by FUNCT_2:12;
end;
end;
theorem
for r be Real,f be RealMap of T st f is continuous holds min(r,f) is
continuous
proof
let r be Real,f be RealMap of T such that
A1: f is continuous;
reconsider f9=f,mf9=min(r,f) as Function of T,R^1 by TOPMETR:17;
A2: f9 is continuous by A1,JORDAN5A:27;
now
let t be Point of T;
for R being Subset of R^1 st R is open & mf9.t in R ex U being Subset
of T st U is open & t in U & mf9.:U c= R
proof
reconsider ft=f.t as Point of RealSpace by METRIC_1:def 13;
let R be Subset of R^1 such that
A3: R is open and
A4: mf9.t in R;
now
per cases;
suppose
A5: f.t <=r;
then f.t=min(r,f.t) by XXREAL_0:def 9;
then ft in R by A4,Def9;
then consider s being Real such that
A6: s>0 and
A7: Ball(ft,s) c= R by A3,TOPMETR:15,def 6;
reconsider s9=s as Real;
reconsider B=Ball(ft,s9) as Subset of R^1 by METRIC_1:def 13
,TOPMETR:17;
dist(ft,ft)<s9 by A6,METRIC_1:1;
then
A8: ft in B by METRIC_1:11;
B is open & f9 is_continuous_at t by A2,TMAP_1:50,TOPMETR:14,def 6;
then consider U being Subset of T such that
A9: U is open & t in U and
A10: f9.:U c= B by A8,TMAP_1:43;
min(r,f).:U c= R
proof
let mfx be object;
assume mfx in min(r,f).:U;
then consider x being object such that
A11: x in dom min(r,f) and
A12: x in U and
A13: mfx=min(r,f).x by FUNCT_1:def 6;
reconsider x as Point of T by A11;
f.x in REAL & r in REAL by XREAL_0:def 1;
then reconsider fx=f.x,r9=r as Point of RealSpace
by METRIC_1:def 13;
dom min(r,f)=the carrier of T by FUNCT_2:def 1;
then x in dom f by A11,FUNCT_2:def 1;
then
A14: f.x in f.:U by A12,FUNCT_1:def 6;
then
A15: f.x in B by A10;
now
per cases;
suppose
f.x<=r;
then min(r,f.x)=f.x by XXREAL_0:def 9;
then mfx=f.x by A13,Def9;
hence thesis by A7,A15;
end;
suppose
A16: f.x>r;
dist(fx,ft)<s by A10,A14,METRIC_1:11;
then
A17: |.f.x-f.t.|<s by TOPMETR:11;
A18: r-f.t<=f.x-f.t by A16,XREAL_1:9;
f.x>=f.t by A5,A16,XXREAL_0:2;
then f.x-f.t>=0 by XREAL_1:48;
then f.x-f.t<s by A17,ABSVALUE:def 1;
then
A19: r-f.t<s by A18,XXREAL_0:2;
r-f.t>=0 by A5,XREAL_1:48;
then |.r-f.t.|<s by A19,ABSVALUE:def 1;
then dist(ft,r9)<s by TOPMETR:11;
then
A20: r in B by METRIC_1:11;
min(r,f.x)=r by A16,XXREAL_0:def 9;
then mfx=r by A13,Def9;
hence thesis by A7,A20;
end;
end;
hence thesis;
end;
hence
ex U being Subset of T st U is open & t in U & min(r,f).:U c= R
by A9;
end;
suppose
A21: f.t>r;
set s=f.t-r;
reconsider B=Ball(ft,s) as Subset of R^1 by METRIC_1:def 13
,TOPMETR:17;
s>0 by A21,XREAL_1:50;
then dist(ft,ft)<s by METRIC_1:1;
then
A22: ft in B by METRIC_1:11;
B is open & f9 is_continuous_at t by A2,TMAP_1:50,TOPMETR:14,def 6;
then consider U being Subset of T such that
A23: U is open & t in U and
A24: f9.:U c= B by A22,TMAP_1:43;
min(r,f).:U c= R
proof
let mfx be object;
assume mfx in min(r,f).:U;
then consider x being object such that
A25: x in dom min(r,f) and
A26: x in U and
A27: mfx=min(r,f).x by FUNCT_1:def 6;
reconsider x as Point of T by A25;
reconsider fx=f.x as Point of RealSpace by METRIC_1:def 13;
dom min(r,f)=the carrier of T by FUNCT_2:def 1;
then x in dom f by A25,FUNCT_2:def 1;
then f.x in f.:U by A26,FUNCT_1:def 6;
then dist(ft,fx)<s by A24,METRIC_1:11;
then |.f.t-f.x.|<s by TOPMETR:11;
then f.t+(-f.x) <=f.t+(-r) by ABSVALUE:5;
then -f.x<=-r by XREAL_1:6;
then r<=f.x by XREAL_1:24;
then
A28: min(r,f.x)=r by XXREAL_0:def 9;
min(r,f.t)=r by A21,XXREAL_0:def 9;
then min(r,f).t=r by Def9;
hence thesis by A4,A27,A28,Def9;
end;
hence
ex U being Subset of T st U is open & t in U & min(r,f).:U c= R
by A23;
end;
end;
hence thesis;
end;
hence mf9 is_continuous_at t by TMAP_1:43;
end;
then mf9 is continuous by TMAP_1:50;
hence thesis by JORDAN5A:27;
end;
definition
let X be set, f be Function of [:X,X:],REAL;
pred f is_a_pseudometric_of X means
f is Reflexive symmetric triangle;
end;
Lm8: for f be Function of [:X,X:],REAL holds f is_a_pseudometric_of X iff for
a,b,c be Element of X holds f.(a,a)=0 & f.(a,b)=f.(b,a) & f.(a,c)<=f.(a,b)+f.(b
,c)
by METRIC_1:def 2,METRIC_1:def 4,METRIC_1:def 5;
theorem Th28:
for f be Function of [:X,X:],REAL holds f is_a_pseudometric_of X
iff for a,b,c be Element of X holds f.(a,a) = 0 & f.(a,c)<=f.(a,b)+f.(c,b)
proof
let f be Function of [:X,X:],REAL;
thus f is_a_pseudometric_of X implies for a,b,c be Element of X holds f.(a,a
) = 0 & f.(a,c)<=f.(a,b)+f.(c,b)
proof
assume
A1: f is_a_pseudometric_of X;
let a,b,c be Element of X;
f.(a,c)<=f.(a,b)+f.(b,c) by A1,Lm8;
hence thesis by A1,Lm8;
end;
thus (for a,b,c be Element of X holds f.(a,a) = 0 & f.(a,c)<=f.(a,b)+f.(c,b)
) implies f is_a_pseudometric_of X
proof
assume
A2: for a,b,c be Element of X holds f.(a,a) = 0 & f.(a,c)<=f.(a,b)+f.( c,b);
A3: for a,b being Element of X holds f.(a,b) = f.(b,a)
proof
let a,b be Element of X;
A4: f.(b,a)<=f.(b,b)+f.(a,b) & f.(b,b)=0 by A2;
f.(a,b)<=f.(a,a)+f.(b,a) & f.(a,a)=0 by A2;
hence thesis by A4,XXREAL_0:1;
end;
for a, b, c being Element of X holds f.(a,c) <= f.(a,b) + f.(b,c)
proof
let x, y, z be Element of X;
f.(x,z)<=f.(x,y)+f.(z,y) by A2;
hence thesis by A3;
end;
then f is Reflexive symmetric triangle by A2,A3,METRIC_1:def 2,def 4,def 5;
hence thesis;
end;
end;
Lm9: for r be Real,
X be non empty set,f be Function of [:X,X:],REAL for x,y be
Element of X holds min(r,f).(x,y)=min(r,f.(x,y))
proof
let r be Real,X be non empty set,f be Function of [:X,X:],REAL;
let x,y be Element of X;
min(r,f).(x,y)=min(r,f.[x,y]) by Def9;
hence thesis;
end;
theorem Th29:
for f be Function of [:X,X:],REAL st f is_a_pseudometric_of X
for x,y be Element of X holds f.(x,y)>=0
proof
let f be Function of [:X,X:],REAL such that
A1: f is_a_pseudometric_of X;
let x,y be Element of X;
f.(x,x)<=f.(x,y)+f.(y,x) & f.(x,x)=0 by A1,Lm8;
then 0<=(f.(x,y)+f.(x,y))/2 by A1,Lm8;
hence thesis;
end;
theorem Th30:
for r,m st r>0 & m is_a_pseudometric_of (the carrier of T) holds
min(r,m) is_a_pseudometric_of (the carrier of T)
proof
let r,m such that
A1: r>0 and
A2: m is_a_pseudometric_of (the carrier of T);
now
let a,b,c be Element of T;
m.(a,a)=0 by A2,Th28;
then min(r,m.(a,a))=0 by A1,XXREAL_0:def 9;
hence min(r,m).(a,a)=0 by Lm9;
thus min(r,m).(a,c) <= min(r,m).(a,b)+min(r,m).(c,b)
proof
now
per cases;
suppose
A3: min(r,m).(a,b)+min(r,m).(c,b)>=r;
min(r,m.(a,c))<=r by XXREAL_0:17;
then min(r,m).(a,c)<=r by Lm9;
hence thesis by A3,XXREAL_0:2;
end;
suppose
A4: min(r,m).(a,b)+min(r,m).(c,b)<r;
m.(c,b)>=0 by A2,Th29;
then 0<=min(r,m.(c,b)) by A1,XXREAL_0:20;
then
A5: 0<=min(r,m).(c,b) by Lm9;
m.(a,b)>=0 by A2,Th29;
then 0<=min(r,m.(a,b)) by A1,XXREAL_0:20;
then
A6: 0<=min(r,m).(a,b) by Lm9;
then min(r,m).(a,b)<r by A4,A5,Lm1;
then min(r,m.(a,b))<r by Lm9;
then min(r,m.(a,b))=m.(a,b) by XXREAL_0:def 9;
then
A7: min(r,m).(a,b)=m.(a,b) by Lm9;
min(r,m).(c,b)<r by A4,A6,A5,Lm1;
then min(r,m.(c,b))<r by Lm9;
then min(r,m.(c,b))=m.(c,b) by XXREAL_0:def 9;
then
A8: min(r,m).(c,b)=m.(c,b) by Lm9;
min(r,m.(a,c))<=m.(a,c) & m.(a,c)<=m.(a,b)+m.(c,b) by A2,Th28,
XXREAL_0:17;
then min(r,m.(a,c))<=m.(a,b)+m.(c,b) by XXREAL_0:2;
hence thesis by A7,A8,Lm9;
end;
end;
hence thesis;
end;
end;
hence thesis by Th28;
end;
theorem
for r,m st r>0 & m is_metric_of (the carrier of T) holds min(r,m)
is_metric_of (the carrier of T)
proof
let r,m such that
A1: r>0 and
A2: m is_metric_of (the carrier of T);
let a,b,c be Element of T;
for a,b,c be Element of T holds m.(a,a)=0& m.(a,b)=m.(b,a)& m.(a,c)<=m.(
a,b)+m.(b,c) by A2;
then m is_a_pseudometric_of (the carrier of T) by Lm8;
then
A3: min(r,m) is_a_pseudometric_of (the carrier of T) by A1,Th30;
min(r,m).(a,b)=0 implies a=b
proof
assume min(r,m).(a,b)=0;
then min(r,m.(a,b))=0 by Lm9;
then m.(a,b)=0 by A1,XXREAL_0:def 9;
hence thesis by A2;
end;
hence min(r,m).(a,b)=0 iff a=b by A3,Lm8;
thus thesis by A3,Lm8;
end;