:: by Karol P\c{a}k

::

:: Received May 31, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

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 |.(r1 - r4).| <= (|.(r1 - r2).| + |.(r2 - r3).|) + |.(r3 - r4).|

proof 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 & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds

A = B ) ) );

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 & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds

A = B ) ) );

registration

let T be non empty TopSpace;

existence

ex b_{1} being Subset-Family of T st b_{1} is discrete

end;
existence

ex b

proof end;

registration

let T be non empty TopSpace;

existence

ex b_{1} being Subset-Family of T st

( b_{1} is empty & b_{1} is discrete )

end;
existence

ex b

( b

proof 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

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

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 by Th2, XBOOLE_1:17;

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;

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 & G is discrete & INTERSECTION (F,G) = H holds

H is discrete

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

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 )

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

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;

coherence

clf F is discrete

end;
let F be discrete Subset-Family of T;

coherence

clf F is discrete

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

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)

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

for F being Subset-Family of T st F is discrete holds

F is locally_finite

proof end;

definition
end;

definition

let T be non empty TopSpace;

let Un be FamilySequence of T;

let n be Element of NAT ;

:: original: .

redefine func Un . n -> Subset-Family of T;

coherence

Un . n is Subset-Family of T

end;
let Un be FamilySequence of T;

let n be Element of NAT ;

:: original: .

redefine func Un . n -> Subset-Family of T;

coherence

Un . n is Subset-Family of T

proof 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

end;
let Un be FamilySequence of T;

:: original: Union

redefine func Union Un -> Subset-Family of T;

coherence

Union Un is Subset-Family of T

proof end;

definition

let T be non empty TopSpace;

let Un be FamilySequence of T;

end;
let Un be FamilySequence of T;

attr Un is sigma_discrete means :Def2: :: NAGATA_1:def 2

for n being Element of NAT holds Un . n is discrete ;

for n being Element of NAT holds Un . n is discrete ;

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

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

proof end;

registration

let T be non empty TopSpace;

ex b_{1} being FamilySequence of T st b_{1} is sigma_discrete
by Lm5;

end;
cluster Relation-like omega -defined bool (bool the carrier of T) -valued Function-like non empty V14( omega ) quasi_total sigma_discrete for Element of bool [:omega,(bool (bool the carrier of T)):];

existence ex b

definition

let T be non empty TopSpace;

let Un be FamilySequence of T;

end;
let Un be FamilySequence of T;

attr Un is sigma_locally_finite means :: NAGATA_1:def 3

for n being Element of NAT holds Un . n is locally_finite ;

for n being Element of NAT holds Un . n is locally_finite ;

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

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;

end;
let F be Subset-Family of T;

attr F is sigma_discrete means :: NAGATA_1:def 4

ex f being sigma_discrete FamilySequence of T st F = Union f;

ex f being sigma_discrete FamilySequence of T st F = Union f;

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

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

registration

let T be non empty TopSpace;

ex b_{1} being FamilySequence of T st b_{1} is sigma_locally_finite

end;
cluster Relation-like omega -defined bool (bool the carrier of T) -valued Function-like non empty V14( omega ) quasi_total sigma_locally_finite for Element of bool [:omega,(bool (bool the carrier of T)):];

existence ex b

proof 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 by Th11;

for Un being FamilySequence of T st Un is sigma_discrete holds

Un is sigma_locally_finite by Th11;

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 )

( F is locally_finite & not F is sigma_discrete )

proof end;

definition

let T be non empty TopSpace;

let Un be FamilySequence of T;

end;
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 );

( Un is sigma_discrete & Union Un is Basis of T );

:: 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 & Union Un is Basis of T ) );

for T being non empty TopSpace

for Un being FamilySequence of T holds

( Un is Basis_sigma_discrete iff ( Un is sigma_discrete & Union Un is Basis of T ) );

definition

let T be non empty TopSpace;

let Un be FamilySequence of T;

end;
let Un be FamilySequence of T;

attr Un is Basis_sigma_locally_finite means :: NAGATA_1:def 6

( Un is sigma_locally_finite & Union Un is Basis of T );

( Un is sigma_locally_finite & Union Un is Basis of T );

:: deftheorem 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 & Union Un is Basis of T ) );

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 & Union Un is Basis of T ) );

theorem Th14: :: NAGATA_1:14

for r being Real

for PM being non empty MetrSpace

for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM

