:: NAGATA_1 semantic presentation

Lemma1: for b₁, b₂, b₃ being Real st b₁ >= 0 & b₂ >= 0 & b₁ + b₂ < b₃ holds
( b₁ < b₃ & b₂ < b₃ )

proof end;

Lemma2: for b₁, b₂, b₃, b₄ being Real holds abs (b₁ - b₄) <= ((abs (b₁ - b₂)) + (abs (b₂ - b₃))) + (abs (b₃ - b₄))

proof end;

definition

let c₁ be TopSpace;
let c₂ be Subset-Family of c₁;
attr a₂ is discrete means :Def1: :: NAGATA_1:def 1
for b₁ being Point of a₁ ex b₂ being open Subset of a₁ st
( b₁ in b₂ & ( for b₃, b₄ being Subset of a₁ st b₃ in a₂ & b₄ in a₂ & b₂ meets b₃ & b₂ meets b₄ holds
b₃ = b₄ ) );

end;

:: deftheorem Def1 defines discrete NAGATA_1:def 1 :

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem Th1: :: NAGATA_1:1

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st ex b₃ being Subset of b₁ st b₂ = {b₃} holds
b₂ is discrete

proof end;

theorem Th2: :: NAGATA_1:2

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ & b₃ is discrete holds
b₂ is discrete

proof end;

theorem Th3: :: NAGATA_1:3

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is discrete holds
b₂ /\ b₃ is discrete

proof end;

theorem Th4: :: NAGATA_1:4

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is discrete holds
b₂ \ b₃ is discrete

proof end;

theorem Th5: :: NAGATA_1:5

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Subset-Family of b₁ st b₂ is discrete & b₃ is discrete & INTERSECTION b₂,b₃ = b₄ holds
b₄ is discrete

proof end;

theorem Th6: :: NAGATA_1:6

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁
for b₃, b₄ being Subset of b₁ st b₂ is discrete & b₃ in b₂ & b₄ in b₂ & not b₃ = b₄ holds
b₃ misses b₄

proof end;

theorem Th7: :: NAGATA_1:7

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is discrete holds
for b₃ being Point of b₁ ex b₄ being open Subset of b₁ st
( b₃ in b₄ & (INTERSECTION {b₄},b₂) \ {{} } is trivial )

proof end;

theorem Th8: :: NAGATA_1:8

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ holds
( b₂ is discrete iff ( ( for b₃ being Point of b₁ ex b₄ being open Subset of b₁ st
( b₃ in b₄ & (INTERSECTION {b₄},b₂) \ {{} } is trivial ) ) & ( for b₃, b₄ being Subset of b₁ st b₃ in b₂ & b₄ in b₂ & not b₃ = b₄ holds
b₃ misses b₄ ) ) )

proof end;

Lemma8: for b₁ being non empty TopSpace
for b₂ being open Subset of b₁
for b₃ being Subset of b₁ st b₂ meets Cl b₃ holds
b₂ meets b₃

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be discrete Subset-Family of c₁;
cluster clf a₂ -> discrete ;
coherence

proof end;

end;

Lemma9: for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₁ st b₃ in b₂ holds
Cl b₃ c= Cl (union b₂)

proof end;

theorem Th9: :: NAGATA_1:9

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is discrete holds
for b₃, b₄ being Subset of b₁ st b₃ in b₂ & b₄ in b₂ holds
Cl (b₃ /\ b₄) = (Cl b₃) /\ (Cl b₄)

proof end;

theorem Th10: :: NAGATA_1:10

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is discrete holds
Cl (union b₂) = union (clf b₂)

proof end;

theorem Th11: :: NAGATA_1:11

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is discrete holds
b₂ is locally_finite

proof end;

definition

let c₁ be TopSpace;
mode FamilySequence of a₁ is Function of NAT , bool (bool the carrier of a₁);

end;

definition

let c₁ be non empty TopSpace;
let c₂ be FamilySequence of c₁;
let c₃ be Nat;
redefine func . as c₂ . c₃ -> Subset-Family of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be FamilySequence of c₁;
redefine func Union as Union c₂ -> Subset-Family of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be FamilySequence of c₁;
attr a₂ is sigma_discrete means :Def2: :: NAGATA_1:def 2
for b₁ being Nat holds a₂ . b₁ is discrete;

end;

:: deftheorem Def2 defines sigma_discrete NAGATA_1:def 2 :

Lemma12: for b₁ being non empty TopSpace ex b₂ being FamilySequence of b₁ st b₂ is sigma_discrete

proof end;

registration

let c₁ be non empty TopSpace;
cluster sigma_discrete Relation of NAT , bool (bool the carrier of a₁);
existence by Lemma12;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be FamilySequence of c₁;
attr a₂ is sigma_locally_finite means :Def3: :: NAGATA_1:def 3
for b₁ being Nat holds a₂ . b₁ is locally_finite;

end;

:: deftheorem Def3 defines sigma_locally_finite NAGATA_1:def 3 :

definition

