:: NAGATA_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: NAGATA_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat st i > 0 holds
ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1)
proof end;

definition
func PairFunc -> Function of [:NAT ,NAT :], NAT means :Def1: :: NAGATA_2:def 1
for n, m being Nat holds it . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1;
existence
ex b1 being Function of [:NAT ,NAT :], NAT st
for n, m being Nat holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
proof end;
uniqueness
for b1, b2 being Function of [:NAT ,NAT :], NAT st ( for n, m being Nat holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Nat holds b2 . [n,m] = ((2 |^ n) * ((2 * m) + 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 n, m being Nat holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 );

theorem Th2: :: NAGATA_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
PairFunc is bijective
proof end;

definition
let X be set ;
let f be Function of [:X,X:], REAL ;
let x be Element of X;
func dist f,x -> Function of X, REAL means :Def2: :: NAGATA_2:def 2
for y being Element of X holds it . y = f . x,y;
existence
ex b1 being Function of X, REAL st
for y being Element of X holds b1 . y = f . x,y
proof end;
uniqueness
for b1, b2 being Function of X, REAL st ( for y being Element of X holds b1 . y = f . x,y ) & ( for y being Element of X holds b2 . y = f . x,y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines dist NAGATA_2:def 2 :
for X being set
for f being Function of [:X,X:], REAL
for x being Element of X
for b4 being Function of X, REAL holds
( b4 = dist f,x iff for y being Element of X holds b4 . y = f . x,y );

theorem Th3: :: NAGATA_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being non empty TopSpace
for D being Subset of [:T1,T2:] st D is open holds
for x1 being Point of T1
for x2 being Point of T2
for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 the carrier of T1,the carrier of T2) .: (D /\ [:the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 the carrier of T1,the carrier of T2) .: (D /\ [:{x1},the carrier of T2:]) implies X2 is open ) )
proof end;

theorem Th4: :: NAGATA_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for pmet being Function of [:the carrier of T,the carrier of T:], REAL st ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) holds
for x being Point of T holds dist pmet,x is continuous
proof end;

definition
let X be non empty set ;
let f be Function of [:X,X:], REAL ;
let A be Subset of X;
func inf f,A -> Function of X, REAL means :Def3: :: NAGATA_2:def 3
for x being Element of X holds it . x = inf ((dist f,x) .: A);
existence
ex b1 being Function of X, REAL st
for x being Element of X holds b1 . x = inf ((dist f,x) .: A)
proof end;
uniqueness
for b1, b2 being Function of X, REAL st ( for x being Element of X holds b1 . x = inf ((dist f,x) .: A) ) & ( for x being Element of X holds b2 . x = inf ((dist f,x) .: A) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines inf NAGATA_2:def 3 :
for X being non empty set
for f being Function of [:X,X:], REAL
for A being Subset of X
for b4 being Function of X, REAL holds
( b4 = inf f,A iff for x being Element of X holds b4 . x = inf ((dist f,x) .: A) );

Lm1: for X being non empty set
for f being Function of [:X,X:], REAL st f is_a_pseudometric_of X holds
( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below ) ) )
proof end;

theorem Th5: :: NAGATA_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being Function of [:X,X:], REAL st f is_a_pseudometric_of X holds
for A being non empty Subset of X
for x being Element of X holds (inf f,A) . x >= 0
proof end;

theorem Th6: :: NAGATA_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being Function of [:X,X:], REAL st f is_a_pseudometric_of X holds
for A being Subset of X
for x being Element of X st x in A holds
(inf f,A) . x = 0
proof end;

theorem Th7: :: NAGATA_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for pmet being Function of [:the carrier of T,the carrier of T:], REAL st pmet is_a_pseudometric_of the carrier of T holds
for x, y being Point of T
for A being non empty Subset of T holds abs (((inf pmet,A) . x) - ((inf pmet,A) . y)) <= pmet . x,y
proof end;