for PM being non empty MetrSpace

for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM

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

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 holds

U \ A is open

proof end;

theorem Th17: :: NAGATA_1:17

for T being non empty TopSpace

for U being sequence of (bool the carrier of T) st ( for n being Element of NAT holds U . n is open ) holds

Union U is open

for U being sequence of (bool the carrier of T) st ( for n being Element of 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 sequence of (bool the carrier of T) st

( A c= Union W & Union W c= U & ( for n being Element of NAT holds

( Cl (W . n) c= U & W . n is open ) ) ) ) holds

T is normal

for U being open Subset of T st A is closed & U is open & A c= U holds

ex W being sequence of (bool the carrier of T) st

( A c= Union W & Union W c= U & ( for n being Element of NAT holds

( Cl (W . n) c= U & W . n is open ) ) ) ) holds

T is normal

proof end;

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 & p in U holds

ex O being Subset of T st

( p in O & Cl O c= U & O in Union Bn )

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 regular & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite holds

T is normal

T is normal

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;

F + G is RealMap of T

for b_{1} being RealMap of T holds

( b_{1} = F + G iff for t being Element of T holds b_{1} . t = (F . t) + (G . t) )

end;
let F, G be RealMap of T;

:: original: +

redefine 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);

coherence redefine 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);

F + G is RealMap of T

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def7 defines + NAGATA_1:def 7 :

for T being non empty TopSpace

for F, G, b_{4} being RealMap of T holds

( b_{4} = F + G iff for t being Element of T holds b_{4} . t = (F . t) + (G . t) );

for T being non empty TopSpace

for F, G, b

( b

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) = |.((f . x) - (f . y)).| ) holds

F is continuous

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) = |.((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

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

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 & 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 map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds

map9 is continuous

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

proof end;

definition

let A, B be non empty set ;

let F be Function of A,(Funcs (A,B));

ex b_{1} being Function of A,B st

for p being Element of A holds b_{1} . p = (F . p) . p

for b_{1}, b_{2} being Function of A,B st ( for p being Element of A holds b_{1} . p = (F . p) . p ) & ( for p being Element of A holds b_{2} . p = (F . p) . p ) holds

b_{1} = b_{2}

end;
let F be Function of A,(Funcs (A,B));

func F Toler -> Function of A,B means :Def8: :: NAGATA_1:def 8

for p being Element of A holds it . p = (F . p) . p;

existence for p being Element of A holds it . p = (F . p) . p;

ex b

for p being Element of A holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Function of A,B holds

( b_{4} = F Toler iff for p being Element of A holds b_{4} . p = (F . p) . p );

for A, B being non empty set

for F being Function of A,(Funcs (A,B))

for b

( b

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 & n <= len F holds

F . n is continuous RealMap of T ) holds

ADD "**" F is continuous RealMap of T

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 & 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 is continuous

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 is continuous

proof end;

definition

let X be set ;

let r be Real;

let f be Function of X,REAL;

deffunc H_{1}( Element of X) -> object = min (r,(f . $1));

ex b_{1} being Function of X,REAL st

for x being set st x in X holds

b_{1} . x = min (r,(f . x))

for b_{1}, b_{2} being Function of X,REAL st ( for x being set st x in X holds

b_{1} . x = min (r,(f . x)) ) & ( for x being set st x in X holds

b_{2} . x = min (r,(f . x)) ) holds

b_{1} = b_{2}

end;
let r be Real;

let f be Function of X,REAL;

deffunc H

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 for x being set st x in X holds

it . x = min (r,(f . x));

ex b

for x being set st x in X holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines min NAGATA_1:def 9 :

for X being set

for r being Real

for f, b_{4} being Function of X,REAL holds

( b_{4} = min (r,f) iff for x being set st x in X holds

b_{4} . x = min (r,(f . x)) );

for X being set

for r being Real

for f, b

( b

b

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

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;

end;
let f be Function of [:X,X:],REAL;

pred f is_a_pseudometric_of X means :: NAGATA_1:def 10

( f is Reflexive & f is symmetric & f is triangle );

( f is Reflexive & f is symmetric & f is triangle );

:: deftheorem 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 & f is symmetric & f is triangle ) );

for X being set

for f being Function of [:X,X:],REAL holds

( f is_a_pseudometric_of X iff ( f is Reflexive & f is symmetric & 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 & 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: :: 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)) ) )

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

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

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

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;