:: NAGATA_2 semantic presentation

theorem Th1: :: NAGATA_2:1
for b1 being Nat st b1 > 0 holds
ex b2, b3 being Nat st b1 = (2 |^ b2) * ((2 * b3) + 1)
proof end;

definition
func PairFunc -> Function of [:NAT ,NAT :], NAT means :Def1: :: NAGATA_2:def 1
for b1, b2 being Nat holds a1 . [b1,b2] = ((2 |^ b1) * ((2 * b2) + 1)) - 1;
existence
ex b1 being Function of [:NAT ,NAT :], NAT st
for b2, b3 being Nat holds b1 . [b2,b3] = ((2 |^ b2) * ((2 * b3) + 1)) - 1
proof end;
uniqueness
for b1, b2 being Function of [:NAT ,NAT :], NAT st ( for b3, b4 being Nat holds b1 . [b3,b4] = ((2 |^ b3) * ((2 * b4) + 1)) - 1 ) & ( for b3, b4 being Nat holds b2 . [b3,b4] = ((2 |^ b3) * ((2 * b4) + 1)) - 1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines PairFunc NAGATA_2:def 1 :
for b1 being Function of [:NAT ,NAT :], NAT holds
( b1 = PairFunc iff for b2, b3 being Nat holds b1 . [b2,b3] = ((2 |^ b2) * ((2 * b3) + 1)) - 1 );

theorem Th2: :: NAGATA_2:2
PairFunc is bijective
proof end;

definition
let c1 be set ;
let c2 be Function of [:c1,c1:], REAL ;
let c3 be Element of c1;
func dist c2,c3 -> Function of a1, REAL means :Def2: :: NAGATA_2:def 2
for b1 being Element of a1 holds a4 . b1 = a2 . a3,b1;
existence
ex b1 being Function of c1, REAL st
for b2 being Element of c1 holds b1 . b2 = c2 . c3,b2
proof end;
uniqueness
for b1, b2 being Function of c1, REAL st ( for b3 being Element of c1 holds b1 . b3 = c2 . c3,b3 ) & ( for b3 being Element of c1 holds b2 . b3 = c2 . c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines dist NAGATA_2:def 2 :
for b1 being set
for b2 being Function of [:b1,b1:], REAL
for b3 being Element of b1
for b4 being Function of b1, REAL holds
( b4 = dist b2,b3 iff for b5 being Element of b1 holds b4 . b5 = b2 . b3,b5 );

theorem Th3: :: NAGATA_2:3
for b1, b2 being non empty TopSpace
for b3 being Subset of [:b1,b2:] st b3 is open holds
for b4 being Point of b1
for b5 being Point of b2
for b6 being Subset of b1
for b7 being Subset of b2 holds
( ( b6 = (pr1 the carrier of b1,the carrier of b2) .: (b3 /\ [:the carrier of b1,{b5}:]) implies b6 is open ) & ( b7 = (pr2 the carrier of b1,the carrier of b2) .: (b3 /\ [:{b4},the carrier of b2:]) implies b7 is open ) )
proof end;

theorem Th4: :: NAGATA_2:4
for b1 being non empty TopSpace
for b2 being Function of [:the carrier of b1,the carrier of b1:], REAL st ( for b3 being RealMap of [:b1,b1:] st b2 = b3 holds
b3 is continuous ) holds
for b3 being Point of b1 holds dist b2,b3 is continuous
proof end;

definition
let c1 be non empty set ;
let c2 be Function of [:c1,c1:], REAL ;
let c3 be Subset of c1;
func inf c2,c3 -> Function of a1, REAL means :Def3: :: NAGATA_2:def 3
for b1 being Element of a1 holds a4 . b1 = inf ((dist a2,b1) .: a3);
existence
ex b1 being Function of c1, REAL st
for b2 being Element of c1 holds b1 . b2 = inf ((dist c2,b2) .: c3)
proof end;
uniqueness
for b1, b2 being Function of c1, REAL st ( for b3 being Element of c1 holds b1 . b3 = inf ((dist c2,b3) .: c3) ) & ( for b3 being Element of c1 holds b2 . b3 = inf ((dist c2,b3) .: c3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines inf NAGATA_2:def 3 :
for b1 being non empty set
for b2 being Function of [:b1,b1:], REAL
for b3 being Subset of b1
for b4 being Function of b1, REAL holds
( b4 = inf b2,b3 iff for b5 being Element of b1 holds b4 . b5 = inf ((dist b2,b5) .: b3) );

Lemma8: for b1 being non empty set
for b2 being Function of [:b1,b1:], REAL st b2 is_a_pseudometric_of b1 holds
( b2 is bounded_below & ( for b3 being non empty Subset of b1
for b4 being Element of b1 holds
( not (dist b2,b4) .: b3 is empty & (dist b2,b4) .: b3 is bounded_below ) ) )
proof end;

theorem Th5: :: NAGATA_2:5
for b1 being non empty set
for b2 being Function of [:b1,b1:], REAL st b2 is_a_pseudometric_of b1 holds
for b3 being non empty Subset of b1
for b4 being Element of b1 holds (inf b2,b3) . b4 >= 0
proof end;

theorem Th6: :: NAGATA_2:6
for b1 being non empty set
for b2 being Function of [:b1,b1:], REAL st b2 is_a_pseudometric_of b1 holds
for b3 being Subset of b1
for b4 being Element of b1 st b4 in b3 holds
(inf b2,b3) . b4 = 0
proof end;

theorem Th7: :: NAGATA_2:7
for b1 being non empty TopSpace
for b2 being Function of [:the carrier of b1,the carrier of b1:], REAL st b2 is_a_pseudometric_of the carrier of b1 holds
for b3, b4 being Point of b1
for b5 being non empty Subset of b1 holds abs (((inf b2,b5) . b3) - ((inf b2,b5) . b4)) <= b2 . b3,b4
proof end;

theorem Th8: :: NAGATA_2:8
for b1 being non empty TopSpace
for b2 being Function of [:the carrier of b1,the carrier of b1:], REAL st b2 is_a_pseudometric_of the carrier of b1 & ( for b3 being Point of b1 holds dist b2,b3 is continuous ) holds
for b3 being non empty Subset of b1 holds inf b2,b3 is continuous
proof end;

theorem Th9: :: NAGATA_2:9
for b1 being set
for b2 being Function of [:b1,b1:], REAL st b2 is_metric_of b1 holds
b2 is_a_pseudometric_of b1
proof end;

theorem Th10: :: NAGATA_2:10
for b1 being non empty TopSpace
for b2 being Function of [:the carrier of b1,the carrier of b1:], REAL st b2 is_metric_of the carrier of b1 & ( for b3 being non empty Subset of b1 holds Cl b3 = { b4 where B is Point of b1 : (inf b2,b3) . b4 = 0 } ) holds
b1 is metrizable
proof end;

theorem Th11: :: NAGATA_2:11
for b1 being non empty TopSpace
for b2 being Functional_Sequence of [:the carrier of b1,the carrier of b1:], REAL st ( for b3 being Nat ex b4 being Function of [:the carrier of b1,the carrier of b1:], REAL st
( b2 . b3 = b4 & b4 is_a_pseudometric_of the carrier of b1 ) ) & ( for b3 being Element of [:the carrier of b1,the carrier of b1:] holds b2 # b3 is summable ) holds
for b3 being Function of [:the carrier of b1,the carrier of b1:], REAL st ( for b4 being Element of [:the carrier of b1,the carrier of b1:] holds b3 . b4 = Sum (b2 # b4) ) holds
b3 is_a_pseudometric_of the carrier of b1
proof end;

theorem Th12: :: NAGATA_2:12
for b1 being Real
for b2 being Nat
for b3 being Real_Sequence st ( for b4 being Nat st b4 <= b2 holds
b3 . b4 <= b1 ) holds
for b4 being Nat st b4 <= b2 holds
(Partial_Sums b3) . b4 <= b1 * (b4 + 1)
proof end;

theorem Th13: :: NAGATA_2:13
for b1 being Real_Sequence
for b2 being Nat holds abs ((Partial_Sums b1) . b2) <= (Partial_Sums (abs b1)) . b2
proof end;

theorem Th14: :: NAGATA_2:14
for b1 being non empty TopSpace
for b2 being Functional_Sequence of the carrier of b1, REAL st ( for b3 being Nat ex b4 being RealMap of b1 st
( b2 . b3 = b4 & b4 is continuous & ( for b5 being Point of b1 holds b4 . b5 >= 0 ) ) ) & ex b3 being Real_Sequence st
( b3 is summable & ( for b4 being Nat
for b5 being Point of b1 holds (b2 # b5) . b4 <= b3 . b4 ) ) holds
for b3 being RealMap of b1 st ( for b4 being Point of b1 holds b3 . b4 = Sum (b2 # b4) ) holds
b3 is continuous
proof end;

theorem Th15: :: NAGATA_2:15
for b1 being non empty TopSpace
for b2 being Real
for b3 being Functional_Sequence of [:the carrier of b1,the carrier of b1:], REAL st ( for b4 being Nat ex b5 being Function of [:the carrier of b1,the carrier of b1:], REAL st
( b3 . b4 = b5 & b5 is_a_pseudometric_of the carrier of b1 & ( for b6 being Element of [:the carrier of b1,the carrier of b1:] holds b5 . b6 <= b2 ) & ( for b6 being RealMap of [:b1,b1:] st b5 = b6 holds
b6 is continuous ) ) ) holds
for b4 being Function of [:the carrier of b1,the carrier of b1:], REAL st ( for b5 being Element of [:the carrier of b1,the carrier of b1:] holds b4 . b5 = Sum (((1 / 2) GeoSeq ) (#) (b3 # b5)) ) holds
( b4 is_a_pseudometric_of the carrier of b1 & ( for b5 being RealMap of [:b1,b1:] st b4 = b5 holds
b5 is continuous ) )
proof end;

theorem Th16: :: NAGATA_2:16
for b1 being non empty TopSpace
for b2 being Function of [:the carrier of b1,the carrier of b1:], REAL st b2 is_a_pseudometric_of the carrier of b1 & ( for b3 being RealMap of [:b1,b1:] st b2 = b3 holds
b3 is continuous ) holds
for b3 being non empty Subset of b1
for b4 being Point of b1 st b4 in Cl b3 holds
(inf b2,b3) . b4 = 0
proof end;

theorem Th17: :: NAGATA_2:17
for b1 being non empty TopSpace st b1 is_T1 holds
for b2 being Real
for b3 being Functional_Sequence of [:the carrier of b1,the carrier of b1:], REAL st ( for b4 being Nat ex b5 being Function of [:the carrier of b1,the carrier of b1:], REAL st
( b3 . b4 = b5 & b5 is_a_pseudometric_of the carrier of b1 & ( for b6 being Element of [:the carrier of b1,the carrier of b1:] holds b5 . b6 <= b2 ) & ( for b6 being RealMap of [:b1,b1:] st b5 = b6 holds
b6 is continuous ) ) ) & ( for b4 being Point of b1
for b5 being non empty Subset of b1 st not b4 in b5 & b5 is closed holds
ex b6 being Nat st
for b7 being Function of [:the carrier of b1,the carrier of b1:], REAL st b3 . b6 = b7 holds
(inf b7,b5) . b4 > 0 ) holds
( ex b4 being Function of [:the carrier of b1,the carrier of b1:], REAL st
( b4 is_metric_of the carrier of b1 & ( for b5 being Element of [:the carrier of b1,the carrier of b1:] holds b4 . b5 = Sum (((1 / 2) GeoSeq ) (#) (b3 # b5)) ) ) & b1 is metrizable )
proof end;

theorem Th18: :: NAGATA_2:18
for b1 being non empty set
for b2, b3 being FinSequence of b1
for b4 being BinOp of b1 st b2 is one-to-one & b3 is one-to-one & rng b3 c= rng b2 & b4 is commutative & b4 is associative & ( b4 has_a_unity or ( len b3 >= 1 & len b2 > len b3 ) ) holds
ex b5 being FinSequence of b1 st
( b5 is one-to-one & rng b5 = (rng b2) \ (rng b3) & b4 "**" b2 = b4 . (b4 "**" b3),(b4 "**" b5) )
proof end;

theorem Th19: :: NAGATA_2:19
for b1 being non empty TopSpace holds
( ( b1 is_T3 & b1 is_T1 & ex b2 being FamilySequence of b1 st b2 is Basis_sigma_locally_finite ) iff b1 is metrizable )
proof end;

theorem Th20: :: NAGATA_2:20
for b1 being non empty TopSpace st b1 is metrizable holds
for b2 being Subset-Family of b1 st b2 is_a_cover_of b1 & b2 is open holds
ex b3 being FamilySequence of b1 st
( Union b3 is open & Union b3 is_a_cover_of b1 & Union b3 is_finer_than b2 & b3 is sigma_discrete )
proof end;

theorem Th21: :: NAGATA_2:21
for b1 being non empty TopSpace st b1 is metrizable holds
ex b2 being FamilySequence of b1 st b2 is Basis_sigma_discrete
proof end;

theorem Th22: :: NAGATA_2:22
for b1 being non empty TopSpace holds
( ( b1 is_T3 & b1 is_T1 & ex b2 being FamilySequence of b1 st b2 is Basis_sigma_discrete ) iff b1 is metrizable )
proof end;