begin
theorem Th1:
definition
func PairFunc -> Function of
[:NAT ,NAT :],
NAT means :
Def1:
for
n,
m being
Element of
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 Element of NAT holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
uniqueness
for b1, b2 being Function of [:NAT ,NAT :],NAT st ( for n, m being Element of NAT holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Element of NAT holds b2 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) holds
b1 = b2
end;
:: deftheorem Def1 defines PairFunc NAGATA_2:def 1 :
theorem Th2:
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:
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
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
end;
:: deftheorem Def2 defines dist NAGATA_2:def 2 :
theorem Th3:
theorem Th4:
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:
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)
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
end;
:: deftheorem Def3 defines inf NAGATA_2:def 3 :
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 ) ) )
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
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
Element of
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
pmet9 being
RealMap of
[:T,T:] st
pmet = pmet9 holds
pmet9 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
pmet9 being
RealMap of
[:T,T:] st
pmet = pmet9 holds
pmet9 is
continuous ) )
theorem Th16:
theorem Th17:
for
T being non
empty TopSpace st
T is
T_1 holds
for
s being
Real for
FS2 being
Functional_Sequence of
[:the carrier of T,the carrier of T:],
REAL st ( for
n being
Element of
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
pmet9 being
RealMap of
[:T,T:] st
pmet = pmet9 holds
pmet9 is
continuous ) ) ) & ( for
p being
Point of
T for
A9 being non
empty Subset of
T st not
p in A9 &
A9 is
closed holds
ex
n being
Element of
NAT st
for
pmet being
Function of
[:the carrier of T,the carrier of T:],
REAL st
FS2 . n = pmet holds
(inf pmet,A9) . 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 )
theorem Th18:
NAT = rng PairFunc
by Th2, FUNCT_2:def 3;
then Lm2:
PairFunc " = PairFunc "
by Th2, TOPS_2:def 4;
theorem Th19:
theorem Th20:
theorem Th21:
theorem