let c₁ be non empty TopSpace;
let c₂ be Subset-Family of c₁;
attr a₂ is sigma_discrete means :Def4: :: NAGATA_1:def 4
ex b₁ being sigma_discrete FamilySequence of a₁ st a₂ = Union b₁;

end;

:: deftheorem Def4 defines sigma_discrete NAGATA_1:def 4 :

notation

let c₁ be set ;
antonym uncountable c₁ for countable c₁;

end;

registration

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

end;

registration

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

proof end;

end;

theorem Th12: :: NAGATA_1:12

for b₁ being non empty TopSpace
for b₂ being FamilySequence of b₁ st b₂ is sigma_discrete holds
b₂ is sigma_locally_finite

proof end;

theorem Th13: :: NAGATA_1:13

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

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be FamilySequence of c₁;
attr a₂ is Basis_sigma_discrete means :: NAGATA_1:def 5
( a₂ is sigma_discrete & Union a₂ is Basis of a₁ );

end;

:: deftheorem Def5 defines Basis_sigma_discrete NAGATA_1:def 5 :

definition

let c₁ be non empty TopSpace;
let c₂ be FamilySequence of c₁;
attr a₂ is Basis_sigma_locally_finite means :Def6: :: NAGATA_1:def 6
( a₂ is sigma_locally_finite & Union a₂ is Basis of a₁ );

end;

:: deftheorem Def6 defines Basis_sigma_locally_finite NAGATA_1:def 6 :

theorem Th14: :: NAGATA_1:14

