:: NAGATA_1 semantic presentation

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

proof end;

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

proof end;

definition

let T be TopSpace;
let F be Subset-Family of T;
attr F 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 & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B ) );

end;

:: deftheorem Def1 defines discrete NAGATA_1:def 1 :

registration

let T be non empty TopSpace;
cluster discrete Element of bool (bool the carrier of T);
existence

proof end;

end;

registration

let T be non empty TopSpace;
cluster empty discrete Element of bool (bool the carrier of T);
existence

proof end;

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

proof end;

theorem Th2: :: NAGATA_1:2

for T being non empty TopSpace
for F, G being Subset-Family of T st F c= G & G is discrete holds
F is discrete

proof end;

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

proof end;

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

proof end;

theorem :: NAGATA_1:5

for T being non empty TopSpace
for F, G, H being Subset-Family of T st F is discrete & G is discrete & INTERSECTION F,G = H holds
H is discrete

proof end;

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 & A in F & B in F & not A = B holds
A misses B

proof end;

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 & (INTERSECTION {O},F) \ {{} } is trivial )

proof end;

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 & (INTERSECTION {O},F) \ {{} } is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds
A misses B ) ) )

proof end;

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

proof end;

registration

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

proof end;

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)

proof end;

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 & B in F holds
Cl (A /\ B) = (Cl A) /\ (Cl B)

proof end;

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)

proof end;

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

proof end;

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 Nat;
:: original: .
redefine func Un . n -> Subset-Family of T;
coherence

proof end;

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

proof end;

end;

definition

let T be non empty TopSpace;
let Un be FamilySequence of T;
attr Un is sigma_discrete means :Def2: :: NAGATA_1:def 2
for n being Nat holds Un . n is discrete;

end;

:: 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

proof end;

registration

let T be non empty TopSpace;
cluster sigma_discrete Relation of NAT , bool (bool the carrier 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 :Def3: :: NAGATA_1:def 3
for n being Nat holds Un . n is locally_finite;

end;

:: deftheorem Def3 defines sigma_locally_finite NAGATA_1:def 3 :

definition

let T be non empty TopSpace;
let F be Subset-Family of T;
attr F 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 :

notation

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

end;

registration

cluster uncountable -> non empty set ;
coherence by CARD_4:def 1;

end;

registration

let T be non empty TopSpace;
cluster sigma_locally_finite Relation of NAT , bool (bool the carrier of T);
existence

proof end;

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

proof end;

theorem :: NAGATA_1:13

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

proof end;

definition

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

end;

:: deftheorem defines Basis_sigma_discrete NAGATA_1:def 5 :

definition

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

end;

:: deftheorem Def6 defines Basis_sigma_locally_finite NAGATA_1:def 6 :

theorem Th14: :: NAGATA_1:14

for PM being non empty MetrStruct
for r being real number st PM is non empty MetrSpace holds
for x being Element of PM holds ([#] PM) \ (cl_Ball x,r) in Family_open_set PM

proof end;

theorem :: NAGATA_1:15

for T being non empty TopSpace st T is metrizable holds
( T is_T3 & T is_T1 )

proof end;

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

proof end;

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

proof end;

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 Nat holds U . n is open ) holds
Union U is open

proof end;

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 & U is open & A c= U holds
ex W being Function of NAT , bool the carrier of T st
( A c= Union W & Union W c= U & ( for n being Nat holds
( Cl (W . n) c= U & W . n is open ) ) ) ) holds
T is_T4

proof end;

theorem Th19: :: NAGATA_1:19

for T being non empty TopSpace st T is_T3 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 & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )

proof end;

theorem :: NAGATA_1:20

for T being non empty TopSpace st T is_T3 & T is_T1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite holds
T is_T4

proof end;

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

proof end;

definition

let T be non empty TopSpace;
let F, G be RealMap of T;
deffunc H₁( Element of T) -> Element of REAL = (F . $1) + (G . $1);
func F + G -> RealMap of T means :Def7: :: NAGATA_1:def 7
for t being Element of T holds it . t = (F . t) + (G . t);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines + NAGATA_1:def 7 :

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

proof end;

theorem Th22: :: NAGATA_1:22

for T being non empty TopSpace
for F, G being RealMap of T st F is continuous & G is continuous holds
F + G is continuous

proof end;

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 has_a_unity & ADD is commutative & ADD is associative )

proof end;

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 map' being Element of Funcs the carrier of T,REAL st map' is_a_unity_wrt ADD holds
map' is continuous

proof end;

definition

let T, T1 be non empty TopSpace;
let Sub be Function of the carrier of T, bool the carrier of T;
let Fun be Function of the carrier of T, Funcs the carrier of T,the carrier of T1;
func Fun Toler Sub -> Function of T,T1 means :Def8: :: NAGATA_1:def 8
for p being Point of T holds it . p = (Fun . p) . p;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Toler NAGATA_1:def 8 :

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 Nat st 0 <> n & n <= len F holds
F . n is continuous RealMap of T ) holds
ADD "**" F is continuous RealMap of T

proof end;

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 & S . p is open & ( for p, q being Point of T st p in S . q holds
(F . p) . p = (F . q) . p ) ) ) holds
F Toler S is continuous

proof end;

definition

let X be set ;
let r be Real;
let f be Function of X, REAL ;
deffunc H₁( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines min NAGATA_1:def 9 :

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

proof end;

definition

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

end;

:: 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) ) )

proof end;

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 & f . a,c <= (f . a,b) + (f . c,b) ) )

proof end;

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)

proof end;

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

proof end;

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 & m is_a_pseudometric_of the carrier of T holds
min r,m is_a_pseudometric_of the carrier of T

proof end;

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 & m is_metric_of the carrier of T holds
min r,m is_metric_of the carrier of T

proof end;