theorem Th8: :: NAGATA_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for pmet being Function of [:the carrier of T,the carrier of T:], REAL st pmet is_a_pseudometric_of the carrier of T & ( for p being Point of T holds dist pmet,p is continuous ) holds
for A being non empty Subset of T holds inf pmet,A is continuous
proof end;

theorem Th9: :: NAGATA_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for f being Function of [:X,X:], REAL st f is_metric_of X holds
f is_a_pseudometric_of X
proof end;

theorem Th10: :: NAGATA_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for pmet being Function of [:the carrier of T,the carrier of T:], REAL st pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (inf pmet,A) . p = 0 } ) holds
T is metrizable
proof end;

theorem Th11: :: NAGATA_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for FS2 being Functional_Sequence of [:the carrier of T,the carrier of T:], REAL st ( for n being Nat ex pmet being Function of [:the carrier of T,the carrier of T:], REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T ) ) & ( for pq being Element of [:the carrier of T,the carrier of T:] holds FS2 # pq is summable ) holds
for pmet being Function of [:the carrier of T,the carrier of T:], REAL st ( for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ) holds
pmet is_a_pseudometric_of the carrier of T
proof end;

theorem Th12: :: NAGATA_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real
for n being Nat
for seq being Real_Sequence st ( for m being Nat st m <= n holds
seq . m <= r ) holds
for m being Nat st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
proof end;

theorem Th13: :: NAGATA_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Real_Sequence
for k being Nat holds abs ((Partial_Sums seq) . k) <= (Partial_Sums (abs seq)) . k
proof end;

theorem Th14: :: NAGATA_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for FS1 being Functional_Sequence of the carrier of T, REAL st ( for n being Nat ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Nat
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) holds
for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
proof end;

theorem Th15: :: NAGATA_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for s being Real
for FS2 being Functional_Sequence of [:the carrier of T,the carrier of T:], REAL st ( for n being Nat ex pmet being Function of [:the carrier of T,the carrier of T:], REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq <= s ) & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) ) ) holds
for pmet being Function of [:the carrier of T,the carrier of T:], REAL st ( for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq ) (#) (FS2 # pq)) ) holds
( pmet is_a_pseudometric_of the carrier of T & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) )
proof end;

theorem Th16: :: NAGATA_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for pmet being Function of [:the carrier of T,the carrier of T:], REAL st pmet is_a_pseudometric_of the carrier of T & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) holds
for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(inf pmet,A) . p = 0
proof end;

theorem Th17: :: NAGATA_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is_T1 holds
for s being Real
for FS2 being Functional_Sequence of [:the carrier of T,the carrier of T:], REAL st ( for n being Nat ex pmet being Function of [:the carrier of T,the carrier of T:], REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq <= s ) & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) ) ) & ( for p being Point of T
for A' being non empty Subset of T st not p in A' & A' is closed holds
ex n being Nat st
for pmet being Function of [:the carrier of T,the carrier of T:], REAL st FS2 . n = pmet holds
(inf pmet,A') . p > 0 ) holds
( ex pmet being Function of [:the carrier of T,the carrier of T:], REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq ) (#) (FS2 # pq)) ) ) & T is metrizable )
proof end;

theorem Th18: :: NAGATA_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p, q being FinSequence of D
for B being BinOp of D st p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B has_a_unity or ( len q >= 1 & len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . (B "**" q),(B "**" r) )
proof end;

theorem Th19: :: NAGATA_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds
( ( T is_T3 & T is_T1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) iff T is metrizable )
proof end;

theorem Th20: :: NAGATA_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is metrizable holds
for FX being Subset-Family of T st FX is_a_cover_of T & FX is open holds
ex Un being FamilySequence of T st
( Union Un is open & Union Un is_a_cover_of T & Union Un is_finer_than FX & Un is sigma_discrete )
proof end;

theorem Th21: :: NAGATA_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is metrizable holds
ex Un being FamilySequence of T st Un is Basis_sigma_discrete
proof end;

theorem :: NAGATA_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds
( ( T is_T3 & T is_T1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ) iff T is metrizable )
proof end;