:: The {N}agata-Smirnov Theorem. {P}art {I}
:: by Karol P\c{a}k
::
:: Received May 31, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

Lm1:  for r, s, t being Real st r >= 0 &amp; s >= 0 &amp; r + s < t holds
( r < t &amp; s < t )
proofend;

Lm2:  for r1, r2, r3, r4 being Real holds abs (r1 - r4) <= ((abs (r1 - r2)) + (abs (r2 - r3))) + (abs (r3 - r4))
proofend;

definition
let T be TopSpace;
let F be Subset-Family of T;
attrF is discrete  means :Def1: :: NAGATA_1:def 1
 for p being Point of T ex O being open Subset of T st
( p in O &amp; ( for A, B being Subset of T st A in F &amp; B in F &amp; O meets A &amp; O meets B holds
A = B ) );
end;

:: deftheorem Def1 defines discrete NAGATA_1:def_1_:_
 for T being TopSpace
for F being Subset-Family of T holds
( F is discrete iff for p being Point of T ex O being open Subset of T st
( p in O &amp; ( for A, B being Subset of T st A in F &amp; B in F &amp; O meets A &amp; O meets B holds
A = B ) ) );

registration
let T be non empty TopSpace;
cluster discrete for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st b1 is discrete
proofend;
end;

registration
let T be non empty TopSpace;
cluster empty discrete for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( b1 is empty &amp; b1 is discrete )
proofend;
end;

theorem Th1: :: NAGATA_1:1
for T being non empty TopSpace
for F being Subset-Family of T st ex A being Subset of T st F = {A} holds
F is discrete
proofend;

theorem Th2: :: NAGATA_1:2
for T being non empty TopSpace
for F, G being Subset-Family of T st F c= G &amp; G is discrete holds
F is discrete
proofend;

theorem :: NAGATA_1:3
for T being non empty TopSpace
for F, G being Subset-Family of T st F is discrete holds
F /\ G is discrete by Th2, XBOOLE_1:17;

theorem :: NAGATA_1:4
for T being non empty TopSpace
for F, G being Subset-Family of T st F is discrete holds
F \ G is discrete by Th2, XBOOLE_1:36;

theorem :: NAGATA_1:5
for T being non empty TopSpace
for F, G, H being Subset-Family of T st F is discrete &amp; G is discrete &amp; INTERSECTION (F,G) = H holds
H is discrete
proofend;

theorem Th6: :: NAGATA_1:6
for T being non empty TopSpace
for F being Subset-Family of T
for A, B being Subset of T st F is discrete &amp; A in F &amp; B in F &amp; not A = B holds
A misses B
proofend;

theorem Th7: :: NAGATA_1:7
for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
for p being Point of T ex O being open Subset of T st
( p in O &amp; (INTERSECTION ({O},F)) \ {{}} is trivial )
proofend;

theorem :: NAGATA_1:8
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st
( p in O &amp; (INTERSECTION ({O},F)) \ {{}} is trivial ) ) &amp; ( for A, B being Subset of T st A in F &amp; B in F &amp; not A = B holds
A misses B ) ) )
proofend;

Lm3:  for T being non empty TopSpace
for O being open Subset of T
for A being Subset of T st O meets Cl A holds
O meets A
proofend;

registration
let T be non empty TopSpace;
let F be discrete Subset-Family of T;
cluster clf F ->  discrete ;
coherence
 clf F is discrete
proofend;
end;

Lm4:  for T being non empty TopSpace
for F being Subset-Family of T
for A being Subset of T st A in F holds
Cl A c= Cl (union F)
proofend;

theorem :: NAGATA_1:9
for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
for A, B being Subset of T st A in F &amp; B in F holds
Cl (A /\ B) = (Cl A) /\ (Cl B)
proofend;

theorem :: NAGATA_1:10
for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
Cl (union F) = union (clf F)
proofend;

theorem Th11: :: NAGATA_1:11
for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
F is locally_finite
proofend;

definition
let T be TopSpace;
mode FamilySequence of T is Function of NAT,(bool (bool the carrier of T));
end;

definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
let n be Element of NAT ;
:: original:.
redefine funcUn . n ->  Subset-Family of T;
coherence
 Un . n is Subset-Family of T
proofend;
end;

definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
:: original:Union
redefine func Union Un ->  Subset-Family of T;
coherence
 Union Un is Subset-Family of T
proofend;
end;

definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
attrUn is sigma_discrete  means :Def2: :: NAGATA_1:def 2
 for n being Element of NAT holds Un . n is discrete ;
end;

:: deftheorem Def2 defines sigma_discrete NAGATA_1:def_2_:_
 for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is sigma_discrete iff for n being Element of NAT holds Un . n is discrete );

Lm5:  for T being non empty TopSpace ex Un being FamilySequence of T st Un is sigma_discrete
proofend;