for b₁ being non empty MetrStruct
for b₂ being real number st b₁ is non empty MetrSpace holds
for b₃ being Element of b₁ holds ([#] b₁) \ (cl_Ball b₃,b₂) in Family_open_set b₁

proof end;

theorem Th15: :: NAGATA_1:15

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

proof end;

theorem Th16: :: NAGATA_1:16

for b₁ being non empty TopSpace st b₁ is metrizable holds
ex b₂ being FamilySequence of b₁ st b₂ is Basis_sigma_locally_finite

proof end;

Lemma17: for b₁ being non empty TopSpace
for b₂ being open Subset of b₁
for b₃ being Subset of b₁ st b₃ is closed & b₂ is open holds
b₂ \ b₃ is open

proof end;

theorem Th17: :: NAGATA_1:17

for b₁ being non empty TopSpace
for b₂ being Function of NAT , bool the carrier of b₁ st ( for b₃ being Nat holds b₂ . b₃ is open ) holds
Union b₂ is open

proof end;

theorem Th18: :: NAGATA_1:18

for b₁ being non empty TopSpace st ( for b₂ being Subset of b₁
for b₃ being open Subset of b₁ st b₂ is closed & b₃ is open & b₂ c= b₃ holds
ex b₄ being Function of NAT , bool the carrier of b₁ st
( b₂ c= Union b₄ & Union b₄ c= b₃ & ( for b₅ being Nat holds
( Cl (b₄ . b₅) c= b₃ & b₄ . b₅ is open ) ) ) ) holds
b₁ is_T4

proof end;

theorem Th19: :: NAGATA_1:19

for b₁ being non empty TopSpace st b₁ is_T3 holds
for b₂ being FamilySequence of b₁ st Union b₂ is Basis of b₁ holds
for b₃ being Subset of b₁
for b₄ being Point of b₁ st b₃ is open & b₄ in b₃ holds
ex b₅ being Subset of b₁ st
( b₄ in b₅ & Cl b₅ c= b₃ & b₅ in Union b₂ )

proof end;

theorem Th20: :: NAGATA_1:20

for b₁ being non empty TopSpace st b₁ is_T3 & b₁ is_T1 & ex b₂ being FamilySequence of b₁ st b₂ is Basis_sigma_locally_finite holds
b₁ is_T4

proof end;

Lemma21: for b₁ being Real
for b₂ being Point of RealSpace st b₁ > 0 holds
b₂ in Ball b₂,b₁

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be RealMap of c₁;
deffunc H₁( Element of c₁) -> Element of REAL = (c₂ . a₁) + (c₃ . a₁);
func c₂ + c₃ -> RealMap of a₁ means :Def7: :: NAGATA_1:def 7
for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines + NAGATA_1:def 7 :

theorem Th21: :: NAGATA_1:21

for b₁ being non empty TopSpace
for b₂ being RealMap of b₁ st b₂ is continuous holds
for b₃ being RealMap of [:b₁,b₁:] st ( for b₄, b₅ being Element of b₁ holds b₃ . [b₄,b₅] = abs ((b₂ . b₄) - (b₂ . b₅)) ) holds
b₃ is continuous

proof end;

theorem Th22: :: NAGATA_1:22

for b₁ being non empty TopSpace
for b₂, b₃ being RealMap of b₁ st b₂ is continuous & b₃ is continuous holds
b₂ + b₃ is continuous

proof end;

theorem Th23: :: NAGATA_1:23

for b₁ being non empty TopSpace
for b₂ being BinOp of Funcs the carrier of b₁,REAL st ( for b₃, b₄ being RealMap of b₁ holds b₂ . b₃,b₄ = b₃ + b₄ ) holds
( b₂ has_a_unity & b₂ is commutative & b₂ is associative )

proof end;

theorem Th24: :: NAGATA_1:24

for b₁ being non empty TopSpace
for b₂ being BinOp of Funcs the carrier of b₁,REAL st ( for b₃, b₄ being RealMap of b₁ holds b₂ . b₃,b₄ = b₃ + b₄ ) holds
for b₃ being Element of Funcs the carrier of b₁,REAL st b₃ is_a_unity_wrt b₂ holds
b₃ is continuous

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Function of the carrier of c₁, bool the carrier of c₁;
let c₄ be Function of the carrier of c₁, Funcs the carrier of c₁,the carrier of c₂;
func c₄ Toler c₃ -> Function of a₁,a₂ means :Def8: :: NAGATA_1:def 8
for b₁ being Point of a₁ holds a₅ . b₁ = (a₄ . b₁) . b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Toler NAGATA_1:def 8 :

theorem Th25: :: NAGATA_1:25

for b₁ being non empty TopSpace
for b₂ being BinOp of Funcs the carrier of b₁,REAL st ( for b₃, b₄ being RealMap of b₁ holds b₂ . b₃,b₄ = b₃ + b₄ ) holds
for b₃ being FinSequence of Funcs the carrier of b₁,REAL st ( for b₄ being Nat st 0 <> b₄ & b₄ <= len b₃ holds
b₃ . b₄ is continuous RealMap of b₁ ) holds
b₂ "**" b₃ is continuous RealMap of b₁

proof end;

theorem Th26: :: NAGATA_1:26

for b₁, b₂ being non empty TopSpace
for b₃ being Function of the carrier of b₁, Funcs the carrier of b₁,the carrier of b₂ st ( for b₄ being Point of b₁ holds b₃ . b₄ is continuous Function of b₁,b₂ ) holds
for b₄ being Function of the carrier of b₁, bool the carrier of b₁ st ( for b₅ being Point of b₁ holds
( b₅ in b₄ . b₅ & b₄ . b₅ is open & ( for b₆, b₇ being Point of b₁ st b₆ in b₄ . b₇ holds
(b₃ . b₆) . b₆ = (b₃ . b₇) . b₆ ) ) ) holds
b₃ Toler b₄ is continuous

proof end;

definition

let c₁ be set ;
let c₂ be Real;
let c₃ be Function of c₁, REAL ;
deffunc H₁( Element of c₁) -> set = min c₂,(c₃ . a₁);
func min c₂,c₃ -> Function of a₁, REAL means :Def9: :: NAGATA_1:def 9
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = min a₂,(a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines min NAGATA_1:def 9 :

theorem Th27: :: NAGATA_1:27

for b₁ being non empty TopSpace
for b₂ being Real
for b₃ being RealMap of b₁ st b₃ is continuous holds
min b₂,b₃ is continuous

proof end;

definition

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

end;

:: deftheorem Def10 defines is_a_pseudometric_of NAGATA_1:def 10 :

Lemma29: for b₁ being set
for b₂ being Function of [:b₁,b₁:], REAL holds
( b₂ is_a_pseudometric_of b₁ iff for b₃, b₄, b₅ being Element of b₁ holds
( b₂ . b₃,b₃ = 0 & b₂ . b₃,b₄ = b₂ . b₄,b₃ & b₂ . b₃,b₅ <= (b₂ . b₃,b₄) + (b₂ . b₄,b₅) ) )

proof end;

theorem Th28: :: NAGATA_1:28

for b₁ being set
for b₂ being Function of [:b₁,b₁:], REAL holds
( b₂ is_a_pseudometric_of b₁ iff for b₃, b₄, b₅ being Element of b₁ holds
( b₂ . b₃,b₃ = 0 & b₂ . b₃,b₅ <= (b₂ . b₃,b₄) + (b₂ . b₅,b₄) ) )

proof end;

Lemma31: for b₁ being Real
for b₂ being non empty set
for b₃ being Function of [:b₂,b₂:], REAL
for b₄, b₅ being Element of b₂ holds (min b₁,b₃) . b₄,b₅ = min b₁,(b₃ . b₄,b₅)

proof end;

theorem Th29: :: NAGATA_1:29

for b₁ being set
for b₂ being Function of [:b₁,b₁:], REAL st b₂ is_a_pseudometric_of b₁ holds
for b₃, b₄ being Element of b₁ holds b₂ . b₃,b₄ >= 0

proof end;

theorem Th30: :: NAGATA_1:30

for b₁ being non empty TopSpace
for b₂ being Real
for b₃ being Function of [:the carrier of b₁,the carrier of b₁:], REAL st b₂ > 0 & b₃ is_a_pseudometric_of the carrier of b₁ holds
min b₂,b₃ is_a_pseudometric_of the carrier of b₁

proof end;

theorem Th31: :: NAGATA_1:31

for b₁ being non empty TopSpace
for b₂ being Real
for b₃ being Function of [:the carrier of b₁,the carrier of b₁:], REAL st b₂ > 0 & b₃ is_metric_of the carrier of b₁ holds
min b₂,b₃ is_metric_of the carrier of b₁

proof end;