begin
Lm1:
for r, s, t being Real st r >= 0 & s >= 0 & r + s < t holds
( r < t & s < t )
Lm2:
for r1, r2, r3, r4 being Real holds abs (r1 - r4) <= ((abs (r1 - r2)) + (abs (r2 - r3))) + (abs (r3 - r4))
:: deftheorem Def1 defines discrete NAGATA_1:def 1 :
theorem Th1:
theorem Th2:
theorem
theorem
theorem
theorem Th6:
theorem Th7:
theorem
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
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)
theorem
theorem
theorem Th11:
:: deftheorem Def2 defines sigma_discrete NAGATA_1:def 2 :
Lm5:
for T being non empty TopSpace ex Un being FamilySequence of T st Un is sigma_discrete
:: deftheorem Def3 defines sigma_locally_finite NAGATA_1:def 3 :
:: deftheorem Def4 defines sigma_discrete NAGATA_1:def 4 :
theorem
theorem
:: deftheorem defines Basis_sigma_discrete NAGATA_1:def 5 :
:: deftheorem Def6 defines Basis_sigma_locally_finite NAGATA_1:def 6 :
theorem Th14:
theorem
theorem
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
theorem Th17:
theorem Th18:
theorem Th19:
theorem
Lm7:
for r being Real
for A being Point of RealSpace st r > 0 holds
A in Ball A,r
:: deftheorem Def7 defines + NAGATA_1:def 7 :
theorem
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem Def8 defines Toler NAGATA_1:def 8 :
theorem
theorem
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:
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)
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) ) & ( for x being set st x in X holds
b2 . x = min r,(f . x) ) holds
b1 = b2
end;
:: deftheorem Def9 defines min NAGATA_1:def 9 :
theorem
:: deftheorem Def10 defines is_a_pseudometric_of NAGATA_1:def 10 :
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 & f . a,b = f . b,a & f . a,c <= (f . a,b) + (f . b,c) ) )
theorem Th28:
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)
theorem Th29:
theorem Th30:
theorem