registration
let T be non empty TopSpace;
cluster Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total sigma_discrete for Element of bool [:NAT,(bool (bool the carrier of T)):];
existence
 ex b1 being FamilySequence of T st b1 is sigma_discrete by Lm5;
end;

definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
attrUn is sigma_locally_finite  means :Def3: :: NAGATA_1:def 3
 for n being Element of NAT holds Un . n is locally_finite ;
end;

:: deftheorem Def3 defines sigma_locally_finite NAGATA_1:def_3_:_
 for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is sigma_locally_finite iff for n being Element of NAT holds Un . n is locally_finite );

definition
let T be non empty TopSpace;
let F be Subset-Family of T;
attrF is sigma_discrete  means :Def4: :: NAGATA_1:def 4
 ex f being sigma_discrete FamilySequence of T st F = Union f;
end;

:: deftheorem Def4 defines sigma_discrete NAGATA_1:def_4_:_
 for T being non empty TopSpace
for F being Subset-Family of T holds
( F is sigma_discrete iff ex f being sigma_discrete FamilySequence of T st F = Union f );

notation
let X be set ;
antonym  uncountable X for  countable ;
end;

registration
cluster uncountable  ->  non empty for set ;
coherence
 for b1 being set st b1 is uncountable holds
not b1 is empty ;
end;

registration
let T be non empty TopSpace;
cluster Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total sigma_locally_finite for Element of bool [:NAT,(bool (bool the carrier of T)):];
existence
 ex b1 being FamilySequence of T st b1 is sigma_locally_finite
proofend;
end;

theorem :: NAGATA_1:12
for T being non empty TopSpace
for Un being FamilySequence of T st Un is sigma_discrete holds
Un is sigma_locally_finite
proofend;

theorem :: NAGATA_1:13
for A being uncountable set ex F being Subset-Family of (1TopSp [:A,A:]) st
( F is locally_finite &amp; not F is sigma_discrete )
proofend;

definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
attrUn is Basis_sigma_discrete  means :: NAGATA_1:def 5
( Un is sigma_discrete &amp; Union Un is Basis of T );
end;

:: deftheorem  defines Basis_sigma_discrete NAGATA_1:def_5_:_
 for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is Basis_sigma_discrete iff ( Un is sigma_discrete &amp; Union Un is Basis of T ) );

definition
let T be non empty TopSpace;
let Un be FamilySequence of T;
attrUn is Basis_sigma_locally_finite  means :Def6: :: NAGATA_1:def 6
( Un is sigma_locally_finite &amp; Union Un is Basis of T );
end;

:: deftheorem Def6 defines Basis_sigma_locally_finite NAGATA_1:def_6_:_
 for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is Basis_sigma_locally_finite iff ( Un is sigma_locally_finite &amp; Union Un is Basis of T ) );

theorem Th14: :: NAGATA_1:14
for r being real number
for PM being non empty MetrSpace
for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM
proofend;

theorem :: NAGATA_1:15
for T being non empty TopSpace st T is metrizable holds
( T is regular &amp; T is T_1 )
proofend;

theorem :: NAGATA_1:16
for T being non empty TopSpace st T is metrizable holds
ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite
proofend;

Lm6:  for T being non empty TopSpace
for U being open Subset of T
for A being Subset of T st A is closed holds
U \ A is open
proofend;

theorem Th17: :: NAGATA_1:17
for T being non empty TopSpace
for U being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT holds U . n is open ) holds
Union U is open
proofend;

theorem Th18: :: NAGATA_1:18
for T being non empty TopSpace st ( for A being Subset of T
for U being open Subset of T st A is closed &amp; U is open &amp; A c= U holds
ex W being Function of NAT,(bool the carrier of T) st
( A c= Union W &amp; Union W c= U &amp; ( for n being Element of NAT holds
( Cl (W . n) c= U &amp; W . n is open ) ) ) ) holds
T is normal
proofend;

theorem Th19: :: NAGATA_1:19
for T being non empty TopSpace st T is regular holds
for Bn being FamilySequence of T st Union Bn is Basis of T holds
for U being Subset of T
for p being Point of T st U is open &amp; p in U holds
ex O being Subset of T st
( p in O &amp; Cl O c= U &amp; O in Union Bn )
proofend;

theorem :: NAGATA_1:20
for T being non empty TopSpace st T is regular &amp; ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite holds
T is normal
proofend;

Lm7:  for r being Real
for A being Point of RealSpace st r > 0 holds
A in Ball (A,r)
proofend;

definition
let T be non empty TopSpace;
let F, G be RealMap of T;
:: original:+
redefine funcF + G ->  RealMap of T means :Def7: :: NAGATA_1:def 7
 for t being Element of T holds it . t = (F . t) + (G . t);
coherence
 F + G is RealMap of T
proofend;
compatibility
 for b1 being RealMap of T holds
( b1 = F + G iff for t being Element of T holds b1 . t = (F . t) + (G . t) )
proofend;
end;

:: deftheorem Def7 defines + NAGATA_1:def_7_:_
 for T being non empty TopSpace
for F, G, b4 being RealMap of T holds
( b4 = F + G iff for t being Element of T holds b4 . t = (F . t) + (G . t) );

theorem :: NAGATA_1:21
for T being non empty TopSpace
for f being RealMap of T st f is continuous holds
for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = abs ((f . x) - (f . y)) ) holds
F is continuous
proofend;

theorem Th22: :: NAGATA_1:22
for T being non empty TopSpace
for F, G being RealMap of T st F is continuous &amp; G is continuous holds
F + G is continuous
proofend;

theorem Th23: :: NAGATA_1:23
for T being non empty TopSpace
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 &amp; ADD is commutative &amp; ADD is associative )
proofend;

theorem Th24: :: NAGATA_1:24
for T being non empty TopSpace
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
for map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds
map9 is continuous
proofend;

definition
let A, B be non empty set ;
let F be Function of A,(Funcs (A,B));
funcF Toler  ->  Function of A,B means :Def8: :: NAGATA_1:def 8
 for p being Element of A holds it . p = (F . p) . p;
existence
 ex b1 being Function of A,B st
for p being Element of A holds b1 . p = (F . p) . p
proofend;
uniqueness
 for b1, b2 being Function of A,B st ( for p being Element of A holds b1 . p = (F . p) . p ) &amp; ( for p being Element of A holds b2 . p = (F . p) . p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines Toler NAGATA_1:def_8_:_
 for A, B being non empty set
for F being Function of A,(Funcs (A,B))
for b4 being Function of A,B holds
( b4 = F Toler iff for p being Element of A holds b4 . p = (F . p) . p );

theorem :: NAGATA_1:25
for T being non empty TopSpace
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
for F being FinSequence of Funcs ( the carrier of T,REAL) st ( for n being Element of NAT st 0 <> n &amp; n <= len F holds
F . n is continuous RealMap of T ) holds
ADD "**" F is continuous RealMap of T
proofend;

theorem :: NAGATA_1:26
for T, T1 being non empty TopSpace
for F being Function of the carrier of T,(Funcs ( the carrier of T, the carrier of T1)) st ( for p being Point of T holds F . p is continuous Function of T,T1 ) holds
for S being Function of the carrier of T,(bool the carrier of T) st ( for p being Point of T holds
( p in S . p &amp; S . p is open &amp; ( for p, q being Point of T st p in S . q holds
(F . p) . p = (F . q) . p ) ) ) holds
F Toler is continuous
proofend;

definition
let X be set ;
let r be Real;
let f be Function of X,REAL;
deffunc H1( Element of X) ->  set = min (r,(f . $1));
func min (r,f) ->  Function of X,REAL means :Def9: :: NAGATA_1:def 9
 for x being set st x in X holds
it . x = min (r,(f . x));
existence
 ex b1 being Function of X,REAL st
for x being set st x in X holds
b1 . x = min (r,(f . x))
proofend;
uniqueness
 for b1, b2 being Function of X,REAL st ( for x being set st x in X holds
b1 . x = min (r,(f . x)) ) &amp; ( for x being set st x in X holds
b2 . x = min (r,(f . x)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines min NAGATA_1:def_9_:_
 for X being set
for r being Real
for f, b4 being Function of X,REAL holds
( b4 = min (r,f) iff for x being set st x in X holds
b4 . x = min (r,(f . x)) );

theorem :: NAGATA_1:27
for T being non empty TopSpace
for r being Real
for f being RealMap of T st f is continuous holds
min (r,f) is continuous
proofend;

definition
let X be set ;
let f be Function of [:X,X:],REAL;
predf is_a_pseudometric_of X means :Def10: :: NAGATA_1:def 10
( f is Reflexive &amp; f is symmetric &amp; f is triangle );
end;

:: deftheorem Def10 defines is_a_pseudometric_of NAGATA_1:def_10_:_
 for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff ( f is Reflexive &amp; f is symmetric &amp; f is triangle ) );

Lm8:  for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 &amp; f . (a,b) = f . (b,a) &amp; f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) )
proofend;

theorem Th28: :: NAGATA_1:28
for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 &amp; f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )
proofend;

Lm9:  for r being Real
for X being non empty set
for f being Function of [:X,X:],REAL
for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y)))
proofend;

theorem Th29: :: NAGATA_1:29
for X being set
for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for x, y being Element of X holds f . (x,y) >= 0
proofend;

theorem Th30: :: NAGATA_1:30
for T being non empty TopSpace
for r being Real
for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 &amp; m is_a_pseudometric_of the carrier of T holds
min (r,m) is_a_pseudometric_of the carrier of T
proofend;

theorem :: NAGATA_1:31
for T being non empty TopSpace
for r being Real
for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 &amp; m is_metric_of the carrier of T holds
min (r,m) is_metric_of the carrier of T
proofend;