nagata_2.miz
begin
reserve i,k,m,n for
Nat,
r,s for
Real,
rn for
Real,
x,y,z,X for
set,
T,T1,T2 for non
empty
TopSpace,
p,q for
Point of T,
A,B,C for
Subset of T,
A9 for non
empty
Subset of T,
pq for
Element of
[:the
carrier of T, the
carrier of T:],
pq9 for
Point of
[:T, T:],
pmet,pmet1 for
Function of
[:the
carrier of T, the
carrier of T:],
REAL ,
pmet9,pmet19 for
RealMap of
[:T, T:],
f,f1 for
RealMap of T,
FS2 for
Functional_Sequence of
[:the
carrier of T, the
carrier of T:],
REAL ,
seq for
Real_Sequence;
theorem ::
NAGATA_2:1
Th1: for i st i
>
0 holds ex n, m st i
= ((2
|^ n)
* ((2
* m)
+ 1))
proof
defpred
N[
Nat] means for k st 1
<= k & k
<= $1 holds ex n, m st k
= ((2
|^ n)
* ((2
* m)
+ 1));
A1: for i st
N[i] holds
N[(i
+ 1)]
proof
let i such that
A2:
N[i];
let k such that
A3: 1
<= k and
A4: k
<= (i
+ 1);
now
per cases by
A4,
XXREAL_0: 1;
suppose
A5: k
= (i
+ 1) & i
=
0 ;
set m =
0 ;
A6: 1
= (2
|^
0 ) by
NEWTON: 4;
k
= (1
* ((m
* 2)
+ 1)) by
A5;
hence thesis by
A6;
end;
suppose
A7: k
= (i
+ 1) & i
>
0 ;
per cases by
NAT_D: 12;
suppose (k
mod 2)
= 1;
then
consider m be
Nat such that
A8: k
= ((2
* m)
+ 1) and 1
< 2 by
NAT_D:def 2;
reconsider m as
Element of
NAT by
ORDINAL1:def 12;
1
= (2
|^
0 ) by
NEWTON: 4;
then k
= ((2
|^
0 )
* ((2
* m)
+ 1)) by
A8;
hence thesis;
end;
suppose (k
mod 2)
=
0 ;
then
consider j be
Nat such that
A9: k
= ((2
* j)
+
0 ) and
0
< 2 by
NAT_D:def 2;
reconsider j as
Element of
NAT by
ORDINAL1:def 12;
A10: j
<= i
proof
assume j
> i;
then (j
+ j)
> (i
+ 1) by
NAT_1: 14,
XREAL_1: 8;
hence thesis by
A7,
A9;
end;
j
<>
0 by
A7,
A9;
then j
>= 1 by
NAT_1: 14;
then
consider n, m such that
A11: j
= ((2
|^ n)
* ((2
* m)
+ 1)) by
A2,
A10;
k
= ((2
* (2
|^ n))
* ((2
* m)
+ 1)) by
A9,
A11;
then k
= ((2
|^ (n
+ 1))
* ((2
* m)
+ 1)) by
NEWTON: 6;
hence thesis;
end;
end;
suppose k
< (i
+ 1);
then k
<= i by
NAT_1: 13;
hence thesis by
A2,
A3;
end;
end;
hence thesis;
end;
let i;
assume i
>
0 ;
then
A12: i
>= 1 by
NAT_1: 14;
A13:
N[
0 ];
for n holds
N[n] from
NAT_1:sch 2(
A13,
A1);
hence thesis by
A12;
end;
definition
::
NAGATA_2:def1
func
PairFunc ->
Function of
[:
NAT ,
NAT :],
NAT means
:
Def1: for n, m holds (it
.
[n, m])
= (((2
|^ n)
* ((2
* m)
+ 1))
- 1);
existence
proof
deffunc
N(
Element of
NAT ,
Element of
NAT ) = (
In ((((2
|^ $1)
* ((2
* $2)
+ 1))
- 1),
NAT ));
A1: for n,m be
Element of
NAT holds (((2
|^ n)
* ((2
* m)
+ 1))
- 1)
in
NAT
proof
let n,m be
Element of
NAT ;
0
< (2
|^ n) by
NEWTON: 83;
then (((2
|^ n)
* ((2
* m)
+ 1))
- 1) is
Element of
NAT by
NAT_1: 20,
XREAL_1: 129;
hence thesis;
end;
consider NN be
Function of
[:
NAT ,
NAT :],
NAT such that
A2: for n,m be
Element of
NAT holds (NN
. (n,m))
=
N(n,m) from
BINOP_1:sch 4;
take NN;
let n, m;
A3: n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
(NN
. (n,m))
= (
In ((((2
|^ n)
* ((2
* m)
+ 1))
- 1),
NAT )) by
A2,
A3
.= (((2
|^ n)
* ((2
* m)
+ 1))
- 1) by
A1,
SUBSET_1:def 8,
A3;
hence thesis;
end;
uniqueness
proof
let N1,N2 be
Function of
[:
NAT ,
NAT :],
NAT ;
assume that
A4: for n, m holds (N1
.
[n, m])
= (((2
|^ n)
* ((2
* m)
+ 1))
- 1) and
A5: for n, m holds (N2
.
[n, m])
= (((2
|^ n)
* ((2
* m)
+ 1))
- 1);
now
let n,m be
Element of
NAT ;
(N1
.
[n, m])
= (((2
|^ n)
* ((2
* m)
+ 1))
- 1) by
A4;
hence (N1
. (n,m))
= (N2
. (n,m)) by
A5;
end;
hence thesis;
end;
end
theorem ::
NAGATA_2:2
Th2:
PairFunc is
bijective
proof
now
let nm1,nm2 be
object;
assume that
A1: nm1
in
[:
NAT ,
NAT :] and
A2: nm2
in
[:
NAT ,
NAT :] and
A3: (
PairFunc
. nm1)
= (
PairFunc
. nm2);
consider n2,m2 be
object such that
A4: n2
in
NAT & m2
in
NAT and
A5:
[n2, m2]
= nm2 by
A2,
ZFMISC_1:def 2;
consider n1,m1 be
object such that
A6: n1
in
NAT & m1
in
NAT and
A7:
[n1, m1]
= nm1 by
A1,
ZFMISC_1:def 2;
reconsider n1, n2, m1, m2 as
Element of
NAT by
A6,
A4;
A8: (((2
|^ n2)
* ((2
* m2)
+ 1))
- 1)
= (
PairFunc
. nm2) by
A5,
Def1;
A9: (((2
|^ n1)
* ((2
* m1)
+ 1))
- 1)
= (
PairFunc
. nm1) by
A7,
Def1;
then n1
= n2 by
A3,
A8,
CARD_4: 4;
hence nm1
= nm2 by
A3,
A7,
A5,
A9,
A8,
CARD_4: 4;
end;
hence
PairFunc is
one-to-one by
FUNCT_2: 19;
now
let i be
object;
assume i
in
NAT ;
then
reconsider i9 = i as
Element of
NAT ;
consider n,m be
Nat such that
A10: (i9
+ 1)
= ((2
|^ n)
* ((2
* m)
+ 1)) by
Th1;
n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
then
A11:
[n, m]
in
[:
NAT ,
NAT :] by
ZFMISC_1: 87;
(i9
-
0 )
= (((2
|^ n)
* ((2
* m)
+ 1))
- 1) by
A10;
then (
dom
PairFunc )
=
[:
NAT ,
NAT :] & i
= (
PairFunc
.
[n, m]) by
Def1,
FUNCT_2:def 1;
hence i
in (
rng
PairFunc ) by
FUNCT_1:def 3,
A11;
end;
then
NAT
c= (
rng
PairFunc );
then
NAT
= (
rng
PairFunc );
hence
PairFunc is
onto;
end;
definition
let X be
set, f be
Function of
[:X, X:],
REAL , x be
Element of X;
::
NAGATA_2:def2
func
dist (f,x) ->
Function of X,
REAL means
:
Def2: for y be
Element of X holds (it
. y)
= (f
. (x,y));
existence
proof
deffunc
D(
object) = (f
. (x,$1));
A1: for y be
object st y
in X holds
D(y)
in
REAL by
XREAL_0:def 1;
consider DIST be
Function of X,
REAL such that
A2: for y be
object st y
in X holds (DIST
. y)
=
D(y) from
FUNCT_2:sch 2(
A1);
now
per cases ;
suppose
A3: X is
empty;
let y be
Element of X;
not
[x, y]
in (
dom f) by
A3;
then
A4: (f
.
[x, y])
=
{} by
FUNCT_1:def 2;
not y
in (
dom DIST) by
A3;
hence (f
. (x,y))
= (DIST
. y) by
A4,
FUNCT_1:def 2;
end;
suppose X is non
empty;
hence for y be
Element of X holds (DIST
. y)
= (f
. (x,y)) by
A2;
end;
end;
hence thesis;
end;
uniqueness
proof
let D1,D2 be
Function of X,
REAL ;
assume that
A5: for y be
Element of X holds (D1
. y)
= (f
. (x,y)) and
A6: for y be
Element of X holds (D2
. y)
= (f
. (x,y));
now
let y be
Element of X;
(D1
. y)
= (f
. (x,y)) by
A5;
hence (D1
. y)
= (D2
. y) by
A6;
end;
hence thesis;
end;
end
theorem ::
NAGATA_2:3
Th3: for D be
Subset of
[:T1, T2:] st D is
open holds for x1 be
Point of T1, x2 be
Point of T2 holds for X1 be
Subset of T1, X2 be
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
set cT1 = the
carrier of T1;
set cT2 = the
carrier of T2;
let D be
Subset of
[:T1, T2:];
assume D is
open;
then
consider FA be
Subset-Family of
[:T1, T2:] such that
A1: D
= (
union FA) and
A2: for B be
set st B
in FA holds ex B1 be
Subset of T1, B2 be
Subset of T2 st B
=
[:B1, B2:] & B1 is
open & B2 is
open by
BORSUK_1: 5;
let x1 be
Point of T1, x2 be
Point of T2;
let X1 be
Subset of T1, X2 be
Subset of T2;
thus X1
= ((
pr1 (cT1,cT2))
.: (D
/\
[:cT1,
{x2}:])) implies X1 is
open
proof
assume
A3: X1
= ((
pr1 (cT1,cT2))
.: (D
/\
[:cT1,
{x2}:]));
for t be
set holds t
in X1 iff ex U be
Subset of T1 st U is
open & U
c= X1 & t
in U
proof
let t be
set;
t
in X1 implies ex U be
Subset of T1 st U is
open & U
c= X1 & t
in U
proof
assume t
in X1;
then
consider tx be
object such that
A4: tx
in (
dom (
pr1 (cT1,cT2))) and
A5: tx
in (D
/\
[:cT1,
{x2}:]) and
A6: t
= ((
pr1 (cT1,cT2))
. tx) by
A3,
FUNCT_1:def 6;
tx
in D by
A5,
XBOOLE_0:def 4;
then
consider tX be
set such that
A7: tx
in tX and
A8: tX
in FA by
A1,
TARSKI:def 4;
consider tX1 be
Subset of T1, tX2 be
Subset of T2 such that
A9: tX
=
[:tX1, tX2:] and
A10: tX1 is
open and tX2 is
open by
A2,
A8;
take tX1;
thus tX1 is
open by
A10;
consider tx1,tx2 be
object such that
A11: tx1
in cT1 & tx2
in cT2 and
A12: tx
=
[tx1, tx2] by
A4,
ZFMISC_1:def 2;
thus tX1
c= X1
proof
tx
in
[:cT1,
{x2}:] by
A5,
XBOOLE_0:def 4;
then
A13: tx2
= x2 by
A12,
ZFMISC_1: 106;
let a be
object such that
A14: a
in tX1;
[a, x2]
in
[:cT1, cT2:] by
A14,
ZFMISC_1: 87;
then
A15:
[a, x2]
in (
dom (
pr1 (cT1,cT2))) by
FUNCT_3:def 4;
tx2
in tX2 by
A12,
A7,
A9,
ZFMISC_1: 87;
then
[a, x2]
in
[:tX1, tX2:] by
A14,
A13,
ZFMISC_1: 87;
then
A16:
[a, x2]
in (
union FA) by
A8,
A9,
TARSKI:def 4;
[a, x2]
in
[:cT1,
{x2}:] by
A14,
ZFMISC_1: 106;
then
[a, x2]
in (D
/\
[:cT1,
{x2}:]) by
A1,
A16,
XBOOLE_0:def 4;
then ((
pr1 (cT1,cT2))
. (a,x2))
in ((
pr1 (cT1,cT2))
.: (D
/\
[:cT1,
{x2}:])) by
A15,
FUNCT_1:def 6;
hence thesis by
A3,
A14,
FUNCT_3:def 4;
end;
((
pr1 (cT1,cT2))
. (tx1,tx2))
= tx1 by
A11,
FUNCT_3:def 4;
hence thesis by
A6,
A12,
A7,
A9,
ZFMISC_1: 87;
end;
hence thesis;
end;
hence thesis by
TOPS_1: 25;
end;
thus X2
= ((
pr2 (cT1,cT2))
.: (D
/\
[:
{x1}, cT2:])) implies X2 is
open
proof
assume
A17: X2
= ((
pr2 (cT1,cT2))
.: (D
/\
[:
{x1}, cT2:]));
for t be
set holds t
in X2 iff ex U be
Subset of T2 st U is
open & U
c= X2 & t
in U
proof
let t be
set;
t
in X2 implies ex U be
Subset of T2 st U is
open & U
c= X2 & t
in U
proof
assume t
in X2;
then
consider tx be
object such that
A18: tx
in (
dom (
pr2 (cT1,cT2))) and
A19: tx
in (D
/\
[:
{x1}, cT2:]) and
A20: t
= ((
pr2 (cT1,cT2))
. tx) by
A17,
FUNCT_1:def 6;
tx
in D by
A19,
XBOOLE_0:def 4;
then
consider tX be
set such that
A21: tx
in tX and
A22: tX
in FA by
A1,
TARSKI:def 4;
consider tx1,tx2 be
object such that
A23: tx1
in cT1 & tx2
in cT2 and
A24: tx
=
[tx1, tx2] by
A18,
ZFMISC_1:def 2;
A25: ((
pr2 (cT1,cT2))
. (tx1,tx2))
= tx2 by
A23,
FUNCT_3:def 5;
consider tX1 be
Subset of T1, tX2 be
Subset of T2 such that
A26: tX
=
[:tX1, tX2:] and tX1 is
open and
A27: tX2 is
open by
A2,
A22;
A28: tX2
c= X2
proof
tx
in
[:
{x1}, cT2:] by
A19,
XBOOLE_0:def 4;
then
A29: tx1
= x1 by
A24,
ZFMISC_1: 105;
let a be
object such that
A30: a
in tX2;
[x1, a]
in
[:cT1, cT2:] by
A30,
ZFMISC_1: 87;
then
A31:
[x1, a]
in (
dom (
pr2 (cT1,cT2))) by
FUNCT_3:def 5;
tx1
in tX1 by
A24,
A21,
A26,
ZFMISC_1: 87;
then
[x1, a]
in
[:tX1, tX2:] by
A30,
A29,
ZFMISC_1: 87;
then
A32:
[x1, a]
in (
union FA) by
A22,
A26,
TARSKI:def 4;
[x1, a]
in
[:
{x1}, cT2:] by
A30,
ZFMISC_1: 105;
then
[x1, a]
in (D
/\
[:
{x1}, cT2:]) by
A1,
A32,
XBOOLE_0:def 4;
then ((
pr2 (cT1,cT2))
. (x1,a))
in ((
pr2 (cT1,cT2))
.: (D
/\
[:
{x1}, cT2:])) by
A31,
FUNCT_1:def 6;
hence thesis by
A17,
A30,
FUNCT_3:def 5;
end;
tx2
in tX2 by
A24,
A21,
A26,
ZFMISC_1: 87;
hence thesis by
A20,
A24,
A27,
A25,
A28;
end;
hence thesis;
end;
hence thesis by
TOPS_1: 25;
end;
end;
theorem ::
NAGATA_2:4
Th4: for pmet st for pmet9 st pmet
= pmet9 holds pmet9 is
continuous holds for x be
Point of T holds (
dist (pmet,x)) is
continuous
proof
set cT = the
carrier of T;
let pmet such that
A1: for pmet9 st pmet
= pmet9 holds pmet9 is
continuous;
[:cT, cT:]
= the
carrier of
[:T, T:] by
BORSUK_1:def 2;
then
reconsider pmet9 = pmet as
RealMap of
[:T, T:];
reconsider pmetR = pmet9 as
Function of
[:T, T:],
R^1 by
TOPMETR: 17;
let x be
Point of T;
reconsider distx = (
dist (pmet,x)) as
Function of T,
R^1 by
TOPMETR: 17;
pmet9 is
continuous by
A1;
then
A2: pmetR is
continuous by
JORDAN5A: 27;
now
let t be
Point of T;
for R be
Subset of
R^1 st R is
open & (distx
. t)
in R holds ex U be
Subset of T st U is
open & t
in U & (distx
.: U)
c= R
proof
reconsider xt =
[x, t] as
Point of
[:T, T:] by
BORSUK_1:def 2;
A3: (
dom (
pr2 (cT,cT)))
=
[:cT, cT:] by
FUNCT_3:def 5;
A4: pmetR
is_continuous_at xt & (distx
. t)
= (pmet
. (x,t)) by
A2,
Def2,
TMAP_1: 50;
let R be
Subset of
R^1 ;
assume R is
open & (distx
. t)
in R;
then
consider XU be
Subset of
[:T, T:] such that
A5: XU is
open and
A6: xt
in XU and
A7: (pmetR
.: XU)
c= R by
A4,
TMAP_1: 43;
set U = ((
pr2 (cT,cT))
.: (XU
/\
[:
{x}, cT:]));
[x, t]
in
[:
{x}, cT:] by
ZFMISC_1: 105;
then
[x, t]
in (XU
/\
[:
{x}, cT:]) by
A6,
XBOOLE_0:def 4;
then ((
pr2 (cT,cT))
. (x,t))
in ((
pr2 (cT,cT))
.: (XU
/\
[:
{x}, cT:])) by
A3,
FUNCT_1:def 6;
then
A8: t
in U by
FUNCT_3:def 5;
A9: (distx
.: U)
c= R
proof
let du be
object;
assume du
in (distx
.: U);
then
consider u be
object such that
A10: u
in (
dom distx) and
A11: u
in U and
A12: (distx
. u)
= du by
FUNCT_1:def 6;
reconsider u as
Point of T by
A10;
consider xu be
object such that
A13: xu
in (
dom (
pr2 (cT,cT))) and
A14: xu
in (XU
/\
[:
{x}, cT:]) and
A15: ((
pr2 (cT,cT))
. xu)
= u by
A11,
FUNCT_1:def 6;
consider x9,u9 be
object such that
A16: x9
in cT & u9
in cT and
A17: xu
=
[x9, u9] by
A13,
ZFMISC_1:def 2;
reconsider x9, u9 as
Point of T by
A16;
[x9, u9]
in
[:
{x}, cT:] by
A14,
A17,
XBOOLE_0:def 4;
then ((
pr2 (cT,cT))
. (x9,u9))
= u9 & x9
= x by
FUNCT_3:def 5,
ZFMISC_1: 105;
then
A18: (pmet
. (x9,u9))
= du by
A12,
A15,
A17,
Def2;
A19: (
dom pmetR)
= the
carrier of
[:T, T:] by
FUNCT_2:def 1;
[x9, u9]
in XU by
A14,
A17,
XBOOLE_0:def 4;
then du
in (pmetR
.: XU) by
A18,
A19,
FUNCT_1:def 6;
hence thesis by
A7;
end;
U is
open by
A5,
Th3;
hence thesis by
A8,
A9;
end;
hence distx
is_continuous_at t by
TMAP_1: 43;
end;
then distx is
continuous by
TMAP_1: 50;
hence thesis by
JORDAN5A: 27;
end;
definition
let X be non
empty
set, f be
Function of
[:X, X:],
REAL , A be
Subset of X;
::
NAGATA_2:def3
func
lower_bound (f,A) ->
Function of X,
REAL means
:
Def3: for x be
Element of X holds (it
. x)
= (
lower_bound ((
dist (f,x))
.: A));
existence
proof
deffunc
I(
Element of X) = (
In ((
lower_bound ((
dist (f,$1))
.: A)),
REAL ));
consider INF be
Function of X,
REAL such that
A1: for x be
Element of X holds (INF
. x)
=
I(x) from
FUNCT_2:sch 4;
take INF;
let x be
Element of X;
(INF
. x)
=
I(x) by
A1;
hence thesis;
end;
uniqueness
proof
let I1,I2 be
Function of X,
REAL ;
assume that
A2: for x be
Element of X holds (I1
. x)
= (
lower_bound ((
dist (f,x))
.: A)) and
A3: for x be
Element of X holds (I2
. x)
= (
lower_bound ((
dist (f,x))
.: A));
now
let x be
Element of X;
(I1
. x)
= (
lower_bound ((
dist (f,x))
.: A)) by
A2;
hence (I1
. x)
= (I2
. x) by
A3;
end;
hence thesis;
end;
end
Lm1: for X be non
empty
set, f be
Function of
[:X, X:],
REAL st f
is_a_pseudometric_of X holds f is
bounded_below & for A be non
empty
Subset of X, x be
Element of X holds ((
dist (f,x))
.: A) is non
empty
bounded_below
proof
let X be non
empty
set, f be
Function of
[:X, X:],
REAL such that
A1: f
is_a_pseudometric_of X;
A2:
now
let A be non
empty
Subset of X, x be
Element of X;
A3:
0 is
LowerBound of ((
dist (f,x))
.: A)
proof
let rn be
ExtReal;
assume rn
in ((
dist (f,x))
.: A);
then
consider y be
object such that
A4: y
in (
dom (
dist (f,x))) and y
in A and
A5: rn
= ((
dist (f,x))
. y) by
FUNCT_1:def 6;
reconsider y as
Element of X by
A4;
(f
. (x,y))
>=
0 by
A1,
NAGATA_1: 29;
hence rn
>=
0 by
A5,
Def2;
end;
(
dom (
dist (f,x)))
= X by
FUNCT_2:def 1;
hence ((
dist (f,x))
.: A) is non
empty
bounded_below by
A3;
end;
now
let xy be
object;
assume xy
in (
dom f);
then
consider x,y be
object such that
A6: x
in X & y
in X and
A7:
[x, y]
= xy by
ZFMISC_1:def 2;
reconsider x, y as
Element of X by
A6;
(f
. (x,y))
>=
0 &
0
> (
- 1) by
A1,
NAGATA_1: 29;
hence (f
. xy)
> (
- 1) by
A7;
end;
hence thesis by
A2,
SEQ_2:def 2;
end;
theorem ::
NAGATA_2:5
Th5: for X be non
empty
set, f be
Function of
[:X, X:],
REAL st f
is_a_pseudometric_of X holds for A be non
empty
Subset of X, x be
Element of X holds ((
lower_bound (f,A))
. x)
>=
0
proof
let X be non
empty
set, f be
Function of
[:X, X:],
REAL such that
A1: f
is_a_pseudometric_of X;
let A be non
empty
Subset of X, x be
Element of X;
A2:
now
let rn;
assume rn
in ((
dist (f,x))
.: A);
then
consider y be
object such that
A3: y
in (
dom (
dist (f,x))) and y
in A and
A4: rn
= ((
dist (f,x))
. y) by
FUNCT_1:def 6;
((
dist (f,x))
. y)
= (f
. (x,y)) by
A3,
Def2;
hence rn
>=
0 by
A1,
A3,
A4,
NAGATA_1: 29;
end;
X
= (
dom (
dist (f,x))) by
FUNCT_2:def 1;
then (
lower_bound ((
dist (f,x))
.: A))
>=
0 by
A2,
SEQ_4: 43;
hence thesis by
Def3;
end;
theorem ::
NAGATA_2:6
Th6: for X be non
empty
set, f be
Function of
[:X, X:],
REAL st f
is_a_pseudometric_of X holds for A be
Subset of X, x be
Element of X holds x
in A implies ((
lower_bound (f,A))
. x)
=
0
proof
let X be non
empty
set, f be
Function of
[:X, X:],
REAL such that
A1: f
is_a_pseudometric_of X;
let A be
Subset of X, x be
Element of X;
assume
A2: x
in A;
then
reconsider A as non
empty
Subset of X;
A3: ((
dist (f,x))
.: A) is non
empty
bounded_below by
A1,
Lm1;
f is
Reflexive by
A1,
NAGATA_1:def 10;
then (f
. (x,x))
=
0 by
METRIC_1:def 2;
then X
= (
dom (
dist (f,x))) & ((
dist (f,x))
. x)
=
0 by
Def2,
FUNCT_2:def 1;
then
0
in ((
dist (f,x))
.: A) by
A2,
FUNCT_1:def 6;
then (
lower_bound ((
dist (f,x))
.: A))
<=
0 by
A3,
SEQ_4:def 2;
then ((
lower_bound (f,A))
. x)
<=
0 by
Def3;
hence thesis by
A1,
Th5;
end;
theorem ::
NAGATA_2:7
Th7: for pmet st pmet
is_a_pseudometric_of the
carrier of T holds for x,y be
Point of T, A be non
empty
Subset of T holds
|.(((
lower_bound (pmet,A))
. x)
- ((
lower_bound (pmet,A))
. y)).|
<= (pmet
. (x,y))
proof
let pmet such that
A1: pmet
is_a_pseudometric_of the
carrier of T;
A2: pmet is
symmetric by
A1,
NAGATA_1:def 10;
let x,y be
Point of T, A be non
empty
Subset of T;
A3: for x1,y1 be
Point of T holds (((
lower_bound (pmet,A))
. y1)
- ((
lower_bound (pmet,A))
. x1))
>= (
- (pmet
. (x1,y1)))
proof
let x1,y1 be
Point of T;
A4: ((
dist (pmet,x1))
.: A) is non
empty
bounded_below by
A1,
Lm1;
A5: for rn st rn
in ((
dist (pmet,y1))
.: A) holds rn
>= ((
lower_bound ((
dist (pmet,x1))
.: A))
- (pmet
. (x1,y1)))
proof
let rn;
assume rn
in ((
dist (pmet,y1))
.: A);
then
consider z be
object such that
A6: z
in (
dom (
dist (pmet,y1))) and
A7: z
in A and
A8: ((
dist (pmet,y1))
. z)
= rn by
FUNCT_1:def 6;
reconsider z as
Point of T by
A6;
A9: ((
dist (pmet,x1))
. z)
= (pmet
. (x1,z)) by
Def2;
pmet is
triangle by
A1,
NAGATA_1:def 10;
then
A10: ((pmet
. (x1,y1))
+ (pmet
. (y1,z)))
>= (pmet
. (x1,z)) by
METRIC_1:def 5;
(
dom (
dist (pmet,x1)))
= the
carrier of T by
FUNCT_2:def 1;
then ((
dist (pmet,x1))
. z)
in ((
dist (pmet,x1))
.: A) by
A7,
FUNCT_1:def 6;
then (pmet
. (x1,z))
>= (
lower_bound ((
dist (pmet,x1))
.: A)) by
A4,
A9,
SEQ_4:def 2;
then ((pmet
. (x1,y1))
+ (pmet
. (y1,z)))
>= ((
lower_bound ((
dist (pmet,x1))
.: A))
+
0 ) by
A10,
XXREAL_0: 2;
then ((pmet
. (y1,z))
-
0 )
>= ((
lower_bound ((
dist (pmet,x1))
.: A))
- (pmet
. (x1,y1))) by
XREAL_1: 21;
hence thesis by
A8,
Def2;
end;
((
dist (pmet,y1))
.: A) is non
empty
bounded_below by
A1,
Lm1;
then ((
lower_bound ((
dist (pmet,y1))
.: A))
-
0 )
>= ((
lower_bound ((
dist (pmet,x1))
.: A))
- (pmet
. (x1,y1))) by
A5,
SEQ_4: 43;
then
A11: ((
lower_bound ((
dist (pmet,y1))
.: A))
- (
lower_bound ((
dist (pmet,x1))
.: A)))
>= (
0
- (pmet
. (x1,y1))) by
XREAL_1: 17;
(
lower_bound ((
dist (pmet,y1))
.: A))
= ((
lower_bound (pmet,A))
. y1) by
Def3;
hence thesis by
A11,
Def3;
end;
then (((
lower_bound (pmet,A))
. y)
- ((
lower_bound (pmet,A))
. x))
>= (
- (pmet
. (x,y)));
then (
- (((
lower_bound (pmet,A))
. x)
- ((
lower_bound (pmet,A))
. y)))
>= (
- (pmet
. (x,y)));
then
A12: (((
lower_bound (pmet,A))
. x)
- ((
lower_bound (pmet,A))
. y))
<= (pmet
. (x,y)) by
XREAL_1: 24;
(((
lower_bound (pmet,A))
. x)
- ((
lower_bound (pmet,A))
. y))
>= (
- (pmet
. (y,x))) by
A3;
then (((
lower_bound (pmet,A))
. x)
- ((
lower_bound (pmet,A))
. y))
>= (
- (pmet
. (x,y))) by
A2,
METRIC_1:def 4;
hence thesis by
A12,
ABSVALUE: 5;
end;
theorem ::
NAGATA_2:8
Th8: for pmet st pmet
is_a_pseudometric_of the
carrier of T & for p holds (
dist (pmet,p)) is
continuous holds for A be non
empty
Subset of T holds (
lower_bound (pmet,A)) is
continuous
proof
let pmet such that
A1: pmet
is_a_pseudometric_of the
carrier of T and
A2: for p holds (
dist (pmet,p)) is
continuous;
let A be non
empty
Subset of T;
reconsider infR = (
lower_bound (pmet,A)) as
Function of T,
R^1 by
TOPMETR: 17;
now
let t be
Point of T;
reconsider dR = (
dist (pmet,t)) as
Function of T,
R^1 by
TOPMETR: 17;
for R be
Subset of
R^1 st R is
open & (infR
. t)
in R holds ex U be
Subset of T st U is
open & t
in U & (infR
.: U)
c= R
proof
reconsider infRt = (infR qua
real-valued
Function
. t), dRt = (dR qua
real-valued
Function
. t) as
Point of
RealSpace by
METRIC_1:def 13,
XREAL_0:def 1;
let R be
Subset of
R^1 ;
assume R is
open & (infR
. t)
in R;
then
consider r be
Real such that
A3: r
>
0 and
A4: (
Ball (infRt,r))
c= R by
TOPMETR: 15,
TOPMETR:def 6;
reconsider dB = (
Ball (dRt,r)) as
Subset of
R^1 by
METRIC_1:def 13,
TOPMETR: 17;
|.((dR
. t)
- (dR
. t)).|
=
0 by
ABSVALUE: 2;
then (
dist (dRt,dRt))
< r by
A3,
TOPMETR: 11;
then
A5: dRt
in dB by
METRIC_1: 11;
(
dist (pmet,t)) is
continuous by
A2;
then dR is
continuous by
JORDAN5A: 27;
then dB is
open & dR
is_continuous_at t by
TMAP_1: 50,
TOPMETR: 14,
TOPMETR:def 6;
then
consider B be
Subset of T such that
A6: B is
open & t
in B and
A7: (dR
.: B)
c= dB by
A5,
TMAP_1: 43;
(infR
.: B)
c= R
proof
let Ib be
object;
assume Ib
in (infR
.: B);
then
consider b be
object such that
A8: b
in (
dom infR) and
A9: b
in B and
A10: (infR
. b)
= Ib by
FUNCT_1:def 6;
reconsider b as
Point of T by
A8;
reconsider infRb = (infR qua
real-valued
Function
. b), dRb = (dR qua
real-valued
Function
. b) as
Point of
RealSpace by
METRIC_1:def 13,
XREAL_0:def 1;
(pmet
. (t,b))
>=
0 by
A1,
NAGATA_1: 29;
then
A11: (dR
. b)
>=
0 by
Def2;
(dR
. t)
= (pmet
. (t,t)) by
Def2;
then (dR
. t)
=
0 by
A1,
NAGATA_1: 28;
then
A12: (
dist (dRt,dRb))
=
|.(
0
- (dR
. b)).| by
TOPMETR: 11;
(
dom dR)
= the
carrier of T by
FUNCT_2:def 1;
then (dR
. b)
in (dR
.: B) by
A9,
FUNCT_1:def 6;
then (
dist (dRt,dRb))
< r by
A7,
METRIC_1: 11;
then
|.(
- (
0
- (dR
. b))).|
< r by
A12,
COMPLEX1: 52;
then (dR
. b)
< r by
A11,
ABSVALUE:def 1;
then
A13: (pmet
. (t,b))
< r by
Def2;
|.(((
lower_bound (pmet,A))
. t)
- ((
lower_bound (pmet,A))
. b)).|
<= (pmet
. (t,b)) & (
dist (infRt,infRb))
=
|.(((
lower_bound (pmet,A))
. t)
- ((
lower_bound (pmet,A))
. b)).| by
A1,
Th7,
TOPMETR: 11;
then (
dist (infRt,infRb))
< r by
A13,
XXREAL_0: 2;
then infRb
in (
Ball (infRt,r)) by
METRIC_1: 11;
hence thesis by
A4,
A10;
end;
hence thesis by
A6;
end;
hence infR
is_continuous_at t by
TMAP_1: 43;
end;
then infR is
continuous by
TMAP_1: 50;
hence thesis by
JORDAN5A: 27;
end;
theorem ::
NAGATA_2:9
Th9: for f be
Function of
[:X, X:],
REAL st f
is_metric_of X holds f
is_a_pseudometric_of X
proof
let f be
Function of
[:X, X:],
REAL ;
assume f
is_metric_of X;
then for a,b,c be
Element of X holds (f
. (a,a))
=
0 & (f
. (a,b))
= (f
. (b,a)) & (f
. (a,c))
<= ((f
. (a,b))
+ (f
. (b,c))) by
PCOMPS_1:def 6;
then f is
Reflexive
symmetric
triangle by
METRIC_1:def 2,
METRIC_1:def 4,
METRIC_1:def 5;
hence thesis by
NAGATA_1:def 10;
end;
theorem ::
NAGATA_2:10
Th10: for pmet st pmet
is_metric_of the
carrier of T & (for A be non
empty
Subset of T holds (
Cl A)
= { p where p be
Point of T : ((
lower_bound (pmet,A))
. p)
=
0 }) holds T is
metrizable
proof
let pmet such that
A1: pmet
is_metric_of the
carrier of T and
A2: for A be non
empty
Subset of T holds (
Cl A)
= { p where p be
Point of T : ((
lower_bound (pmet,A))
. p)
=
0 };
set PM = (
SpaceMetr (the
carrier of T,pmet));
reconsider PM as non
empty
MetrSpace by
A1,
PCOMPS_1: 36;
A3: for x,y be
Element of PM holds (pmet
. (x,y))
= (
dist (x,y))
proof
let x,y be
Element of PM;
PM
=
MetrStruct (# the
carrier of T, pmet #) by
A1,
PCOMPS_1:def 7;
hence thesis by
METRIC_1:def 1;
end;
A4: (
Family_open_set PM)
c= the
topology of T
proof
let A be
object;
assume
A5: A
in (
Family_open_set PM);
then
reconsider AT = A as
Subset of T by
A1,
PCOMPS_2: 4;
per cases ;
suppose (AT
` ) is
empty;
then (AT
` )
= ((
[#] T)
` ) by
XBOOLE_1: 37;
then AT
= the
carrier of T by
TOPS_1: 1;
hence thesis by
PRE_TOPC:def 1;
end;
suppose
A6: (AT
` ) is non
empty;
for x holds x
in AT iff ex U be
Subset of T st U is
open & U
c= AT & x
in U
proof
let x;
x
in AT implies ex U be
Subset of T st U is
open & U
c= AT & x
in U
proof
assume
A7: x
in AT;
then
reconsider xP = x as
Element of PM by
A1,
PCOMPS_2: 4;
consider r such that
A8: r
>
0 and
A9: (
Ball (xP,r))
c= AT by
A5,
A7,
PCOMPS_1:def 4;
reconsider xT = x as
Element of T by
A7;
A10: ex y be
object st y
in (AT
` ) by
A6;
reconsider B = (
Ball (xP,r)) as
Subset of T by
A1,
PCOMPS_2: 4;
set Inf = { p where p be
Point of T : ((
lower_bound (pmet,(B
` )))
. p)
=
0 };
(AT
` )
c= (B
` ) by
A9,
SUBSET_1: 12;
then
consider b be
set such that
A11: b
in (B
` ) by
A10;
(B
` )
= Inf
proof
thus (B
` )
c= Inf
proof
let y be
object such that
A12: y
in (B
` );
((
lower_bound (pmet,(B
` )))
. y)
=
0 by
A1,
A12,
Th6,
Th9;
hence thesis by
A12;
end;
let y be
object;
assume y
in Inf;
then
consider yT be
Point of T such that
A13: y
= yT and
A14: ((
lower_bound (pmet,(B
` )))
. yT)
=
0 ;
assume not y
in (B
` );
then
A15: yT
in B by
A13,
XBOOLE_0:def 5;
reconsider yP = yT as
Point of PM by
A1,
PCOMPS_2: 4;
pmet
is_a_pseudometric_of the
carrier of T by
A1,
Th9;
then
A16: ((
dist (pmet,yT))
.: (B
` )) is non
empty
bounded_below by
A11,
Lm1;
(
Ball (xP,r))
in (
Family_open_set PM) by
PCOMPS_1: 29;
then
consider s such that
A17: s
>
0 and
A18: (
Ball (yP,s))
c= (
Ball (xP,r)) by
A15,
PCOMPS_1:def 4;
(
lower_bound ((
dist (pmet,yT))
.: (B
` )))
=
0 by
A14,
Def3;
then
consider rn such that
A19: rn
in ((
dist (pmet,yT))
.: (B
` )) and
A20: rn
< (
0
+ s) by
A17,
A16,
SEQ_4:def 2;
consider z be
object such that
A21: z
in (
dom (
dist (pmet,yT))) and
A22: z
in (B
` ) and
A23: rn
= ((
dist (pmet,yT))
. z) by
A19,
FUNCT_1:def 6;
reconsider zT = z as
Point of T by
A21;
reconsider zP = z as
Point of PM by
A1,
A21,
PCOMPS_2: 4;
(pmet
. (yT,zT))
< s by
A20,
A23,
Def2;
then (
dist (yP,zP))
< s by
A3;
then zP
in (
Ball (yP,s)) by
METRIC_1: 11;
then (B
` )
meets B by
A18,
A22,
XBOOLE_0: 3;
hence thesis by
XBOOLE_1: 79;
end;
then (B
` )
= (
Cl (B
` )) by
A2,
A11;
then
A24: B is
open by
TOPS_1: 4;
(pmet
. (xT,xT))
=
0 by
A1,
PCOMPS_1:def 6;
then (
dist (xP,xP))
< r by
A3,
A8;
then xP
in B by
METRIC_1: 11;
hence thesis by
A9,
A24;
end;
hence thesis;
end;
then AT is
open by
TOPS_1: 25;
hence thesis by
PRE_TOPC:def 2;
end;
end;
the
topology of T
c= (
Family_open_set PM)
proof
let A be
object;
assume
A25: A
in the
topology of T;
then
reconsider AT = A as
Subset of T;
reconsider AP = A as
Subset of PM by
A1,
A25,
PCOMPS_2: 4;
per cases ;
suppose (AT
` ) is
empty;
then (AT
` )
= ((
[#] T)
` ) by
XBOOLE_1: 37;
then AT
= the
carrier of T by
TOPS_1: 1;
then AT
= the
carrier of PM by
A1,
PCOMPS_2: 4;
hence thesis by
PCOMPS_1: 30;
end;
suppose
A26: (AT
` ) is non
empty;
for xP be
Element of PM st xP
in AP holds ex r st r
>
0 & (
Ball (xP,r))
c= AP
proof
let xP be
Element of PM such that
A27: xP
in AP;
reconsider xT = xP as
Element of T by
A1,
PCOMPS_2: 4;
take r = ((
lower_bound (pmet,(AT
` )))
. xT);
A28: (
Ball (xP,r))
c= AP
proof
pmet
is_a_pseudometric_of the
carrier of T by
A1,
Th9;
then
A29: ((
dist (pmet,xT))
.: (AT
` )) is non
empty
bounded_below by
A26,
Lm1;
let y be
object;
assume that
A30: y
in (
Ball (xP,r)) and
A31: not y
in AP;
reconsider yP = y as
Point of PM by
A30;
A32: (
dist (xP,yP))
< r by
A30,
METRIC_1: 11;
reconsider yT = yP as
Point of T by
A1,
PCOMPS_2: 4;
A33: (
dom (
dist (pmet,xT)))
= the
carrier of T by
FUNCT_2:def 1;
yT
in (AT
` ) by
A31,
XBOOLE_0:def 5;
then ((
dist (pmet,xT))
. yT)
in ((
dist (pmet,xT))
.: (AT
` )) by
A33,
FUNCT_1:def 6;
then
A34: (
lower_bound ((
dist (pmet,xT))
.: (AT
` )))
<= ((
dist (pmet,xT))
. yT) by
A29,
SEQ_4:def 2;
((
dist (pmet,xT))
. yT)
= (pmet
. (xT,yT)) & (
lower_bound ((
dist (pmet,xT))
.: (AT
` )))
= ((
lower_bound (pmet,(AT
` )))
. xT) by
Def2,
Def3;
hence thesis by
A3,
A32,
A34;
end;
AT is
open by
A25,
PRE_TOPC:def 2;
then (AT
` )
= (
Cl (AT
` )) by
PRE_TOPC: 22;
then
A35: (AT
` )
= { p where p be
Point of T : ((
lower_bound (pmet,(AT
` )))
. p)
=
0 } by
A2,
A26;
((
lower_bound (pmet,(AT
` )))
. xT)
>
0
proof
assume ((
lower_bound (pmet,(AT
` )))
. xT)
<=
0 ;
then ((
lower_bound (pmet,(AT
` )))
. xT)
=
0 by
A1,
A26,
Th5,
Th9;
then xT
in (AT
` ) by
A35;
then (AT
` )
meets AT by
A27,
XBOOLE_0: 3;
hence thesis by
XBOOLE_1: 79;
end;
hence thesis by
A28;
end;
hence thesis by
PCOMPS_1:def 4;
end;
end;
then the
topology of T
= (
Family_open_set PM) by
A4;
hence thesis by
A1,
PCOMPS_1:def 8;
end;
theorem ::
NAGATA_2:11
Th11: for FS2 st (for n holds ex pmet st (FS2
. n)
= pmet & pmet
is_a_pseudometric_of the
carrier of T) & for pq holds (FS2
# pq) is
summable holds for pmet st for pq holds (pmet
. pq)
= (
Sum (FS2
# pq)) holds pmet
is_a_pseudometric_of the
carrier of T
proof
set cT = the
carrier of T;
let FS2 such that
A1: for n holds ex pmet st (FS2
. n)
= pmet & pmet
is_a_pseudometric_of cT and
A2: for pq holds (FS2
# pq) is
summable;
let pmet such that
A3: for pq holds (pmet
. pq)
= (
Sum (FS2
# pq));
now
let a,b,c be
Point of T;
thus (pmet
. (a,a))
=
0
proof
set aa =
[a, a];
set F = (FS2
# aa);
now
let n;
consider pmet1 such that
A4: (FS2
. n)
= pmet1 and
A5: pmet1
is_a_pseudometric_of cT by
A1;
(pmet1
. (a,a))
=
0 by
A5,
NAGATA_1: 28;
hence (F
. n)
= (
0
* (F
. n)) by
A4,
SEQFUNC:def 10;
end;
then
A6: F
= (
0
(#) F) by
SEQ_1: 9;
F is
summable by
A2;
then (
Sum F)
= (
0
* (
Sum F)) by
A6,
SERIES_1: 10;
hence thesis by
A3;
end;
thus (pmet
. (a,c))
<= ((pmet
. (a,b))
+ (pmet
. (c,b)))
proof
set ab =
[a, b], cb =
[c, b], ac =
[a, c];
set Fac = (FS2
# ac);
set Fab = (FS2
# ab);
set Fcb = (FS2
# cb);
A7:
now
let n;
A8: ((FS2
. n)
. ac)
= (Fac
. n) & ((FS2
. n)
. ab)
= (Fab
. n) by
SEQFUNC:def 10;
consider pmet1 such that
A9: (FS2
. n)
= pmet1 and
A10: pmet1
is_a_pseudometric_of cT by
A1;
A11:
0
<= (pmet1
. (a,c)) by
A10,
NAGATA_1: 29;
(pmet1
. (a,c))
<= ((pmet1
. (a,b))
+ (pmet1
. (c,b))) by
A10,
NAGATA_1: 28;
then (Fac
. n)
<= ((Fab
. n)
+ (Fcb
. n)) by
A9,
A8,
SEQFUNC:def 10;
hence
0
<= (Fac
. n) & (Fac
. n)
<= ((Fab
+ Fcb)
. n) by
A9,
A11,
SEQFUNC:def 10,
SEQ_1: 7;
end;
A12: Fab is
summable & Fcb is
summable by
A2;
then (Fab
+ Fcb) is
summable by
SERIES_1: 7;
then
A13: (
Sum Fac)
<= (
Sum (Fab
+ Fcb)) by
A7,
SERIES_1: 20;
A14: (
Sum Fab)
= (pmet
. ab) & (
Sum Fcb)
= (pmet
. cb) by
A3;
(
Sum (Fab
+ Fcb))
= ((
Sum Fab)
+ (
Sum Fcb)) by
A12,
SERIES_1: 7;
hence thesis by
A3,
A13,
A14;
end;
end;
hence thesis by
NAGATA_1: 28;
end;
theorem ::
NAGATA_2:12
Th12: for n, seq st for m st m
<= n holds (seq
. m)
<= r holds for m st m
<= n holds ((
Partial_Sums seq)
. m)
<= (r
* (m
+ 1))
proof
let n, seq such that
A1: for m st m
<= n holds (seq
. m)
<= r;
defpred
P[
Nat] means $1
<= n implies ((
Partial_Sums seq)
. $1)
<= (r
* ($1
+ 1));
A2: for m st
P[m] holds
P[(m
+ 1)]
proof
let m such that
A3:
P[m];
A4: ((
Partial_Sums seq)
. (m
+ 1))
= (((
Partial_Sums seq)
. m)
+ (seq
. (m
+ 1))) by
SERIES_1:def 1;
assume
A5: (m
+ 1)
<= n;
then (seq
. (m
+ 1))
<= r by
A1;
then ((
Partial_Sums seq)
. (m
+ 1))
<= ((r
* (m
+ 1))
+ r) by
A3,
A5,
A4,
NAT_1: 13,
XREAL_1: 7;
hence thesis;
end;
((
Partial_Sums seq)
.
0 )
= (seq
.
0 ) by
SERIES_1:def 1;
then
A6:
P[
0 ] by
A1;
for m holds
P[m] from
NAT_1:sch 2(
A6,
A2);
hence thesis;
end;
theorem ::
NAGATA_2:13
Th13: for k holds
|.((
Partial_Sums seq)
. k).|
<= ((
Partial_Sums (
abs seq))
. k)
proof
set PS = (
Partial_Sums seq), absPS = (
Partial_Sums (
abs seq));
defpred
P[
Nat] means
|.(PS
. $1).|
<= (absPS
. $1);
A1: for k st
P[k] holds
P[(k
+ 1)]
proof
let k;
assume
P[k];
then
A2: (
|.(PS
. k).|
+
|.(seq
. (k
+ 1)).|)
<= ((absPS
. k)
+
|.(seq
. (k
+ 1)).|) by
XREAL_1: 7;
(PS
. (k
+ 1))
= ((PS
. k)
+ (seq
. (k
+ 1))) by
SERIES_1:def 1;
then
A3:
|.(PS
. (k
+ 1)).|
<= (
|.(PS
. k).|
+
|.(seq
. (k
+ 1)).|) by
COMPLEX1: 56;
((
abs seq)
. (k
+ 1))
=
|.(seq
. (k
+ 1)).| by
SEQ_1: 12;
then
|.(PS
. (k
+ 1)).|
<= ((absPS
. k)
+ ((
abs seq)
. (k
+ 1))) by
A3,
A2,
XXREAL_0: 2;
hence thesis by
SERIES_1:def 1;
end;
(absPS
.
0 )
= ((
abs seq)
.
0 ) & ((
abs seq)
.
0 )
=
|.(seq
.
0 ).| by
SEQ_1: 12,
SERIES_1:def 1;
then
A4:
P[
0 ] by
SERIES_1:def 1;
for k holds
P[k] from
NAT_1:sch 2(
A4,
A1);
hence thesis;
end;
theorem ::
NAGATA_2:14
Th14: for FS1 be
Functional_Sequence of the
carrier of T,
REAL st (for n holds ex f st (FS1
. n)
= f & f is
continuous & for p holds (f
. p)
>=
0 ) & (ex seq st seq is
summable & for n, p holds ((FS1
# p)
. n)
<= (seq
. n)) holds for f st for p holds (f
. p)
= (
Sum (FS1
# p)) holds f is
continuous
proof
let FS1 be
Functional_Sequence of the
carrier of T,
REAL such that
A1: for n holds ex f st (FS1
. n)
= f & f is
continuous & for p holds (f
. p)
>=
0 and
A2: ex seq st seq is
summable & for n, p holds ((FS1
# p)
. n)
<= (seq
. n);
let f such that
A3: for p holds (f
. p)
= (
Sum (FS1
# p));
reconsider fR = f as
Function of T,
R^1 by
TOPMETR: 17;
now
let p;
for R be
Subset of
R^1 st R is
open & (fR
. p)
in R holds ex U be
Subset of T st U is
open & p
in U & (fR
.: U)
c= R
proof
reconsider fRp = (fR qua
real-valued
Function
. p) as
Point of
RealSpace by
METRIC_1:def 13,
XREAL_0:def 1;
let R be
Subset of
R^1 ;
assume R is
open & (fR
. p)
in R;
then
consider rn such that
A4: rn
>
0 and
A5: (
Ball (fRp,rn))
c= R by
TOPMETR: 15,
TOPMETR:def 6;
set r2 = (rn
/ 2), r4 = (rn
/ 4);
reconsider r2, r4 as
Real;
A6: r4
>
0 by
A4,
XREAL_1: 224;
consider seq such that
A7: seq is
summable and
A8: for n, q holds ((FS1
# q)
. n)
<= (seq
. n) by
A2;
(
Partial_Sums seq) is
convergent by
A7,
SERIES_1:def 2;
then
consider n such that
A9: for m st n
<= m holds
|.(((
Partial_Sums seq)
. m)
- (
lim (
Partial_Sums seq))).|
< r4 by
A6,
SEQ_2:def 7;
defpred
Sn[
object,
object] means ex SS be
Subset of T st SS
= $2 & SS is
open & p
in SS & for f1 st (FS1
. $1)
= f1 holds for f1p be
Point of
RealSpace st f1p
= (f1
. p) holds (f1
.: SS)
c= (
Ball (f1p,(r2
/ (n
+ 1))));
A10: for k be
object st k
in (
{
0 }
\/ (
Seg n)) holds ex U be
object st U
in (
bool the
carrier of T) &
Sn[k, U]
proof
let k be
object;
assume k
in (
{
0 }
\/ (
Seg n));
then k
in (
Seg n) or k
in
{
0 } by
XBOOLE_0:def 3;
then
reconsider k as
Element of
NAT by
TARSKI:def 1;
consider f1 such that
A11: (FS1
. k)
= f1 and
A12: f1 is
continuous and for p holds (f1
. p)
>=
0 by
A1;
reconsider f19 = f1 as
Function of T,
R^1 by
TOPMETR: 17;
reconsider f1p = (f19 qua
real-valued
Function
. p) as
Point of
RealSpace by
METRIC_1:def 13,
XREAL_0:def 1;
set B = (
Ball (f1p,(r2
/ (n
+ 1))));
reconsider B as
Subset of
R^1 by
METRIC_1:def 13,
TOPMETR: 17;
(
dist (f1p,f1p))
=
0 & r2
>
0 by
A4,
METRIC_1: 1,
XREAL_1: 215;
then (
dist (f1p,f1p))
< (r2
/ (n
+ 1)) by
XREAL_1: 139;
then
A13: f1p
in B by
METRIC_1: 11;
f19 is
continuous by
A12,
JORDAN5A: 27;
then B is
open & f19
is_continuous_at p by
TMAP_1: 50,
TOPMETR: 14,
TOPMETR:def 6;
then
consider U be
Subset of T such that
A14: U is
open & p
in U and
A15: (f19
.: U)
c= B by
A13,
TMAP_1: 43;
for f1 st (FS1
. k)
= f1 holds for f1p be
Point of
RealSpace st f1p
= (f1
. p) holds (f1
.: U)
c= (
Ball (f1p,(r2
/ (n
+ 1)))) by
A11,
A15;
hence thesis by
A14;
end;
consider FSn be
Function of (
{
0 }
\/ (
Seg n)), (
bool the
carrier of T) such that
A16: for k be
object st k
in (
{
0 }
\/ (
Seg n)) holds
Sn[k, (FSn
. k)] from
FUNCT_2:sch 1(
A10);
A17: for k, q holds ((FS1
# q)
. k)
>=
0
proof
let k, q;
(ex f1 st (FS1
. k)
= f1 & f1 is
continuous & for q holds (f1
. q)
>=
0 ) & ((FS1
. k)
. q)
= ((FS1
# q)
. k) by
A1,
SEQFUNC:def 10;
hence thesis;
end;
A18: for k holds ((seq
^\ (n
+ 1))
. k)
>=
0
proof
let k;
0
<= ((FS1
# p)
. ((n
+ 1)
+ k)) & (seq
. ((n
+ 1)
+ k))
= ((seq
^\ (n
+ 1))
. k) by
A17,
NAT_1:def 3;
hence thesis by
A8;
end;
reconsider RNG = (
rng FSn) as
Subset-Family of T;
A19: RNG is
open
proof
let Q be
Subset of T;
assume Q
in RNG;
then
consider x be
object such that
A20: x
in (
dom FSn) and
A21: (FSn
. x)
= Q by
FUNCT_1:def 3;
ex SS be
Subset of T st SS
= (FSn
. x) & SS is
open & p
in SS & for f1 st (FS1
. x)
= f1 holds for f1p be
Point of
RealSpace st f1p
= (f1
. p) holds (f1
.: SS)
c= (
Ball (f1p,(r2
/ (n
+ 1)))) by
A16,
A20;
hence thesis by
A21;
end;
0
in
{
0 } by
TARSKI:def 1;
then
0
in (
{
0 }
\/ (
Seg n)) by
XBOOLE_0:def 3;
then
reconsider RNG as non
empty
Subset-Family of T by
FUNCT_2: 4;
A22: (
lim (
Partial_Sums seq))
= (
Sum seq) & (
Sum seq)
= (((
Partial_Sums seq)
. n)
+ (
Sum (seq
^\ (n
+ 1)))) by
A7,
SERIES_1: 15,
SERIES_1:def 3;
|.(((
Partial_Sums seq)
. n)
- (
lim (
Partial_Sums seq))).|
< r4 by
A9;
then
|.(
- (
Sum (seq
^\ (n
+ 1)))).|
< r4 by
A22;
then
A23:
|.(
Sum (seq
^\ (n
+ 1))).|
< r4 by
COMPLEX1: 52;
(seq
^\ (n
+ 1)) is
summable by
A7,
SERIES_1: 12;
then (
Sum (seq
^\ (n
+ 1)))
>=
0 by
A18,
SERIES_1: 18;
then
A24: (
Sum (seq
^\ (n
+ 1)))
< r4 by
A23,
ABSVALUE:def 1;
A25: for q holds (FS1
# q) is
summable &
0
<= (
Sum ((FS1
# q)
^\ (n
+ 1))) & (
Sum ((FS1
# q)
^\ (n
+ 1)))
< r4
proof
let q;
set F = (FS1
# q);
A26:
now
let k;
A27: (seq
. ((n
+ 1)
+ k))
= ((seq
^\ (n
+ 1))
. k) by
NAT_1:def 3;
0
<= (F
. ((n
+ 1)
+ k)) & (F
. ((n
+ 1)
+ k))
<= (seq
. ((n
+ 1)
+ k)) by
A8,
A17;
hence
0
<= ((F
^\ (n
+ 1))
. k) & ((F
^\ (n
+ 1))
. k)
<= ((seq
^\ (n
+ 1))
. k) by
A27,
NAT_1:def 3;
end;
A28: for k holds
0
<= (F
. k) & (F
. k)
<= (seq
. k) by
A8,
A17;
then F is
summable by
A7,
SERIES_1: 20;
then
A29: (F
^\ (n
+ 1)) is
summable by
SERIES_1: 12;
(seq
^\ (n
+ 1)) is
summable by
A7,
SERIES_1: 12;
then (
Sum (F
^\ (n
+ 1)))
<= (
Sum (seq
^\ (n
+ 1))) by
A26,
SERIES_1: 20;
hence thesis by
A7,
A24,
A28,
A26,
A29,
SERIES_1: 18,
SERIES_1: 20,
XXREAL_0: 2;
end;
A30: (fR
.: (
meet RNG))
c= R
proof
let fRq be
object;
assume fRq
in (fR
.: (
meet RNG));
then
consider q be
object such that
A31: q
in (
dom fR) and
A32: q
in (
meet RNG) and
A33: fRq
= (fR
. q) by
FUNCT_1:def 6;
reconsider q as
Point of T by
A31;
set sp = (FS1
# p), sq = (FS1
# q), spn = (sp
^\ (n
+ 1)), sqn = (sq
^\ (n
+ 1));
set absPSpq = (
Partial_Sums
|.(sp
- sq).|);
for k st k
<= n holds (
|.(sp
- sq).|
. k)
<= (r2
/ (n
+ 1))
proof
let k such that
A34: k
<= n;
k
=
0 or k
>= 1 by
NAT_1: 14;
then k
in
{
0 } or k
in (
Seg n) by
A34,
FINSEQ_1: 1,
TARSKI:def 1;
then
A35: k
in (
{
0 }
\/ (
Seg n)) by
XBOOLE_0:def 3;
then (FSn
. k)
in RNG by
FUNCT_2: 4;
then
A36: q
in (FSn
. k) by
A32,
SETFAM_1:def 1;
A37: k
in
NAT by
ORDINAL1:def 12;
(
dom (sp
- sq))
=
NAT by
FUNCT_2:def 1;
then
A38: ((sp
- sq)
. k)
= ((sp
. k)
- (sq
. k)) by
VALUED_1: 13,
A37;
consider f1 such that
A39: (FS1
. k)
= f1 and f1 is
continuous and for p holds (f1
. p)
>=
0 by
A1;
reconsider f1p = (f1
. p), f1q = (f1
. q) as
Point of
RealSpace by
METRIC_1:def 13;
ex SS be
Subset of T st SS
= (FSn
. k) & SS is
open & p
in SS & for f1 st (FS1
. k)
= f1 holds for f1p be
Point of
RealSpace st f1p
= (f1
. p) holds (f1
.: SS)
c= (
Ball (f1p,(r2
/ (n
+ 1)))) by
A16,
A35;
then
A40: (f1
.: (FSn
. k))
c= (
Ball (f1p,(r2
/ (n
+ 1)))) by
A39;
(
dom f1)
= the
carrier of T by
FUNCT_2:def 1;
then f1q
in (f1
.: (FSn
. k)) by
A36,
FUNCT_1:def 6;
then (
dist (f1p,f1q))
< (r2
/ (n
+ 1)) by
A40,
METRIC_1: 11;
then
A41:
|.((f1
. p)
- (f1
. q)).|
< (r2
/ (n
+ 1)) by
TOPMETR: 11;
(f1
. p)
= (sp
. k) by
A39,
SEQFUNC:def 10;
then
|.((sp
. k)
- (sq
. k)).|
< (r2
/ (n
+ 1)) by
A39,
A41,
SEQFUNC:def 10;
hence thesis by
A38,
SEQ_1: 12;
end;
then
A42: (absPSpq
. n)
<= ((r2
/ (n
+ 1))
* (n
+ 1)) by
Th12;
A43: n
in
NAT by
ORDINAL1:def 12;
set PSp = (
Partial_Sums sp), PSq = (
Partial_Sums sq), PSpq = (
Partial_Sums (sp
- sq));
(PSp
- PSq)
= PSpq & (
dom (PSp
- PSq))
=
NAT by
SEQ_1: 1,
SERIES_1: 6;
then
A44:
|.((PSp
. n)
- (PSq
. n)).|
=
|.(PSpq
. n).| by
VALUED_1: 13,
A43;
|.(PSpq
. n).|
<= (absPSpq
. n) by
Th13;
then
|.((PSp
. n)
- (PSq
. n)).|
<= ((r2
/ (n
+ 1))
* (n
+ 1)) by
A44,
A42,
XXREAL_0: 2;
then
A45:
|.((PSp
. n)
- (PSq
. n)).|
<= r2 by
XCMPLX_1: 87;
0
<= (
Sum spn) by
A25;
then
A46:
|.(
Sum spn).|
= (
Sum spn) by
ABSVALUE:def 1;
0
<= (
Sum sqn) by
A25;
then
A47:
|.(
Sum sqn).|
= (
Sum sqn) by
ABSVALUE:def 1;
reconsider fRq = (fR qua
real-valued
Function
. q) as
Point of
RealSpace by
METRIC_1:def 13,
XREAL_0:def 1;
A48:
|.((
Sum spn)
- (
Sum sqn)).|
<= (
|.(
Sum spn).|
+
|.(
Sum sqn).|) by
COMPLEX1: 57;
A49: fRp
= (
Sum sp) & fRq
= (
Sum sq) by
A3;
(
Sum sp)
= ((PSp
. n)
+ (
Sum spn)) & (
Sum sq)
= ((PSq
. n)
+ (
Sum sqn)) by
A25,
SERIES_1: 15;
then
|.((fR
. p)
- (fR
. q)).|
=
|.(((PSp
. n)
- (PSq
. n))
+ ((
Sum spn)
- (
Sum sqn))).| by
A49;
then
A50:
|.((fR
. p)
- (fR
. q)).|
<= (
|.((PSp
. n)
- (PSq
. n)).|
+
|.((
Sum spn)
- (
Sum sqn)).|) by
COMPLEX1: 56;
(
Sum spn)
< r4 & (
Sum sqn)
< r4 by
A25;
then (
|.(
Sum spn).|
+
|.(
Sum sqn).|)
< (r4
+ r4) by
A46,
A47,
XREAL_1: 8;
then
|.((
Sum spn)
- (
Sum sqn)).|
< r2 by
A48,
XXREAL_0: 2;
then (
|.((PSp
. n)
- (PSq
. n)).|
+
|.((
Sum spn)
- (
Sum sqn)).|)
< (r2
+ r2) by
A45,
XREAL_1: 8;
then
|.((fR
. p)
- (fR
. q)).|
< rn by
A50,
XXREAL_0: 2;
then (
dist (fRp,fRq))
< rn by
TOPMETR: 11;
then fRq
in (
Ball (fRp,rn)) by
METRIC_1: 11;
hence thesis by
A5,
A33;
end;
now
let Fx be
set;
assume Fx
in RNG;
then
consider x be
object such that
A51: x
in (
dom FSn) and
A52: (FSn
. x)
= Fx by
FUNCT_1:def 3;
ex SS be
Subset of T st SS
= (FSn
. x) & SS is
open & p
in SS & for f1 st (FS1
. x)
= f1 holds for f1p be
Point of
RealSpace st f1p
= (f1
. p) holds (f1
.: SS)
c= (
Ball (f1p,(r2
/ (n
+ 1)))) by
A16,
A51;
hence p
in Fx by
A52;
end;
then p
in (
meet RNG) by
SETFAM_1:def 1;
hence thesis by
A19,
A30,
TOPS_2: 20;
end;
hence fR
is_continuous_at p by
TMAP_1: 43;
end;
then fR is
continuous by
TMAP_1: 50;
hence thesis by
JORDAN5A: 27;
end;
theorem ::
NAGATA_2:15
Th15: for s, FS2 st for n holds ex pmet st (FS2
. n)
= pmet & pmet
is_a_pseudometric_of the
carrier of T & (for pq holds (pmet
. pq)
<= s) & for pmet9 st pmet
= pmet9 holds pmet9 is
continuous holds for pmet st for pq holds (pmet
. pq)
= (
Sum (((1
/ 2)
GeoSeq )
(#) (FS2
# pq))) holds pmet
is_a_pseudometric_of the
carrier of T & for pmet9 st pmet
= pmet9 holds pmet9 is
continuous
proof
set Geo = ((1
/ 2)
GeoSeq );
set cT = the
carrier of T, cTT = the
carrier of
[:T, T:];
let s, FS2 such that
A1: for n holds ex pmet st (FS2
. n)
= pmet & pmet
is_a_pseudometric_of cT & (for pq holds (pmet
. pq)
<= s) & for pmet9 st pmet
= pmet9 holds pmet9 is
continuous;
set SGeo = (s
(#) Geo);
deffunc
GF(
Nat) = ((Geo
. $1)
(#) (FS2
. $1));
consider GeoF be
Functional_Sequence of
[:cT, cT:],
REAL such that
A2: for n be
Nat holds (GeoF
. n)
=
GF(n) from
SEQFUNC:sch 1;
cTT
=
[:cT, cT:] by
BORSUK_1:def 2;
then
reconsider GeoF9 = GeoF as
Functional_Sequence of cTT,
REAL ;
A3: for pq, k holds
0
<= ((GeoF
# pq)
. k) & ((GeoF
# pq)
. k)
<= (SGeo
. k)
proof
let pq, k;
consider x,y be
object such that
A4: x
in cT & y
in cT and
A5:
[x, y]
= pq by
ZFMISC_1:def 2;
reconsider x, y as
Point of T by
A4;
consider pmet1 such that
A6: (FS2
. k)
= pmet1 and
A7: pmet1
is_a_pseudometric_of cT and
A8: for pq holds (pmet1
. pq)
<= s and for pmet19 st pmet1
= pmet19 holds pmet19 is
continuous by
A1;
A9:
0
<= (pmet1
. (x,y)) by
A7,
NAGATA_1: 29;
(
dom ((Geo
. k)
(#) (FS2
. k)))
=
[:cT, cT:] by
A6,
FUNCT_2:def 1;
then
A10: ((Geo
. k)
* ((FS2
. k)
. pq))
= (((Geo
. k)
(#) (FS2
. k))
. pq) by
VALUED_1:def 5
.= ((GeoF
. k)
. pq) by
A2
.= ((GeoF
# pq)
. k) by
SEQFUNC:def 10;
((1
/ 2)
|^ k)
>
0 by
NEWTON: 83;
then
A11: (Geo
. k)
>
0 by
PREPOWER:def 1;
then ((Geo
. k)
* (pmet1
. pq))
<= ((Geo
. k)
* s) by
A8,
XREAL_1: 64;
hence thesis by
A6,
A5,
A10,
A9,
A11,
SEQ_1: 9;
end;
A12: for n holds ex f be
RealMap of
[:T, T:] st ((GeoF9
. n)
= f & f is
continuous & for pq9 holds (f
. pq9)
>=
0 )
proof
let n;
consider pmet1 such that
A13: (FS2
. n)
= pmet1 and pmet1
is_a_pseudometric_of cT and for pq holds (pmet1
. pq)
<= s and
A14: for pmet19 st pmet1
= pmet19 holds pmet19 is
continuous by
A1;
cTT
=
[:cT, cT:] by
BORSUK_1:def 2;
then
reconsider pmet19 = pmet1 as
RealMap of
[:T, T:];
reconsider pR = pmet19 as
Function of
[:T, T:],
R^1 by
TOPMETR: 17;
pmet19 is
continuous by
A14;
then pR is
continuous by
JORDAN5A: 27;
then
consider fR be
Function of
[:T, T:],
R^1 such that
A15: for pq9 be
Point of
[:T, T:], rn st (pR
. pq9)
= rn holds (fR
. pq9)
= ((Geo
. n)
* rn) and
A16: fR is
continuous by
JGRAPH_2: 23;
reconsider f = fR as
RealMap of
[:T, T:] by
TOPMETR: 17;
A17: (
dom f)
= cTT by
FUNCT_2:def 1;
take f;
A18: (
dom pmet1)
=
[:cT, cT:] by
FUNCT_2:def 1;
A19: (GeoF9
. n)
= ((Geo
. n)
(#) (FS2
. n)) by
A2;
then
A20: (
dom (FS2
. n))
= (
dom (GeoF9
. n)) by
VALUED_1:def 5;
A21:
[:cT, cT:]
= cTT by
BORSUK_1:def 2;
A22:
now
let pq9 such that pq9
in (
dom (GeoF9
. n));
((GeoF9
. n)
. pq9)
= ((Geo
. n)
* (pmet1
. pq9)) by
A13,
A19,
A20,
A18,
A21,
VALUED_1:def 5;
hence ((GeoF9
. n)
. pq9)
= (f
. pq9) by
A15;
end;
now
let pq9;
reconsider pq = pq9 as
Element of
[:cT, cT:] by
BORSUK_1:def 2;
((GeoF9
. n)
. pq9)
= ((GeoF
# pq)
. n) & ((GeoF
# pq)
. n)
>=
0 by
A3,
SEQFUNC:def 10;
hence (f
. pq9)
>=
0 by
A13,
A20,
A18,
A22;
end;
hence thesis by
A13,
A16,
A20,
A18,
A17,
A21,
A22,
JORDAN5A: 27,
PARTFUN1: 5;
end;
let pmet such that
A23: for pq holds (pmet
. pq)
= (
Sum (Geo
(#) (FS2
# pq)));
A24: for pq holds (pmet
. pq)
= (
Sum (GeoF
# pq))
proof
let pq;
now
let z be
object;
assume z
in
NAT ;
then
reconsider k = z as
Element of
NAT ;
ex pmet1 st (FS2
. k)
= pmet1 & pmet1
is_a_pseudometric_of cT & (for pq holds (pmet1
. pq)
<= s) & for pmet19 st pmet1
= pmet19 holds pmet19 is
continuous by
A1;
then (
dom ((Geo
. k)
(#) (FS2
. k)))
=
[:cT, cT:] by
FUNCT_2:def 1;
then ((Geo
. k)
* ((FS2
. k)
. pq))
= (((Geo
. k)
(#) (FS2
. k))
. pq) by
VALUED_1:def 5
.= ((GeoF
. k)
. pq) by
A2
.= ((GeoF
# pq)
. k) by
SEQFUNC:def 10;
then ((GeoF
# pq)
. k)
= ((Geo
. k)
* ((FS2
# pq)
. k)) by
SEQFUNC:def 10
.= ((Geo
(#) (FS2
# pq))
. k) by
SEQ_1: 8;
hence ((Geo
(#) (FS2
# pq))
. z)
= ((GeoF
# pq)
. z);
end;
then (Geo
(#) (FS2
# pq))
= (GeoF
# pq);
hence thesis by
A23;
end;
A25: for n holds ex pmet1 st (GeoF
. n)
= pmet1 & pmet1
is_a_pseudometric_of cT
proof
let n;
consider pmet1 such that
A26: (FS2
. n)
= pmet1 and
A27: pmet1
is_a_pseudometric_of cT and for pq holds (pmet1
. pq)
<= s and for pmet19 st pmet1
= pmet19 holds pmet19 is
continuous by
A1;
deffunc
F(
Element of cT,
Element of cT) = ((Geo
. n)
* (pmet1
. ($1,$2)));
consider GF be
Function of
[:cT, cT:],
REAL such that
A28: for p holds for q holds (GF
. (p,q))
=
F(p,q) from
BINOP_1:sch 4;
now
let a,b,c be
Point of T;
((1
/ 2)
|^ n)
>
0 by
NEWTON: 83;
then
A29: (((1
/ 2)
GeoSeq )
. n)
>
0 by
PREPOWER:def 1;
(pmet1
. (a,c))
<= ((pmet1
. (a,b))
+ (pmet1
. (c,b))) by
A27,
NAGATA_1: 28;
then ((pmet1
. (a,c))
* (((1
/ 2)
GeoSeq )
. n))
<= (((pmet1
. (a,b))
+ (pmet1
. (c,b)))
* (Geo
. n)) by
A29,
XREAL_1: 64;
then
A30: (GF
. (a,c))
<= (((Geo
. n)
* (pmet1
. (a,b)))
+ ((Geo
. n)
* (pmet1
. (c,b)))) by
A28;
(GF
. (a,a))
= ((Geo
. n)
* (pmet1
. (a,a))) & (pmet1
. (a,a))
=
0 by
A27,
A28,
NAGATA_1: 28;
hence (GF
. (a,a))
=
0 ;
((Geo
. n)
* (pmet1
. (a,b)))
= (GF
. (a,b)) by
A28;
hence (GF
. (a,c))
<= ((GF
. (a,b))
+ (GF
. (c,b))) by
A28,
A30;
end;
then
A31: GF
is_a_pseudometric_of cT by
NAGATA_1: 28;
A32: (GeoF
. n)
= ((Geo
. n)
(#) (FS2
. n)) by
A2;
then
A33: (
dom (FS2
. n))
= (
dom (GeoF
. n)) by
VALUED_1:def 5;
A34:
now
let x,y be
object;
assume
A35:
[x, y]
in (
dom (GeoF
. n));
then
reconsider x9 = x, y9 = y as
Point of T by
ZFMISC_1: 87;
(GF
. (x9,y9))
= ((Geo
. n)
* (pmet1
. (x9,y9))) by
A28;
hence ((GeoF
. n)
. (x,y))
= (GF
. (x,y)) by
A26,
A32,
A35,
VALUED_1:def 5;
end;
(
dom pmet1)
=
[:cT, cT:] & (
dom GF)
=
[:cT, cT:] by
FUNCT_2:def 1;
hence thesis by
A26,
A33,
A34,
A31,
BINOP_1: 20;
end;
(1
/ 2)
< 1;
then
|.(1
/ 2).|
< 1 by
ABSVALUE:def 1;
then
A36: Geo is
summable by
SERIES_1: 24;
A37: for pq, pq9 st pq
= pq9 holds (GeoF
# pq)
= (GeoF9
# pq9)
proof
let pq, pq9 such that
A38: pq
= pq9;
now
let x be
Element of
NAT ;
((GeoF
# pq)
. x)
= ((GeoF
. x)
. pq) by
SEQFUNC:def 10;
hence ((GeoF
# pq)
. x)
= ((GeoF9
# pq9)
. x) by
A38,
SEQFUNC:def 10;
end;
hence thesis;
end;
A39: ex seq st seq is
summable & for n, pq9 holds ((GeoF9
# pq9)
. n)
<= (seq
. n)
proof
take SGeo;
thus SGeo is
summable by
A36,
SERIES_1: 10;
now
let n, pq9;
reconsider pq = pq9 as
Element of
[:cT, cT:] by
BORSUK_1:def 2;
((GeoF9
# pq9)
. n)
= ((GeoF
# pq)
. n) by
A37;
hence ((GeoF9
# pq9)
. n)
<= (SGeo
. n) by
A3;
end;
hence thesis;
end;
A40: for pmet19 st pmet
= pmet19 holds pmet19 is
continuous by
A12,
A24,
A39,
Th14;
for pq holds (GeoF
# pq) is
summable
proof
let pq;
for k holds
0
<= ((GeoF
# pq)
. k) & ((GeoF
# pq)
. k)
<= (SGeo
. k) & SGeo is
summable by
A3,
A36,
SERIES_1: 10;
hence thesis by
SERIES_1: 20;
end;
hence thesis by
A25,
A24,
A40,
Th11;
end;
theorem ::
NAGATA_2:16
Th16: for pmet st pmet
is_a_pseudometric_of the
carrier of T & for pmet9 st pmet
= pmet9 holds pmet9 is
continuous holds for A be non
empty
Subset of T, p holds p
in (
Cl A) implies ((
lower_bound (pmet,A))
. p)
=
0
proof
set rn = (
In (
0 ,
REAL ));
let pmet such that
A1: pmet
is_a_pseudometric_of the
carrier of T and
A2: for pmet9 st pmet
= pmet9 holds pmet9 is
continuous;
let A be non
empty
Subset of T, p;
A3: (
dom (
lower_bound (pmet,A)))
= the
carrier of T by
FUNCT_2:def 1;
reconsider Z =
{rn}, infA = ((
lower_bound (pmet,A))
.: A) as
Subset of
R^1 by
TOPMETR: 17;
infA
c= Z
proof
let infa be
object;
assume infa
in infA;
then ex a be
object st a
in (
dom (
lower_bound (pmet,A))) & a
in A & infa
= ((
lower_bound (pmet,A))
. a) by
FUNCT_1:def 6;
then infa
=
0 by
A1,
Th6;
hence thesis by
TARSKI:def 1;
end;
then
A4: (
Cl infA)
c= (
Cl Z) by
PRE_TOPC: 19;
reconsider InfA = (
lower_bound (pmet,A)) as
Function of T,
R^1 by
TOPMETR: 17;
for p holds (
dist (pmet,p)) is
continuous by
A2,
Th4;
then (
lower_bound (pmet,A)) is
continuous by
A1,
Th8;
then InfA is
continuous by
JORDAN5A: 27;
then
A5: (InfA
.: (
Cl A))
c= (
Cl (InfA
.: A)) by
TOPS_2: 45;
assume p
in (
Cl A);
then
A6: ((
lower_bound (pmet,A))
. p)
in ((
lower_bound (pmet,A))
.: (
Cl A)) by
A3,
FUNCT_1:def 6;
Z is
closed by
PCOMPS_1: 7,
TOPMETR: 17;
then Z
= (
Cl Z) by
PRE_TOPC: 22;
then (InfA
.: (
Cl A))
c= Z by
A4,
A5;
hence thesis by
A6,
TARSKI:def 1;
end;
theorem ::
NAGATA_2:17
Th17: for T st T is
T_1 holds for s, FS2 st (for n holds ex pmet st (FS2
. n)
= pmet & pmet
is_a_pseudometric_of the
carrier of T & (for pq holds (pmet
. pq)
<= s) & for pmet9 st pmet
= pmet9 holds pmet9 is
continuous) & for p, A9 st not p
in A9 & A9 is
closed holds ex n st for pmet st (FS2
. n)
= pmet holds ((
lower_bound (pmet,A9))
. p)
>
0 holds (ex pmet st pmet
is_metric_of the
carrier of T & for pq holds (pmet
. pq)
= (
Sum (((1
/ 2)
GeoSeq )
(#) (FS2
# pq)))) & T is
metrizable
proof
let T such that
A1: T is
T_1;
set cT = the
carrier of T, Geo = ((1
/ 2)
GeoSeq );
let s, FS2 such that
A2: for n holds ex pmet st (FS2
. n)
= pmet & pmet
is_a_pseudometric_of the
carrier of T & (for pq holds (pmet
. pq)
<= s) & for pmet9 st pmet
= pmet9 holds pmet9 is
continuous and
A3: for p, A9 st not p
in A9 & A9 is
closed holds ex n st for pmet st (FS2
. n)
= pmet holds ((
lower_bound (pmet,A9))
. p)
>
0 ;
deffunc
pm(
Element of cT,
Element of cT) = (
In ((
Sum (Geo
(#) (FS2
#
[$1, $2]))),
REAL ));
consider pmet such that
A4: for p, q holds (pmet
. (p,q))
=
pm(p,q) from
BINOP_1:sch 4;
A5: for pq holds (pmet
. pq)
= (
Sum (Geo
(#) (FS2
# pq)))
proof
let pq;
consider p,q be
object such that
A6: p
in cT & q
in cT and
A7: pq
=
[p, q] by
ZFMISC_1:def 2;
reconsider p, q as
Element of cT by
A6;
(pmet
. pq)
= (pmet
. (p,q)) by
A7
.=
pm(p,q) by
A4;
hence thesis by
A7;
end;
A8: for pq, n holds
0
<= ((Geo
(#) (FS2
# pq))
. n) & ((Geo
(#) (FS2
# pq))
. n)
<= ((s
(#) Geo)
. n)
proof
let pq, n;
consider x,y be
object such that
A9: x
in cT & y
in cT and
A10:
[x, y]
= pq by
ZFMISC_1:def 2;
reconsider x, y as
Point of T by
A9;
A11: ((Geo
. n)
* s)
= ((s
(#) Geo)
. n) by
SEQ_1: 9;
((1
/ 2)
|^ n)
>
0 by
NEWTON: 83;
then
A12: (Geo
. n)
>
0 by
PREPOWER:def 1;
consider pmet1 such that
A13: (FS2
. n)
= pmet1 and
A14: pmet1
is_a_pseudometric_of cT and
A15: for pq holds (pmet1
. pq)
<= s and for pmet19 st pmet1
= pmet19 holds pmet19 is
continuous by
A2;
A16:
0
<= (pmet1
. (x,y)) by
A14,
NAGATA_1: 29;
A17: (pmet1
. pq)
= ((FS2
# pq)
. n) by
A13,
SEQFUNC:def 10;
then ((Geo
. n)
* ((FS2
# pq)
. n))
<= ((Geo
. n)
* s) by
A15,
A12,
XREAL_1: 64;
hence thesis by
A10,
A16,
A12,
A17,
A11,
SEQ_1: 8;
end;
A18: for p, q holds (pmet
. (p,q))
=
0 implies p
= q
proof
let p, q;
assume that
A19: (pmet
. (p,q))
=
0 and
A20: p
<> q;
set Q =
{q};
A21: not p
in Q by
A20,
TARSKI:def 1;
set pq =
[p, q];
A22: (
Sum (Geo
(#) (FS2
# pq)))
=
0 by
A5,
A19;
A23: for n holds
0
<= ((Geo
(#) (FS2
# pq))
. n) & ((Geo
(#) (FS2
# pq))
. n)
<= ((s
(#) Geo)
. n) by
A8;
Q is
closed by
A1,
URYSOHN1: 19;
then
consider n such that
A24: for pmet1 st (FS2
. n)
= pmet1 holds ((
lower_bound (pmet1,Q))
. p)
>
0 by
A3,
A21;
consider pmet1 such that
A25: (FS2
. n)
= pmet1 and
A26: pmet1
is_a_pseudometric_of cT and for pq holds (pmet1
. pq)
<= s and for pmet19 st pmet1
= pmet19 holds pmet19 is
continuous by
A2;
((
lower_bound (pmet1,Q))
. p)
>
0 by
A24,
A25;
then
A27: (
lower_bound ((
dist (pmet1,p))
.: Q))
>
0 by
Def3;
(1
/ 2)
< 1;
then
|.(1
/ 2).|
< 1 by
ABSVALUE:def 1;
then Geo is
summable by
SERIES_1: 24;
then (s
(#) Geo) is
summable by
SERIES_1: 10;
then (Geo
(#) (FS2
# pq)) is
summable by
A23,
SERIES_1: 20;
then ((Geo
(#) (FS2
# pq))
. n)
=
0 by
A23,
A22,
RSSPACE: 17;
then
A28: ((Geo
. n)
* ((FS2
# pq)
. n))
=
0 by
SEQ_1: 8;
((1
/ 2)
|^ n)
>
0 by
NEWTON: 83;
then (Geo
. n)
<>
0 by
PREPOWER:def 1;
then
A29: ((FS2
# pq)
. n)
=
0 by
A28,
XCMPLX_1: 6;
A30: (pmet1
. (p,q))
= ((
dist (pmet1,p))
. q) by
Def2;
(
dom (
dist (pmet1,p)))
= cT & q
in Q by
FUNCT_2:def 1,
TARSKI:def 1;
then
A31: ((
dist (pmet1,p))
. q)
in ((
dist (pmet1,p))
.: Q) by
FUNCT_1:def 6;
((
dist (pmet1,p))
.: Q) is non
empty
bounded_below by
A26,
Lm1;
then ((
dist (pmet1,p))
. q)
>
0 by
A31,
A27,
SEQ_4:def 2;
hence thesis by
A25,
A29,
A30,
SEQFUNC:def 10;
end;
pmet
is_a_pseudometric_of cT by
A2,
A5,
Th15;
then pmet is
Reflexive
discerning
symmetric
triangle by
A18,
METRIC_1:def 3,
NAGATA_1:def 10;
then
A32: pmet
is_metric_of cT by
METRIC_6: 3;
hence ex pmet st pmet
is_metric_of the
carrier of T & for pq holds (pmet
. pq)
= (
Sum (((1
/ 2)
GeoSeq )
(#) (FS2
# pq))) by
A5;
for A be non
empty
Subset of T holds (
Cl A)
= { p where p be
Point of T : ((
lower_bound (pmet,A))
. p)
=
0 }
proof
let A be non
empty
Subset of T;
set INF = { p where p be
Point of T : ((
lower_bound (pmet,A))
. p)
=
0 };
A33: INF
c= (
Cl A)
proof
let x be
object;
assume x
in INF;
then
consider p be
Point of T such that
A34: x
= p and
A35: ((
lower_bound (pmet,A))
. p)
=
0 ;
A36: (
lower_bound ((
dist (pmet,p))
.: A))
=
0 by
A35,
Def3;
pmet
is_a_pseudometric_of cT by
A2,
A5,
Th15;
then
A37: ((
dist (pmet,p))
.: A) is non
empty
bounded_below by
Lm1;
A38: A
c= (
Cl A) & ex y be
object st y
in A by
PRE_TOPC: 18,
XBOOLE_0:def 1;
A39: A
c= (
Cl A) by
PRE_TOPC: 18;
assume not x
in (
Cl A);
then
consider n such that
A40: for pmet1 st (FS2
. n)
= pmet1 holds ((
lower_bound (pmet1,(
Cl A)))
. p)
>
0 by
A3,
A34,
A38;
((1
/ 2)
|^ n)
>
0 by
NEWTON: 83;
then
A41: (Geo
. n)
>
0 by
PREPOWER:def 1;
((1
/ 2)
|^ n)
>
0 by
NEWTON: 83;
then
A42: (Geo
. n)
>
0 by
PREPOWER:def 1;
consider pmet1 such that
A43: (FS2
. n)
= pmet1 and
A44: pmet1
is_a_pseudometric_of cT and for pq holds (pmet1
. pq)
<= s and for pmet19 st pmet1
= pmet19 holds pmet19 is
continuous by
A2;
set r = ((Geo
. n)
* ((
lower_bound (pmet1,(
Cl A)))
. p));
A45: (
lower_bound ((
dist (pmet1,p))
.: (
Cl A)))
= ((
lower_bound (pmet1,(
Cl A)))
. p) by
Def3;
A46: ((
lower_bound (pmet1,(
Cl A)))
. p)
>
0 by
A40,
A43;
then r
>
0 by
A41,
XREAL_1: 129;
then (r
/ 2)
>
0 by
XREAL_1: 215;
then
consider rn such that
A47: rn
in ((
dist (pmet,p))
.: A) and
A48: rn
< ((
lower_bound ((
dist (pmet,p))
.: A))
+ (r
/ 2)) by
A37,
SEQ_4:def 2;
consider a be
object such that
A49: a
in (
dom (
dist (pmet,p))) and
A50: a
in A and
A51: rn
= ((
dist (pmet,p))
. a) by
A47,
FUNCT_1:def 6;
reconsider a as
Point of T by
A49;
reconsider pa =
[p, a] as
Element of
[:cT, cT:];
A52: ((
dist (pmet1,p))
. a)
= (pmet1
. (p,a)) by
Def2;
(
dom (
dist (pmet1,p)))
= cT by
FUNCT_2:def 1;
then
A53: ((
dist (pmet1,p))
. a)
in ((
dist (pmet1,p))
.: (
Cl A)) by
A50,
A39,
FUNCT_1:def 6;
((
dist (pmet1,p))
.: (
Cl A)) is non
empty
bounded_below by
A44,
A50,
A39,
Lm1;
then ((
lower_bound (pmet1,(
Cl A)))
. p)
<= ((
dist (pmet1,p))
. a) by
A53,
A45,
SEQ_4:def 2;
then ((
lower_bound (pmet1,(
Cl A)))
. p)
<= ((FS2
# pa)
. n) by
A43,
A52,
SEQFUNC:def 10;
then r
<= ((Geo
. n)
* ((FS2
# pa)
. n)) by
A42,
XREAL_1: 64;
then
A54: r
<= ((Geo
(#) (FS2
# pa))
. n) by
SEQ_1: 8;
A55: for k holds
0
<= ((Geo
(#) (FS2
# pa))
. k) & ((Geo
(#) (FS2
# pa))
. k)
<= ((s
(#) Geo)
. k) by
A8;
(pmet
. pa)
= (pmet
. (p,a));
then
A56: rn
= (pmet
. pa) by
A51,
Def2;
(1
/ 2)
< 1;
then
|.(1
/ 2).|
< 1 by
ABSVALUE:def 1;
then Geo is
summable by
SERIES_1: 24;
then (s
(#) Geo) is
summable by
SERIES_1: 10;
then (Geo
(#) (FS2
# pa)) is
summable by
A55,
SERIES_1: 20;
then ((Geo
(#) (FS2
# pa))
. n)
<= (
Sum (Geo
(#) (FS2
# pa))) by
A55,
RSSPACE2: 3;
then rn
>= ((Geo
(#) (FS2
# pa))
. n) by
A5,
A56;
then ((Geo
(#) (FS2
# pa))
. n)
< (r
/ 2) by
A48,
A36,
XXREAL_0: 2;
then r
< (r
/ 2) by
A54,
XXREAL_0: 2;
hence thesis by
A41,
A46,
XREAL_1: 129,
XREAL_1: 216;
end;
(
Cl A)
c= INF
proof
let x be
object;
assume
A57: x
in (
Cl A);
then
reconsider p = x as
Point of T;
pmet
is_a_pseudometric_of cT & for pmet9 st pmet
= pmet9 holds pmet9 is
continuous by
A2,
A5,
Th15;
then ((
lower_bound (pmet,A))
. p)
=
0 by
A57,
Th16;
hence thesis;
end;
hence thesis by
A33;
end;
hence thesis by
A32,
Th10;
end;
theorem ::
NAGATA_2:18
Th18: for D be non
empty
set, p,q be
FinSequence of D, B be
BinOp of D st p is
one-to-one & q is
one-to-one & (
rng q)
c= (
rng p) & B is
commutative
associative & (B is
having_a_unity or (
len q)
>= 1 & (
len p)
> (
len q)) holds ex r be
FinSequence of D st r is
one-to-one & (
rng r)
= ((
rng p)
\ (
rng q)) & (B
"**" p)
= (B
. ((B
"**" q),(B
"**" r)))
proof
let D be non
empty
set, p,q be
FinSequence of D, B be
BinOp of D such that
A1: p is
one-to-one and
A2: q is
one-to-one and
A3: (
rng q)
c= (
rng p) and
A4: B is
commutative
associative and
A5: B is
having_a_unity or (
len q)
>= 1 & (
len p)
> (
len q);
A6: (
card (
rng p))
= (
len p) by
A1,
FINSEQ_4: 62;
consider r be
FinSequence such that
A7: (
rng r)
= ((
rng p)
\ (
rng q)) and
A8: r is
one-to-one by
FINSEQ_4: 58;
reconsider r as
FinSequence of D by
A7,
FINSEQ_1:def 4;
(
rng (q
^ r))
= ((
rng q)
\/ ((
rng p)
\ (
rng q))) by
A7,
FINSEQ_1: 31;
then
A9: (
rng (q
^ r))
= (
rng p) by
A3,
XBOOLE_1: 45;
(
rng r)
misses (
rng q) by
A7,
XBOOLE_1: 79;
then
A10: (q
^ r) is
one-to-one by
A2,
A8,
FINSEQ_3: 91;
then (
card (
rng (q
^ r)))
= (
len (q
^ r)) by
FINSEQ_4: 62;
then (
len q)
< ((
len q)
+ (
len r)) or B is
having_a_unity by
A5,
A9,
A6,
FINSEQ_1: 22;
then
A11: 1
<= (
len r) & 1
<= (
len q) & 1
<= (
len p) or B is
having_a_unity by
A5,
NAT_1: 19,
XXREAL_0: 2;
ex P be
Permutation of (
dom p) st (p
* P)
= (q
^ r) & (
dom P)
= (
dom p) & (
rng P)
= (
dom p) by
A1,
A10,
A9,
BHSP_5: 1;
then
A12: (B
"**" p)
= (B
"**" (q
^ r)) by
A4,
A11,
FINSOP_1: 7;
(B
"**" (q
^ r))
= (B
. ((B
"**" q),(B
"**" r))) by
A4,
A11,
FINSOP_1: 5;
hence thesis by
A7,
A8,
A12;
end;
Lm2: (
PairFunc
" )
= (
PairFunc qua
Function
" ) by
Th2,
TOPS_2:def 4;
reconsider jj = 1 as
Real;
::$Notion-Name
theorem ::
NAGATA_2:19
Th19: for T holds (T is
regular & T is
T_1 & ex Bn be
FamilySequence of T st Bn is
Basis_sigma_locally_finite) iff T is
metrizable
proof
let T;
thus (T is
regular & T is
T_1 & ex Bn be
FamilySequence of T st Bn is
Basis_sigma_locally_finite) implies T is
metrizable
proof
set cTT = the
carrier of
[:T, T:];
set bcT = (
bool the
carrier of T);
set cT = the
carrier of T;
assume that
A1: T is
regular and
A2: T is
T_1 and
A3: ex Bn be
FamilySequence of T st Bn is
Basis_sigma_locally_finite;
set Fun = (
Funcs (cTT,
REAL ));
consider Bn be
FamilySequence of T such that
A4: Bn is
Basis_sigma_locally_finite by
A3;
defpred
NN[
object,
object,
RealMap of
[:T, T:]] means ex pmet st $3
= pmet & $3 is
continuous & pmet
is_a_pseudometric_of cT & for p, q holds (pmet
.
[p, q])
<= 1 & for p, q st ex A, B st A is
open & B is
open & A
in (Bn
. $2) & B
in (Bn
. $1) & p
in A & (
Cl A)
c= B & not q
in B holds (pmet
.
[p, q])
= 1;
defpred
N[
object,
object] means ex F be
RealMap of
[:T, T:] st F
= $2 & for n, m st ((
PairFunc
" )
. $1)
=
[n, m] holds
NN[n, m, F];
A5: (
Union Bn) is
Basis of T by
A4,
NAGATA_1:def 6;
A6: Bn is
sigma_locally_finite by
A4,
NAGATA_1:def 6;
A7: for n, m holds ex pmet9 st
NN[n, m, pmet9]
proof
defpred
add9[
Element of Fun,
Element of Fun,
set] means ($1
+ $2)
= $3;
defpred
funcdist[
RealMap of T,
Function] means for p, q holds ($2
. (p,q))
=
|.(($1
. p)
- ($1
. q)).|;
let n, m;
deffunc
V(
object) = (
union { Q where Q be
Subset of T : ex D1 be
set st D1
= $1 & Q
in (Bn
. m) & (
Cl Q)
c= D1 });
set Bnn = (Bn
. n);
deffunc
s(
Subset of T) = { Q where Q be
Subset of T : Q
in (Bn
. n) & Q
meets $1 };
defpred
S[
set,
Subset of T] means $1
in $2 & $2 is
open &
s($2) is
finite;
A8: for A be
object st A
in bcT holds
V(A)
in bcT
proof
let A be
object such that A
in bcT;
set Um = { Q where Q be
Subset of T : ex D1 be
set st D1
= A & Q
in (Bn
. m) & (
Cl Q)
c= D1 };
now
let uv be
object;
assume uv
in
V(A);
then
consider v be
set such that
A9: uv
in v and
A10: v
in Um by
TARSKI:def 4;
ex B st v
= B & ex D1 be
set st D1
= A & B
in (Bn
. m) & (
Cl B)
c= D1 by
A10;
hence uv
in cT by
A9;
end;
then
V(A)
c= cT;
hence thesis;
end;
consider Vm be
Function of bcT, bcT such that
A11: for A be
object st A
in bcT holds (Vm
. A)
=
V(A) from
FUNCT_2:sch 2(
A8);
defpred
F[
object,
object] means ex F be
RealMap of T, S be
Subset of T st S
= $1 & F
= $2 & F is
continuous & (for p holds
0
<= (F
. p) & (F
. p)
<= 1 & (p
in (S
` ) implies (F
. p)
=
0 ) & (p
in (
Cl (Vm
. S)) implies (F
. p)
= 1));
A12: m
in
NAT by
ORDINAL1:def 12;
A13: (Bn
. m) is
locally_finite by
A6,
NAGATA_1:def 3,
A12;
A14: for A holds (
Cl (Vm
. A))
c= A
proof
let A;
set VmA = { Q where Q be
Subset of T : ex D1 be
set st D1
= A & Q
in (Bn
. m) & (
Cl Q)
c= D1 };
VmA
c= bcT
proof
let B be
object;
assume B
in VmA;
then ex C st B
= C & ex D1 be
set st D1
= A & C
in (Bn
. m) & (
Cl C)
c= D1;
hence thesis;
end;
then
reconsider VmA as
Subset-Family of T;
A15: (
union (
clf VmA))
c= A
proof
let ClBu be
object;
assume ClBu
in (
union (
clf VmA));
then
consider ClB be
set such that
A16: ClBu
in ClB and
A17: ClB
in (
clf VmA) by
TARSKI:def 4;
reconsider ClB as
Subset of T by
A17;
consider B such that
A18: (
Cl B)
= ClB and
A19: B
in VmA by
A17,
PCOMPS_1:def 2;
ex C st B
= C & ex D1 be
set st D1
= A & C
in (Bn
. m) & (
Cl C)
c= D1 by
A19;
hence thesis by
A16,
A18;
end;
VmA
c= (Bn
. m)
proof
let B be
object;
assume B
in VmA;
then ex C st B
= C & ex D1 be
set st D1
= A & C
in (Bn
. m) & (
Cl C)
c= D1;
hence thesis;
end;
then
A20: (
Cl (
union VmA))
= (
union (
clf VmA)) by
A13,
PCOMPS_1: 9,
PCOMPS_1: 20;
(Vm
. A)
=
V(A) by
A11;
hence (
Cl (Vm
. A))
c= A by
A15,
A20;
end;
A21: for A be
object st A
in Bnn holds ex f be
object st f
in (
Funcs (cT,
REAL )) &
F[A, f]
proof
let A be
object;
assume A
in Bnn;
then
A22: A
in (
Union Bn) by
PROB_1: 12;
(
Union Bn)
c= the
topology of T by
A5,
TOPS_2: 64;
then
reconsider A as
open
Subset of T by
A22,
PRE_TOPC:def 2;
(A
` )
misses A by
XBOOLE_1: 79;
then
A23: (A
` )
misses (
Cl (Vm
. A)) by
A14,
XBOOLE_1: 63;
T is
normal by
A1,
A4,
NAGATA_1: 20;
then
consider f be
Function of T,
R^1 such that
A24: f is
continuous & for p holds
0
<= (f
. p) & (f
. p)
<= 1 & (p
in (A
` ) implies (f
. p)
=
0 ) & (p
in (
Cl (Vm
. A)) implies (f
. p)
= 1) by
A23,
URYSOHN3: 20;
reconsider f9 = f as
RealMap of T by
TOPMETR: 17;
A25: ex F be
RealMap of T, S be
Subset of T st S
= A & F
= f9 & F is
continuous & for p holds
0
<= (F
. p) & (F
. p)
<= 1 & (p
in (S
` ) implies (F
. p)
=
0 ) & (p
in (
Cl (Vm
. S)) implies (F
. p)
= 1)
proof
take f9, A;
thus thesis by
A24,
JORDAN5A: 27;
end;
f9
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
hence thesis by
A25;
end;
consider Fn be
Function of Bnn, (
Funcs (cT,
REAL )) such that
A26: for A be
object st A
in Bnn holds
F[A, (Fn
. A)] from
FUNCT_2:sch 1(
A21);
A27: n
in
NAT by
ORDINAL1:def 12;
(Bn
. n) is
locally_finite by
A6,
NAGATA_1:def 3,
A27;
then
A28: for p be
Element of cT holds ex A be
Element of bcT st
S[p, A] by
PCOMPS_1:def 1;
consider Sx be
Function of cT, bcT such that
A29: for p be
Element of cT holds
S[p, (Sx
. p)] from
FUNCT_2:sch 3(
A28);
defpred
ss[
object,
object] means for x,y be
Element of T st $1
=
[x, y] holds $2
=
[:(Sx
. x), (Sx
. y):];
A30: for pq9 be
object st pq9
in cTT holds ex SS be
object st SS
in (
bool cTT) &
ss[pq9, SS]
proof
let pq9 be
object;
assume pq9
in cTT;
then pq9
in
[:cT, cT:] by
BORSUK_1:def 2;
then
consider p,q be
object such that
A31: p
in cT & q
in cT and
A32: pq9
=
[p, q] by
ZFMISC_1:def 2;
reconsider p, q as
Point of T by
A31;
now
let p1,q1 be
Point of T;
assume
A33: pq9
=
[p1, q1];
then p1
= p by
A32,
XTUPLE_0: 1;
hence
[:(Sx
. p), (Sx
. q):]
=
[:(Sx
. p1), (Sx
. q1):] by
A32,
A33,
XTUPLE_0: 1;
end;
hence thesis;
end;
consider SS be
Function of cTT, (
bool cTT) such that
A34: for pq be
object st pq
in cTT holds
ss[pq, (SS
. pq)] from
FUNCT_2:sch 1(
A30);
A35: for pq9 holds pq9
in (SS
. pq9) & (SS
. pq9) is
open
proof
let pq9 be
Point of
[:T, T:];
pq9
in cTT;
then pq9
in
[:cT, cT:] by
BORSUK_1:def 2;
then
consider p,q be
object such that
A36: p
in cT & q
in cT and
A37: pq9
=
[p, q] by
ZFMISC_1:def 2;
reconsider p, q as
Point of T by
A36;
A38: p
in (Sx
. p) & q
in (Sx
. q) by
A29;
A39: (Sx
. p) is
open & (Sx
. q) is
open by
A29;
(SS
. pq9)
=
[:(Sx
. p), (Sx
. q):] by
A34,
A37;
hence thesis by
A37,
A38,
A39,
BORSUK_1: 6,
ZFMISC_1:def 2;
end;
A40: for f,g be
Element of Fun holds ex fg be
Element of Fun st
add9[f, g, fg]
proof
let f,g be
Element of Fun;
set f9 = f, g9 = g;
(f9
+ g9)
in Fun by
FUNCT_2: 8;
hence thesis;
end;
consider ADD be
BinOp of (
Funcs (the
carrier of
[:T, T:],
REAL )) such that
A41: for f,g be
Element of Fun holds
add9[f, g, (ADD
. (f,g))] from
BINOP_1:sch 3(
A40);
A42: for f be
Element of (
Funcs (cT,
REAL )) holds ex fxy be
Element of Fun st
funcdist[f, fxy]
proof
let f be
Element of (
Funcs (cT,
REAL ));
defpred
fd[
Element of T,
Element of T,
object] means $3
=
|.((f
. $1)
- (f
. $2)).|;
A43: for x,y be
Element of cT holds ex r be
Element of
REAL st
fd[x, y, r]
proof
let x,y be
Element of cT;
consider r be
Real such that
A44:
fd[x, y, r];
reconsider r as
Element of
REAL by
XREAL_0:def 1;
fd[x, y, r] by
A44;
hence thesis;
end;
consider Fd be
Function of
[:cT, cT:],
REAL such that
A45: for x,y be
Element of cT holds
fd[x, y, (Fd
. (x,y))] from
BINOP_1:sch 3(
A43);
[:cT, cT:]
= cTT by
BORSUK_1:def 2;
then Fd
in Fun by
FUNCT_2: 8;
hence thesis by
A45;
end;
consider Fdist be
Function of (
Funcs (cT,
REAL )), Fun such that
A46: for fd be
Element of (
Funcs (cT,
REAL )) holds
funcdist[fd, (Fdist
. fd)] from
FUNCT_2:sch 3(
A42);
deffunc
Fx(
Element of T) = { (Fn
. A) where A be
Subset of T : A
in (Bn
. n) & A
in
s(.) };
deffunc
RNG(
set) = { (Fdist
. fd) where fd be
RealMap of T : fd
in $1 };
defpred
gxy[
set,
Function] means $2 is
one-to-one & ex p, q st
[p, q]
= $1 & (
rng $2)
=
RNG(\/);
A47: for p holds
Fx(p) is
finite
proof
deffunc
Fxx(
Subset of T) = (Fn
. $1);
let p;
set SFxx = {
Fxx(A) where A be
Subset of T : A
in
s(.) };
A48:
Fx(p)
c= SFxx
proof
let FA be
object;
assume FA
in
Fx(p);
then ex A st FA
= (Fn
. A) & A
in (Bn
. n) & A
in
s(.);
hence thesis;
end;
A49:
s(.) is
finite by
A29;
SFxx is
finite from
FRAENKEL:sch 21(
A49);
hence thesis by
A48;
end;
A50: for p, q holds
RNG(\/) is
finite &
RNG(\/)
c= Fun
proof
deffunc
FD(
RealMap of T) = (Fdist
. $1);
let p, q;
A51:
RNG(\/)
c= Fun
proof
let FDm be
object;
assume FDm
in
RNG(\/);
then
consider fd be
RealMap of T such that
A52: FDm
= (Fdist
. fd) and fd
in (
Fx(p)
\/
Fx(q));
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
hence thesis by
A52,
FUNCT_2: 5;
end;
set RNG9 = {
FD(fd) where fd be
Element of (
Funcs (cT,
REAL )) : fd
in (
Fx(p)
\/
Fx(q)) };
A53:
RNG(\/)
c= RNG9
proof
let Fdistfd be
object;
assume Fdistfd
in
RNG(\/);
then
consider fd be
RealMap of T such that
A54: Fdistfd
= (Fdist
. fd) & fd
in (
Fx(p)
\/
Fx(q));
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
hence thesis by
A54;
end;
Fx(p) is
finite &
Fx(q) is
finite by
A47;
then
A55: (
Fx(p)
\/
Fx(q)) is
finite;
RNG9 is
finite from
FRAENKEL:sch 21(
A55);
hence thesis by
A51,
A53;
end;
A56: for pq be
Element of cTT holds ex G be
Element of (Fun
* ) st
gxy[pq, G]
proof
let pq be
Element of cTT;
pq
in the
carrier of
[:T, T:];
then pq
in
[:cT, cT:] by
BORSUK_1:def 2;
then
consider p,q be
object such that
A57: p
in cT & q
in cT and
A58: pq
=
[p, q] by
ZFMISC_1:def 2;
reconsider p, q as
Point of T by
A57;
consider SF be
FinSequence such that
A59: (
rng SF)
=
RNG(\/) and
A60: SF is
one-to-one by
A50,
FINSEQ_4: 58;
(
rng SF)
c= Fun by
A50,
A59;
then
reconsider SF as
FinSequence of Fun by
FINSEQ_1:def 4;
SF
in (Fun
* ) by
FINSEQ_1:def 11;
hence thesis by
A58,
A59,
A60;
end;
consider SFdist be
Function of cTT, (Fun
* ) such that
A61: for pq be
Element of cTT holds
gxy[pq, (SFdist
. pq)] from
FUNCT_2:sch 3(
A56);
defpred
SFdist[
object,
object] means for FS be
FinSequence of Fun st FS
= (SFdist
. $1) holds $2
= (ADD
"**" FS);
A62: for pq be
object st pq
in cTT holds ex S be
object st S
in Fun &
SFdist[pq, S]
proof
let pq be
object;
assume pq
in cTT;
then (SFdist
. pq)
in (Fun
* ) by
FUNCT_2: 5;
then
reconsider SF = (SFdist
. pq) as
FinSequence of Fun by
FINSEQ_1:def 11;
for FS be
FinSequence of (
Funcs (cTT,
REAL )) st FS
= (SFdist
. pq) holds (ADD
"**" FS)
= (ADD
"**" SF);
hence thesis;
end;
consider SumFdist be
Function of cTT, (
Funcs (cTT,
REAL )) such that
A63: for xy be
object st xy
in cTT holds
SFdist[xy, (SumFdist
. xy)] from
FUNCT_2:sch 1(
A62);
reconsider SumFdist9 = SumFdist as
Function of cTT, (
Funcs (cTT,the
carrier of
R^1 )) by
TOPMETR: 17;
reconsider SumFTS9 = (SumFdist9
Toler ) as
RealMap of
[:T, T:] by
TOPMETR: 17;
cTT
=
[:cT, cT:] by
BORSUK_1:def 2;
then
reconsider SumFTS = (SumFdist9
Toler ) as
Function of
[:cT, cT:],
REAL by
TOPMETR: 17;
A64: for f1,f2 be
RealMap of
[:T, T:] holds (ADD
. (f1,f2))
= (f1
+ f2)
proof
let f1,f2 be
RealMap of
[:T, T:];
reconsider f19 = f1, f29 = f2 as
Element of Fun by
FUNCT_2: 8;
(ADD
. (f19,f29))
= (f19
+ f29) by
A41;
hence thesis;
end;
A65: for p, q st ex A, B st A is
open & B is
open & A
in (Bn
. m) & B
in (Bn
. n) & p
in A & (
Cl A)
c= B & not q
in B holds (SumFTS9
.
[p, q])
>= 1
proof
let p, q;
assume ex A, B st A is
open & B is
open & A
in (Bn
. m) & B
in (Bn
. n) & p
in A & (
Cl A)
c= B & not q
in B;
then
consider A, B such that A is
open and B is
open and
A66: A
in (Bn
. m) and
A67: B
in (Bn
. n) and
A68: p
in A and
A69: (
Cl A)
c= B and
A70: not q
in B;
A71:
F[B, (Fn
. B)] by
A26,
A67;
A
in { Q where Q be
Subset of T : ex D1 be
set st D1
= B & Q
in (Bn
. m) & (
Cl Q)
c= D1 } by
A66,
A69;
then A
c=
V(B) by
ZFMISC_1: 74;
then
A72: A
c= (Vm
. B) by
A11;
(Vm
. B)
c= (
Cl (Vm
. B)) by
PRE_TOPC: 18;
then
A73: p
in (
Cl (Vm
. B)) by
A68,
A72;
(
Cl (Vm
. B))
c= B & p
in (Sx
. p) by
A14,
A29;
then (Sx
. p)
meets B by
A73,
XBOOLE_0: 3;
then
A74: B
in
s(.) by
A67;
reconsider pq =
[p, q] as
Point of
[:T, T:] by
BORSUK_1:def 2;
reconsider SF = (SFdist
. pq) as
FinSequence of Fun by
FINSEQ_1:def 11;
consider x,y be
Point of T such that
A75:
[x, y]
= pq and
A76: (
rng SF)
=
RNG(\/) by
A61;
reconsider ASF = (ADD
"**" SF) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
assume
A77: (SumFTS9
.
[p, q])
< 1;
reconsider FnB = (Fn
. B) as
RealMap of T by
A67,
FUNCT_2: 5,
FUNCT_2: 66;
A78: FnB
in (
Funcs (cT,
REAL )) by
A67,
FUNCT_2: 5;
q
in (B
` ) by
A70,
XBOOLE_0:def 5;
then
A79: (FnB
. q)
=
0 by
A71;
x
= p by
A75,
XTUPLE_0: 1;
then FnB
in
Fx(x) by
A67,
A74;
then FnB
in (
Fx(x)
\/
Fx(y)) by
XBOOLE_0:def 3;
then
A80: (Fdist
. FnB)
in (
rng SF) by
A76;
then
reconsider FdistFnB = (Fdist
. FnB) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
SF
<>
{} by
A80,
RELAT_1: 38;
then (
len SF)
>= 1 by
NAT_1: 14;
then
consider F be
sequence of Fun such that
A81: (F
. 1)
= (SF
. 1) and
A82: for n be
Nat st
0
<> n & n
< (
len SF) holds (F
. (n
+ 1))
= (ADD
. ((F
. n),(SF
. (n
+ 1)))) and
A83: (ADD
"**" SF)
= (F
. (
len SF)) by
FINSOP_1:def 1;
A84: (SumFTS
. pq)
= ((SumFdist
. pq)
. pq) & (SumFdist
. pq)
= ASF by
A63,
NAGATA_1:def 8;
defpred
P[
Nat] means for k st k
<>
0 & k
<= $1 & $1
<= (
len SF) holds for fk,Fn be
RealMap of
[:T, T:] st fk
= (SF
. k) & Fn
= (F
. $1) holds (fk
. pq)
<= (Fn
. pq);
A85: for k st k
<>
0 & k
<= (
len SF) holds for f be
RealMap of
[:T, T:] st f
= (SF
. k) holds (f
. pq)
>=
0
proof
let k such that
A86: k
<>
0 and
A87: k
<= (
len SF);
k
>= 1 by
A86,
NAT_1: 14;
then k
in (
dom SF) by
A87,
FINSEQ_3: 25;
then (SF
. k)
in
RNG(\/) by
A76,
FUNCT_1:def 3;
then
consider fd be
RealMap of T such that
A88: (Fdist
. fd)
= (SF
. k) and fd
in (
Fx(x)
\/
Fx(y));
let f be
RealMap of
[:T, T:] such that
A89: f
= (SF
. k);
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then (f
. (p,q))
=
|.((fd
. p)
- (fd
. q)).| by
A46,
A89,
A88;
hence thesis by
COMPLEX1: 46;
end;
A90: for i holds
P[i] implies
P[(i
+ 1)]
proof
let i;
assume
A91:
P[i];
let k such that
A92: k
<>
0 and
A93: k
<= (i
+ 1) and
A94: (i
+ 1)
<= (
len SF);
now
1
<= (i
+ 1) by
NAT_1: 14;
then (i
+ 1)
in (
dom SF) by
A94,
FINSEQ_3: 25;
then (SF
. (i
+ 1))
in (
rng SF) by
FUNCT_1:def 3;
then
reconsider SFi1 = (SF
. (i
+ 1)) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
reconsider Fi = (F
. i) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
let fk,Fn be
RealMap of
[:T, T:] such that
A95: fk
= (SF
. k) and
A96: Fn
= (F
. (i
+ 1));
per cases by
A93,
XXREAL_0: 1;
suppose
A97: k
< (i
+ 1);
A98: i
< (
len SF) by
A94,
NAT_1: 13;
i
<>
0 by
A92,
A97,
NAT_1: 13;
then (F
. (i
+ 1))
= (ADD
. ((F
. i),(SF
. (i
+ 1)))) by
A82,
A98;
then
A99: Fn
= (Fi
+ SFi1) by
A64,
A96;
(SFi1
. pq)
>=
0 by
A85,
A94;
then ((Fi
. pq)
+
0 )
<= ((Fi
. pq)
+ (SFi1
. pq)) by
XREAL_1: 7;
then
A100: (Fn
. pq)
>= (Fi
. pq) by
A99,
NAGATA_1:def 7;
A101: i
<= (
len SF) by
A94,
NAT_1: 13;
k
<= i by
A97,
NAT_1: 13;
then (fk
. pq)
<= (Fi
. pq) by
A91,
A92,
A95,
A101;
hence (fk
. pq)
<= (Fn
. pq) by
A100,
XXREAL_0: 2;
end;
suppose
A102: k
= (i
+ 1);
per cases ;
suppose i
=
0 ;
hence (fk
. pq)
<= (Fn
. pq) by
A81,
A95,
A96,
A102;
end;
suppose
A103: i
<>
0 ;
(i
+
0 )
< (i
+ 1) by
XREAL_1: 8;
then
A104: i
< (
len SF) by
A94,
XXREAL_0: 2;
1
<= i by
A103,
NAT_1: 14;
then i
in (
dom SF) by
A104,
FINSEQ_3: 25;
then (SF
. i)
in (
rng SF) by
FUNCT_1:def 3;
then
reconsider SFi = (SF
. i) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
0
<= (SFi
. pq) by
A85,
A103,
A104;
then
0
<= (Fi
. pq) by
A91,
A103,
A104;
then
A105: ((Fi
. pq)
+ (fk
. pq))
>= (
0
+ (fk
. pq)) by
XREAL_1: 7;
(F
. (i
+ 1))
= (ADD
. ((F
. i),(SF
. (i
+ 1)))) by
A82,
A103,
A104;
then Fn
= (Fi
+ fk) by
A64,
A95,
A96,
A102;
hence (fk
. pq)
<= (Fn
. pq) by
A105,
NAGATA_1:def 7;
end;
end;
end;
hence thesis;
end;
A106:
P[
0 ];
A107: for i holds
P[i] from
NAT_1:sch 2(
A106,
A90);
consider k be
object such that
A108: k
in (
dom SF) and
A109: (SF
. k)
= (Fdist
. FnB) by
A80,
FUNCT_1:def 3;
A110: k
in (
Seg (
len SF)) by
A108,
FINSEQ_1:def 3;
(FnB
. p)
= 1 by
A73,
A71;
then
A111: (FdistFnB
. (p,q))
=
|.(1
-
0 ).| by
A46,
A78,
A79;
reconsider k as
Element of
NAT by
A108;
A112:
|.1.|
= 1 by
ABSVALUE:def 1;
k
<>
0 & k
<= (
len SF) by
A110,
FINSEQ_1: 1;
hence thesis by
A77,
A84,
A83,
A107,
A111,
A112,
A109;
end;
A113:
now
let p, q;
assume ex A, B st A is
open & B is
open & A
in (Bn
. m) & B
in (Bn
. n) & p
in A & (
Cl A)
c= B & not q
in B;
then (SumFTS9
.
[p, q])
>= 1 by
A65;
then
A114: 1
= (
min (1,(SumFTS9
.
[p, q]))) by
XXREAL_0:def 9;
[:cT, cT:]
= cTT by
BORSUK_1:def 2;
hence 1
= ((
min (jj,SumFTS9))
.
[p, q]) by
A114,
NAGATA_1:def 9;
end;
A115: for pq be
Element of cTT, map9 be
Element of Fun st map9
is_a_unity_wrt ADD holds (map9
. pq)
=
0
proof
let pq be
Element of cTT, map9 be
Element of Fun;
assume map9
is_a_unity_wrt ADD;
then (ADD
. (map9,map9))
= map9 by
BINOP_1: 3;
then ((map9
+ map9)
. pq)
= (map9
. pq) by
A41;
then ((map9
. pq)
+ (map9
. pq))
= (map9
. pq) by
NAGATA_1:def 7;
hence thesis;
end;
A116: for pq1,pq2 be
Point of
[:T, T:] holds (pq1
in (SS
. pq2) implies ((SumFdist
. pq1)
. pq1)
= ((SumFdist
. pq2)
. pq1)) & for SumFdist1,SumFdist2 be
RealMap of
[:T, T:] st SumFdist1
= (SumFdist
. pq1) & SumFdist2
= (SumFdist
. pq2) holds (SumFdist1
. pq1)
>= (SumFdist2
. pq1)
proof
deffunc
No0(
Element of T,
Element of T) = { (Fn
. A) where A be
Subset of T : A
in (Bn
. n) & for FnA be
RealMap of T st (Fn
. A)
= FnA holds ((FnA
. $1)
>
0 or (FnA
. $2)
>
0 ) };
let pq1,pq2 be
Point of
[:T, T:];
reconsider S1 = (SFdist
. pq1), S2 = (SFdist
. pq2) as
FinSequence of Fun by
FINSEQ_1:def 11;
consider p1,q1 be
Point of T such that
A117:
[p1, q1]
= pq1 and
A118: (
rng S1)
=
RNG(\/) by
A61;
A119: for p,q,p1,q1 be
Point of T st
[p, q]
in (SS
.
[p1, q1]) holds
No0(p,q)
c= (
Fx(p1)
\/
Fx(q1))
proof
let p,q,p1,q1 be
Point of T such that
A120:
[p, q]
in (SS
.
[p1, q1]);
reconsider pq1 =
[p1, q1] as
Element of cTT by
BORSUK_1:def 2;
[:(Sx
. p1), (Sx
. q1):]
= (SS
. pq1) by
A34;
then
A121: p
in (Sx
. p1) & q
in (Sx
. q1) by
A120,
ZFMISC_1: 87;
let no0 be
object;
assume no0
in
No0(p,q);
then
consider A be
Subset of T such that
A122: no0
= (Fn
. A) and
A123: A
in (Bn
. n) and
A124: for FnA be
RealMap of T st (Fn
. A)
= FnA holds ((FnA
. p)
>
0 or (FnA
. q)
>
0 );
reconsider FnA = (Fn
. A) as
RealMap of T by
A123,
FUNCT_2: 5,
FUNCT_2: 66;
A125: (FnA
. p)
>
0 or (FnA
. q)
>
0 by
A124;
F[A, (Fn
. A)] by
A26,
A123;
then not p
in (cT
\ A) or not q
in (cT
\ A) by
A125;
then p
in A or q
in A by
XBOOLE_0:def 5;
then A
meets (Sx
. p1) or A
meets (Sx
. q1) by
A121,
XBOOLE_0: 3;
then A
in
s(.) or A
in
s(.) by
A123;
then FnA
in
Fx(p1) or FnA
in
Fx(q1) by
A123;
hence thesis by
A122,
XBOOLE_0:def 3;
end;
A126:
RNG(No0)
c=
RNG(\/)
proof
p1
in (Sx
. p1) & q1
in (Sx
. q1) by
A29;
then
[p1, q1]
in
[:(Sx
. p1), (Sx
. q1):] by
ZFMISC_1: 87;
then
[p1, q1]
in (SS
.
[p1, q1]) by
A34;
then
A127:
No0(p1,q1)
c= (
Fx(p1)
\/
Fx(q1)) by
A119;
let FD be
object;
assume FD
in
RNG(No0);
then ex fd be
RealMap of T st FD
= (Fdist
. fd) & fd
in
No0(p1,q1);
hence thesis by
A127;
end;
A128: for f be
FinSequence of (
Funcs (cTT,
REAL )), p,q,p1,q1 be
Point of T st (
rng f)
= (
RNG(\/)
\
RNG(No0)) holds ((ADD
"**" f)
.
[p, q])
=
0
proof
let f be
FinSequence of (
Funcs (cTT,
REAL )), p,q,p1,q1 be
Point of T such that
A129: (
rng f)
= (
RNG(\/)
\
RNG(No0));
reconsider pq =
[p, q] as
Element of cTT by
BORSUK_1:def 2;
now
per cases ;
suppose
A130: (
len f)
=
0 ;
A131: ADD is
having_a_unity by
A64,
NAGATA_1: 23;
then
A132: ex f be
Element of Fun st f
is_a_unity_wrt ADD by
SETWISEO:def 2;
(ADD
"**" f)
= (
the_unity_wrt ADD) by
A130,
A131,
FINSOP_1:def 1;
then (ADD
"**" f)
is_a_unity_wrt ADD by
A132,
BINOP_1:def 8;
hence ((ADD
"**" f)
. pq)
=
0 by
A115;
end;
suppose
A133: (
len f)
<>
0 ;
then (
len f)
>= 1 by
NAT_1: 14;
then
consider F be
sequence of Fun such that
A134: (F
. 1)
= (f
. 1) and
A135: for n be
Nat st
0
<> n & n
< (
len f) holds (F
. (n
+ 1))
= (ADD
. ((F
. n),(f
. (n
+ 1)))) and
A136: (ADD
"**" f)
= (F
. (
len f)) by
FINSOP_1:def 1;
defpred
R[
Nat] means $1
<>
0 & $1
<= (
len f) implies ((F
. $1)
. pq)
=
0 ;
A137: for k holds
R[k] implies
R[(k
+ 1)]
proof
let k;
assume
A138:
R[k];
assume that (k
+ 1)
<>
0 and
A139: (k
+ 1)
<= (
len f);
A140: k
< (
len f) by
A139,
NAT_1: 13;
(k
+ 1)
>= 1 by
NAT_1: 14;
then (k
+ 1)
in (
dom f) by
A139,
FINSEQ_3: 25;
then
A141: (f
. (k
+ 1))
in (
RNG(\/)
\
RNG(No0)) by
A129,
FUNCT_1:def 3;
then (f
. (k
+ 1))
in
RNG(\/);
then
consider fd be
RealMap of T such that
A142: (Fdist
. fd)
= (f
. (k
+ 1)) and
A143: fd
in (
Fx(p1)
\/
Fx(q1));
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then
reconsider Fdistfd = (Fdist
. fd), Fk1 = (F
. (k
+ 1)), Fk = (F
. k), fk1 = (f
. (k
+ 1)) as
RealMap of
[:T, T:] by
A142,
FUNCT_2: 5,
FUNCT_2: 66;
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then
A144: (Fdistfd
. (p,q))
=
|.((fd
. p)
- (fd
. q)).| by
A46;
A145: not (f
. (k
+ 1))
in
RNG(No0) by
A141,
XBOOLE_0:def 5;
A146: (fd
. p)
=
0 & (fd
. q)
=
0
proof
assume
A147: (fd
. p)
<>
0 or (fd
. q)
<>
0 ;
per cases by
A143,
XBOOLE_0:def 3;
suppose fd
in
Fx(p1);
then
consider A be
Subset of T such that
A148: fd
= (Fn
. A) and
A149: A
in (Bn
. n) and A
in
s(.);
A150:
F[A, (Fn
. A)] by
A26,
A149;
not fd
in
No0(p,q) by
A145,
A142;
then ex FnA be
RealMap of T st (Fn
. A)
= FnA & ( not (FnA
. p)
>
0 ) & not (FnA
. q)
>
0 by
A148,
A149;
hence contradiction by
A147,
A148,
A150;
end;
suppose fd
in
Fx(q1);
then
consider A be
Subset of T such that
A151: fd
= (Fn
. A) and
A152: A
in (Bn
. n) and A
in
s(.);
A153:
F[A, (Fn
. A)] by
A26,
A152;
not fd
in
No0(p,q) by
A145,
A142;
then ex FnA be
RealMap of T st (Fn
. A)
= FnA & ( not (FnA
. p)
>
0 ) & not (FnA
. q)
>
0 by
A151,
A152;
hence contradiction by
A147,
A151,
A153;
end;
end;
per cases ;
suppose k
=
0 ;
hence thesis by
A134,
A142,
A146,
A144,
ABSVALUE: 2;
end;
suppose
A154: k
>
0 ;
then Fk1
= (ADD
. (Fk,fk1)) by
A135,
A140;
then Fk1
= (Fk
+ fk1) by
A64;
then (Fk1
. pq)
= (
0
+ (fk1
. pq)) by
A138,
A139,
A154,
NAGATA_1:def 7,
NAT_1: 13;
hence thesis by
A142,
A146,
A144,
ABSVALUE: 2;
end;
end;
A155:
R[
0 ];
for n holds
R[n] from
NAT_1:sch 2(
A155,
A137);
hence ((ADD
"**" f)
. pq)
=
0 by
A133,
A136;
end;
end;
hence thesis;
end;
A156:
RNG(\/) is
finite by
A50;
then
consider No be
FinSequence such that
A157: (
rng No)
=
RNG(No0) and
A158: No is
one-to-one by
A126,
FINSEQ_4: 58;
RNG(\/)
c= Fun by
A50;
then
A159:
RNG(No0)
c= Fun by
A126;
then
reconsider No as
FinSequence of Fun by
A157,
FINSEQ_1:def 4;
consider p2,q2 be
Point of T such that
A160:
[p2, q2]
= pq2 and
A161: (
rng S2)
=
RNG(\/) by
A61;
reconsider S1 = (SFdist
. pq1), S2 = (SFdist
. pq2) as
FinSequence of Fun by
FINSEQ_1:def 11;
set RNiS2 = (
RNG(No0)
/\
RNG(\/));
A162: S2 is
one-to-one by
A61;
A163: ADD is
having_a_unity & ADD is
commutative
associative by
A64,
NAGATA_1: 23;
S1 is
one-to-one by
A61;
then
consider S1No be
FinSequence of Fun such that S1No is
one-to-one and
A164: (
rng S1No)
= ((
rng S1)
\ (
rng No)) and
A165: (ADD
"**" S1)
= (ADD
. ((ADD
"**" No),(ADD
"**" S1No))) by
A118,
A126,
A157,
A158,
A163,
Th18;
consider NoiS2 be
FinSequence such that
A166: (
rng NoiS2)
= RNiS2 and
A167: NoiS2 is
one-to-one by
A126,
A156,
FINSEQ_4: 58;
RNiS2
c=
RNG(No0) by
XBOOLE_1: 17;
then RNiS2
c= Fun by
A159;
then
reconsider NoiS2 as
FinSequence of Fun by
A166,
FINSEQ_1:def 4;
(
rng NoiS2)
c= (
rng No) by
A157,
A166,
XBOOLE_1: 17;
then
consider NoNoiS2 be
FinSequence of Fun such that NoNoiS2 is
one-to-one and
A168: (
rng NoNoiS2)
= ((
rng No)
\ (
rng NoiS2)) and
A169: (ADD
"**" No)
= (ADD
. ((ADD
"**" NoiS2),(ADD
"**" NoNoiS2))) by
A158,
A163,
A167,
Th18;
(
rng NoiS2)
c= (
rng S2) by
A161,
A166,
XBOOLE_1: 17;
then
consider S2No be
FinSequence of Fun such that S2No is
one-to-one and
A170: (
rng S2No)
= ((
rng S2)
\ (
rng NoiS2)) and
A171: (ADD
"**" S2)
= (ADD
. ((ADD
"**" NoiS2),(ADD
"**" S2No))) by
A163,
A167,
A162,
Th18;
reconsider ANoNoiS2 = (ADD
"**" NoNoiS2), ANo = (ADD
"**" No), AS1No = (ADD
"**" S1No), AS2No = (ADD
"**" S2No), ANoiS2 = (ADD
"**" NoiS2), AS1 = (ADD
"**" S1), AS2 = (ADD
"**" S2) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
(
rng S2No)
= (
RNG(\/)
\
RNG(No0)) by
A161,
A166,
A170,
XBOOLE_1: 47;
then
A172: (AS2No
. pq1)
=
0 by
A128,
A117;
ANo
= (ANoiS2
+ ANoNoiS2) by
A64,
A169;
then
A173: (ANo
. pq1)
= ((ANoiS2
. pq1)
+ (ANoNoiS2
. pq1)) by
NAGATA_1:def 7;
AS1
= (ANo
+ AS1No) by
A64,
A165;
then
A174: (AS1
. pq1)
= ((ANo
. pq1)
+ (AS1No
. pq1)) by
NAGATA_1:def 7;
AS2
= (ANoiS2
+ AS2No) by
A64,
A171;
then
A175: (AS2
. pq1)
= ((ANoiS2
. pq1)
+ (AS2No
. pq1)) by
NAGATA_1:def 7;
A176: (AS1No
. pq1)
=
0 by
A128,
A117,
A118,
A157,
A164;
thus pq1
in (SS
. pq2) implies ((SumFdist
. pq1)
. pq1)
= ((SumFdist
. pq2)
. pq1)
proof
A177: ADD is
having_a_unity by
A64,
NAGATA_1: 23;
then
A178: ex f be
Element of Fun st f
is_a_unity_wrt ADD by
SETWISEO:def 2;
assume
A179: pq1
in (SS
. pq2);
now
let FD be
object;
assume FD
in
RNG(No0);
then
A180: ex fd be
RealMap of T st FD
= (Fdist
. fd) & fd
in
No0(p1,q1);
No0(p1,q1)
c= (
Fx(p2)
\/
Fx(q2)) by
A119,
A117,
A160,
A179;
hence FD
in
RNG(\/) by
A180;
end;
then
RNG(No0)
c=
RNG(\/);
then RNiS2
=
RNG(No0) by
XBOOLE_1: 28;
then (
rng NoNoiS2)
=
{} by
A157,
A166,
A168,
XBOOLE_1: 37;
then NoNoiS2
=
{} by
RELAT_1: 41;
then (
len NoNoiS2)
=
0 ;
then (ADD
"**" NoNoiS2)
= (
the_unity_wrt ADD) by
A177,
FINSOP_1:def 1;
then (ADD
"**" NoNoiS2)
is_a_unity_wrt ADD by
A178,
BINOP_1:def 8;
then
A181: (AS1
. pq1)
= (AS2
. pq1) by
A115,
A174,
A173,
A175,
A176,
A172;
(SumFdist
. pq1)
= AS1 by
A63;
hence thesis by
A63,
A181;
end;
A182: (ANoNoiS2
. (p1,q1))
>=
0
proof
set N = NoNoiS2;
per cases ;
suppose
A183: (
len N)
=
0 ;
A184: ADD is
having_a_unity by
A64,
NAGATA_1: 23;
then
A185: ex f be
Element of Fun st f
is_a_unity_wrt ADD by
SETWISEO:def 2;
(ADD
"**" N)
= (
the_unity_wrt ADD) by
A183,
A184,
FINSOP_1:def 1;
then (ADD
"**" N)
is_a_unity_wrt ADD by
A185,
BINOP_1:def 8;
hence thesis by
A115,
A117;
end;
suppose
A186: (
len N)
<>
0 ;
then (
len N)
>= 1 by
NAT_1: 14;
then
consider F be
sequence of Fun such that
A187: (F
. 1)
= (N
. 1) and
A188: for n be
Nat st
0
<> n & n
< (
len N) holds (F
. (n
+ 1))
= (ADD
. ((F
. n),(N
. (n
+ 1)))) and
A189: (ADD
"**" N)
= (F
. (
len N)) by
FINSOP_1:def 1;
defpred
R[
Nat] means $1
<>
0 & $1
<= (
len N) implies for Fn be
RealMap of
[:T, T:] st Fn
= (F
. $1) holds (Fn
. (p1,q1))
>=
0 ;
A190: for k holds
R[k] implies
R[(k
+ 1)]
proof
let k;
assume
A191:
R[k];
assume that (k
+ 1)
<>
0 and
A192: (k
+ 1)
<= (
len N);
A193: k
< (
len N) by
A192,
NAT_1: 13;
(k
+ 1)
>= 1 by
NAT_1: 14;
then (k
+ 1)
in (
dom N) by
A192,
FINSEQ_3: 25;
then (N
. (k
+ 1))
in ((
rng No)
\ (
rng NoiS2)) by
A168,
FUNCT_1:def 3;
then (N
. (k
+ 1))
in
RNG(No0) by
A157,
XBOOLE_0:def 5;
then
consider fd be
RealMap of T such that
A194: (Fdist
. fd)
= (N
. (k
+ 1)) and fd
in
No0(p1,q1);
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then
reconsider Fdistfd = (Fdist
. fd), Fk1 = (F
. (k
+ 1)), Fk = (F
. k), Nk1 = (N
. (k
+ 1)) as
RealMap of
[:T, T:] by
A194,
FUNCT_2: 5,
FUNCT_2: 66;
A195:
|.((fd
. p1)
- (fd
. q1)).|
>=
0 by
COMPLEX1: 46;
A196: fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then
A197: (Fdistfd
. (p1,q1))
=
|.((fd
. p1)
- (fd
. q1)).| by
A46;
A198:
now
per cases ;
suppose k
=
0 ;
hence (Fk1
. (p1,q1))
>=
0 by
A46,
A187,
A194,
A196,
A195;
end;
suppose
A199: k
>
0 ;
Fk1
= (ADD
. (Fk,Nk1)) by
A188,
A193,
A199;
then
A200: Fk1
= (Fk
+ Nk1) by
A64;
(Fk
. (p1,q1))
>=
0 by
A191,
A192,
A199,
NAT_1: 13;
then (
0
+
0 )
<= ((Fk
. (p1,q1))
+ (Nk1
. (p1,q1))) by
A194,
A195,
A197;
hence (Fk1
. (p1,q1))
>=
0 by
A117,
A200,
NAGATA_1:def 7;
end;
end;
let Fn be
RealMap of
[:T, T:];
assume Fn
= (F
. (k
+ 1));
hence thesis by
A198;
end;
A201:
R[
0 ];
for n holds
R[n] from
NAT_1:sch 2(
A201,
A190);
hence thesis by
A186,
A189;
end;
end;
now
A202: (AS2
. (p1,q1))
<= (AS1
. (p1,q1)) by
A117,
A182,
A174,
A173,
A175,
A176,
A172,
XREAL_1: 7;
let SumFdist1,SumFdist2 be
RealMap of
[:T, T:];
assume that
A203: SumFdist1
= (SumFdist
. pq1) and
A204: SumFdist2
= (SumFdist
. pq2);
SumFdist2
= AS2 by
A63,
A204;
hence (SumFdist1
. pq1)
>= (SumFdist2
. pq1) by
A63,
A117,
A203,
A202;
end;
hence thesis;
end;
now
let p,q,r be
Point of T;
thus (SumFTS
. (p,p))
=
0
proof
reconsider pp =
[p, p] as
Point of
[:T, T:] by
BORSUK_1:def 2;
reconsider SF = (SFdist
. pp) as
FinSequence of Fun by
FINSEQ_1:def 11;
A205:
now
per cases ;
suppose
A206: (
len SF)
=
0 ;
A207: ADD is
having_a_unity by
A64,
NAGATA_1: 23;
then
A208: ex f be
Element of Fun st f
is_a_unity_wrt ADD by
SETWISEO:def 2;
(ADD
"**" SF)
= (
the_unity_wrt ADD) by
A206,
A207,
FINSOP_1:def 1;
then (ADD
"**" SF)
is_a_unity_wrt ADD by
A208,
BINOP_1:def 8;
hence ((ADD
"**" SF)
. pp)
=
0 by
A115;
end;
suppose
A209: (
len SF)
<>
0 ;
then (
len SF)
>= 1 by
NAT_1: 14;
then
consider F be
sequence of Fun such that
A210: (F
. 1)
= (SF
. 1) and
A211: for n be
Nat st
0
<> n & n
< (
len SF) holds (F
. (n
+ 1))
= (ADD
. ((F
. n),(SF
. (n
+ 1)))) and
A212: (ADD
"**" SF)
= (F
. (
len SF)) by
FINSOP_1:def 1;
defpred
R[
Nat] means $1
<>
0 & $1
<= (
len SF) implies ((F
. $1)
. pp)
=
0 ;
A213: for k holds
R[k] implies
R[(k
+ 1)]
proof
let k;
assume
A214:
R[k];
consider x,y be
Point of T such that
[x, y]
= pp and
A215: (
rng SF)
=
RNG(\/) by
A61;
assume that (k
+ 1)
<>
0 and
A216: (k
+ 1)
<= (
len SF);
A217: k
< (
len SF) by
A216,
NAT_1: 13;
(k
+ 1)
>= 1 by
NAT_1: 14;
then (k
+ 1)
in (
dom SF) by
A216,
FINSEQ_3: 25;
then (SF
. (k
+ 1))
in
RNG(\/) by
A215,
FUNCT_1:def 3;
then
consider fd be
RealMap of T such that
A218: (Fdist
. fd)
= (SF
. (k
+ 1)) and fd
in (
Fx(x)
\/
Fx(y));
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then
reconsider Fdistfd = (Fdist
. fd), Fk1 = (F
. (k
+ 1)), Fk = (F
. k), SFk1 = (SF
. (k
+ 1)) as
RealMap of
[:T, T:] by
A218,
FUNCT_2: 5,
FUNCT_2: 66;
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then
A219: (Fdistfd
. (p,p))
=
|.((fd
. p)
- (fd
. p)).| by
A46;
per cases ;
suppose k
=
0 ;
hence thesis by
A210,
A218,
A219,
ABSVALUE: 2;
end;
suppose
A220: k
>
0 ;
Fk1
= (ADD
. (Fk,SFk1)) by
A211,
A217,
A220;
then Fk1
= (Fk
+ SFk1) by
A64;
then (Fk1
. pp)
= (
0
+ (SFk1
. pp)) by
A214,
A216,
A220,
NAGATA_1:def 7,
NAT_1: 13;
hence thesis by
A218,
A219,
ABSVALUE: 2;
end;
end;
A221:
R[
0 ];
for n holds
R[n] from
NAT_1:sch 2(
A221,
A213);
hence ((ADD
"**" SF)
. pp)
=
0 by
A209,
A212;
end;
end;
(SumFdist
. pp)
= (ADD
"**" SF) by
A63;
hence thesis by
A205,
NAGATA_1:def 8;
end;
thus (SumFTS
. (p,r))
<= ((SumFTS
. (p,q))
+ (SumFTS
. (r,q)))
proof
reconsider pr =
[p, r], pq =
[p, q], rq =
[r, q] as
Point of
[:T, T:] by
BORSUK_1:def 2;
reconsider SFpr = (SFdist
. pr) as
FinSequence of Fun by
FINSEQ_1:def 11;
reconsider ASFpr = (ADD
"**" SFpr) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
reconsider SumFpr = (SumFdist
. pr), SumFpq = (SumFdist
. pq), SumFrq = (SumFdist
. rq) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
A222: (SumFTS
. pr)
= (SumFpr
. pr) & (SumFTS
. pq)
= (SumFpq
. pq) by
NAGATA_1:def 8;
(SumFpr
. pq)
<= (SumFpq
. pq) & (SumFpr
. rq)
<= (SumFrq
. rq) by
A116;
then
A223: ((SumFpr
. pq)
+ (SumFpr
. rq))
<= ((SumFpq
. pq)
+ (SumFrq
. rq)) by
XREAL_1: 7;
A224:
now
per cases ;
suppose
A225: (
len SFpr)
=
0 ;
A226: ADD is
having_a_unity by
A64,
NAGATA_1: 23;
then
A227: ex f be
Element of Fun st f
is_a_unity_wrt ADD by
SETWISEO:def 2;
(ADD
"**" SFpr)
= (
the_unity_wrt ADD) by
A225,
A226,
FINSOP_1:def 1;
then
A228: (ADD
"**" SFpr)
is_a_unity_wrt ADD by
A227,
BINOP_1:def 8;
then (ASFpr
. pr)
=
0 & (ASFpr
. pq)
=
0 by
A115;
hence (ASFpr
. pr)
<= ((ASFpr
. pq)
+ (ASFpr
. rq)) by
A115,
A228;
end;
suppose
A229: (
len SFpr)
<>
0 ;
then (
len SFpr)
>= 1 by
NAT_1: 14;
then
consider F be
sequence of Fun such that
A230: (F
. 1)
= (SFpr
. 1) and
A231: for n be
Nat st
0
<> n & n
< (
len SFpr) holds (F
. (n
+ 1))
= (ADD
. ((F
. n),(SFpr
. (n
+ 1)))) and
A232: (ADD
"**" SFpr)
= (F
. (
len SFpr)) by
FINSOP_1:def 1;
defpred
T[
Nat] means $1
<>
0 & $1
<= (
len SFpr) implies for F9 be
RealMap of
[:T, T:] st F9
= (F
. $1) holds (F9
. pr)
<= ((F9
. pq)
+ (F9
. rq));
A233: for k holds
T[k] implies
T[(k
+ 1)]
proof
let k;
assume
A234:
T[k];
consider x,y be
Point of T such that
[x, y]
= pr and
A235: (
rng SFpr)
=
RNG(\/) by
A61;
assume that (k
+ 1)
<>
0 and
A236: (k
+ 1)
<= (
len SFpr);
A237: k
< (
len SFpr) by
A236,
NAT_1: 13;
(k
+ 1)
>= 1 by
NAT_1: 14;
then (k
+ 1)
in (
dom SFpr) by
A236,
FINSEQ_3: 25;
then (SFpr
. (k
+ 1))
in
RNG(\/) by
A235,
FUNCT_1:def 3;
then
consider fd be
RealMap of T such that
A238: (Fdist
. fd)
= (SFpr
. (k
+ 1)) and fd
in (
Fx(x)
\/
Fx(y));
fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then
reconsider Fdistfd = (Fdist
. fd), Fk1 = (F
. (k
+ 1)), Fk = (F
. k), SFk1 = (SFpr
. (k
+ 1)) as
RealMap of
[:T, T:] by
A238,
FUNCT_2: 5,
FUNCT_2: 66;
A239: ((fd
. p)
- (fd
. r))
= (((fd
. p)
- (fd
. q))
+ ((fd
. q)
- (fd
. r)));
then
A240:
|.((fd
. p)
- (fd
. r)).|
<= (
|.((fd
. p)
- (fd
. q)).|
+
|.((fd
. q)
- (fd
. r)).|) by
COMPLEX1: 56;
A241: fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
then
A242: (Fdistfd
. (p,r))
=
|.((fd
. p)
- (fd
. r)).| & (Fdistfd
. (p,q))
=
|.((fd
. p)
- (fd
. q)).| by
A46;
A243:
|.((fd
. q)
- (fd
. r)).|
=
|.(
- ((fd
. q)
- (fd
. r))).| & (Fdistfd
. (r,q))
=
|.((fd
. r)
- (fd
. q)).| by
A46,
A241,
COMPLEX1: 52;
let F9 be
RealMap of
[:T, T:] such that
A244: F9
= (F
. (k
+ 1));
per cases ;
suppose k
=
0 ;
hence thesis by
A230,
A238,
A239,
A242,
A243,
A244,
COMPLEX1: 56;
end;
suppose
A245: k
>
0 ;
then (Fk
. pr)
<= ((Fk
. pq)
+ (Fk
. rq)) by
A234,
A236,
NAT_1: 13;
then
A246: ((Fk
. pr)
+ (SFk1
. pr))
<= (((Fk
. pq)
+ (Fk
. rq))
+ ((SFk1
. pq)
+ (SFk1
. rq))) by
A238,
A240,
A242,
A243,
XREAL_1: 7;
Fk1
= (ADD
. (Fk,SFk1)) by
A231,
A237,
A245;
then
A247: Fk1
= (Fk
+ SFk1) by
A64;
then (Fk1
. pq)
= ((Fk
. pq)
+ (SFk1
. pq)) & (Fk1
. rq)
= ((Fk
. rq)
+ (SFk1
. rq)) by
NAGATA_1:def 7;
hence thesis by
A244,
A247,
A246,
NAGATA_1:def 7;
end;
end;
A248:
T[
0 ];
for n holds
T[n] from
NAT_1:sch 2(
A248,
A233);
hence (ASFpr
. pr)
<= ((ASFpr
. pq)
+ (ASFpr
. rq)) by
A229,
A232;
end;
end;
SumFpr
= (ADD
"**" SFpr) by
A63;
then (SumFpr
. pr)
<= ((SumFpq
. pq)
+ (SumFrq
. rq)) by
A224,
A223,
XXREAL_0: 2;
hence thesis by
A222,
NAGATA_1:def 8;
end;
end;
then
A249: SumFTS
is_a_pseudometric_of cT by
NAGATA_1: 28;
A250: for p be
Point of T, fd be
Element of (
Funcs (cT,
REAL )) st fd
in
Fx(p) holds
funcdist[fd, (Fdist
. fd)] & (Fdist
. fd) is
continuous
RealMap of
[:T, T:]
proof
let p be
Point of T, fd be
Element of (
Funcs (cT,
REAL ));
reconsider FD = (Fdist
. fd) as
RealMap of
[:T, T:] by
FUNCT_2: 66;
assume fd
in
Fx(p);
then
consider A be
Subset of T such that
A251: fd
= (Fn
. A) and
A252: A
in (Bn
. n) and A
in
s(.);
A253:
funcdist[fd, (Fdist
. fd)] by
A46;
F[A, (Fn
. A)] by
A26,
A252;
then FD is
continuous by
A251,
A253,
NAGATA_1: 21;
hence thesis by
A46;
end;
A254: for pq9 holds (SumFdist
. pq9) is
continuous
RealMap of
[:T, T:]
proof
let pq9;
reconsider SF = (SFdist
. pq9) as
FinSequence of Fun by
FINSEQ_1:def 11;
consider p, q such that
[p, q]
= pq9 and
A255: (
rng SF)
=
RNG(\/) by
A61;
for n be
Element of
NAT st
0
<> n & n
<= (
len SF) holds (SF
. n) is
continuous
RealMap of
[:T, T:]
proof
let n be
Element of
NAT ;
assume that
A256:
0
<> n and
A257: n
<= (
len SF);
n
>= 1 by
A256,
NAT_1: 14;
then n
in (
dom SF) by
A257,
FINSEQ_3: 25;
then (SF
. n)
in
RNG(\/) by
A255,
FUNCT_1:def 3;
then
consider fd be
RealMap of T such that
A258: (SF
. n)
= (Fdist
. fd) and
A259: fd
in (
Fx(p)
\/
Fx(q));
A260: fd
in (
Funcs (cT,
REAL )) by
FUNCT_2: 8;
fd
in
Fx(p) or fd
in
Fx(q) by
A259,
XBOOLE_0:def 3;
hence thesis by
A250,
A258,
A260;
end;
then (ADD
"**" SF) is
continuous
RealMap of
[:T, T:] by
A64,
NAGATA_1: 25;
hence thesis by
A63;
end;
A261: for pq9 holds (SumFdist9
. pq9) is
continuous
Function of
[:T, T:],
R^1
proof
let pq9;
reconsider SF = (SumFdist
. pq9) as
Function of
[:T, T:],
R^1 by
A254,
TOPMETR: 17;
(SumFdist
. pq9) is
continuous
RealMap of
[:T, T:] by
A254;
then SF is
continuous by
JORDAN5A: 27;
hence thesis;
end;
take (
min (jj,SumFTS9));
A262: for p, q holds ((
min (jj,SumFTS9))
.
[p, q])
<= 1
proof
let p, q;
cTT
=
[:cT, cT:] by
BORSUK_1:def 2;
then ((
min (jj,SumFTS9))
.
[p, q])
= (
min (1,(SumFTS9
.
[p, q]))) by
NAGATA_1:def 9;
hence thesis by
XXREAL_0: 17;
end;
for p,q be
Point of
[:T, T:] st p
in (SS
. q) holds ((SumFdist9
. p)
. p)
= ((SumFdist9
. q)
. p) by
A116;
then (SumFdist9
Toler ) is
continuous by
A261,
A35,
NAGATA_1: 26;
then SumFTS9 is
continuous by
JORDAN5A: 27;
then (
min (jj,SumFTS9))
= (
min (jj,SumFTS)) & (
min (jj,SumFTS9)) is
continuous by
BORSUK_1:def 2,
NAGATA_1: 27;
hence thesis by
A249,
A262,
A113,
NAGATA_1: 30;
end;
A263: for k be
object st k
in
NAT holds ex f be
object st f
in (
Funcs (cTT,
REAL )) &
N[k, f]
proof
A264:
NAT
= (
rng
PairFunc ) by
Th2,
FUNCT_2:def 3;
let k be
object;
assume k
in
NAT ;
then
consider nm be
object such that
A265: nm
in (
dom
PairFunc ) and
A266: k
= (
PairFunc
. nm) by
A264,
FUNCT_1:def 3;
consider n,m be
object such that
A267: n
in
NAT & m
in
NAT and
A268: nm
=
[n, m] by
A265,
ZFMISC_1:def 2;
consider pmet9 such that
A269:
NN[n, m, pmet9] by
A7,
A267;
take pmet9;
thus pmet9
in (
Funcs (cTT,
REAL )) by
FUNCT_2: 8;
take pm = pmet9;
thus pm
= pmet9;
let n1,m1 be
Nat;
assume ((
PairFunc
" )
. k)
=
[n1, m1];
then
[n1, m1]
=
[n, m] by
A265,
A266,
A268,
Lm2,
Th2,
FUNCT_1: 32;
then n1
= n & m1
= m by
XTUPLE_0: 1;
hence thesis by
A269;
end;
consider F be
sequence of (
Funcs (cTT,
REAL )) such that
A270: for n be
object st n
in
NAT holds
N[n, (F
. n)] from
FUNCT_2:sch 1(
A263);
A271:
now
let n be
Nat;
[:cT, cT:]
= cTT by
BORSUK_1:def 2;
hence (F
. n) is
PartFunc of
[:cT, cT:],
REAL by
FUNCT_2: 66;
end;
(
dom F)
=
NAT by
FUNCT_2:def 1;
then
reconsider F9 = F as
Functional_Sequence of
[:cT, cT:],
REAL by
A271,
SEQFUNC: 1;
A272: for p, A9 st not p
in A9 & A9 is
closed holds ex k st for pmet st (F9
. k)
= pmet holds ((
lower_bound (pmet,A9))
. p)
>
0
proof
let p, A9 such that
A273: not p
in A9 and
A274: A9 is
closed;
set O = (A9
` );
p
in O by
A273,
XBOOLE_0:def 5;
then
consider U be
Subset of T such that
A275: p
in U and
A276: (
Cl U)
c= O and
A277: U
in (
Union Bn) by
A1,
A5,
A274,
NAGATA_1: 19;
(
Union Bn)
c= the
topology of T by
A5,
TOPS_2: 64;
then
reconsider U as
open
Subset of T by
A277,
PRE_TOPC:def 2;
consider n such that
A278: U
in (Bn
. n) by
A277,
PROB_1: 12;
consider W be
Subset of T such that
A279: p
in W & (
Cl W)
c= U and
A280: W
in (
Union Bn) by
A1,
A5,
A275,
NAGATA_1: 19;
(
Union Bn)
c= the
topology of T by
A5,
TOPS_2: 64;
then
reconsider W as
open
Subset of T by
A280,
PRE_TOPC:def 2;
consider m such that
A281: W
in (Bn
. m) by
A280,
PROB_1: 12;
set k = (
PairFunc
.
[n, m]);
A282: k
in
NAT by
ORDINAL1:def 12;
A283: n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
consider G be
RealMap of
[:T, T:] such that
A284: G
= (F
. k) and
A285: for n,m be
Nat st ((
PairFunc
" )
. k)
=
[n, m] holds
NN[n, m, G] by
A270,
A282;
A286:
[n, m]
in
[:
NAT ,
NAT :] by
A283,
ZFMISC_1: 87;
reconsider kk = k as
Element of
NAT by
ORDINAL1:def 12;
(
dom
PairFunc )
=
[:
NAT ,
NAT :] by
FUNCT_2:def 1;
then
[n, m]
= ((
PairFunc
" )
. kk) by
Lm2,
Th2,
FUNCT_1: 32,
A286;
then
consider pmet such that
A287: G
= pmet and G is
continuous and pmet
is_a_pseudometric_of cT and
A288: for p, q holds (pmet
.
[p, q])
<= 1 & for p, q st ex A, B st A is
open & B is
open & A
in (Bn
. m) & B
in (Bn
. n) & p
in A & (
Cl A)
c= B & not q
in B holds (pmet
.
[p, q])
= 1 by
A285;
A289: for rn st rn
in ((
dist (pmet,p))
.: A9) holds rn
>= 1
proof
let rn;
assume rn
in ((
dist (pmet,p))
.: A9);
then
consider a be
object such that
A290: a
in (
dom (
dist (pmet,p))) and
A291: a
in A9 and
A292: rn
= ((
dist (pmet,p))
. a) by
FUNCT_1:def 6;
reconsider a as
Point of T by
A290;
A293: (pmet
. (p,a))
= ((
dist (pmet,p))
. a) by
Def2;
U
c= (
Cl U) by
PRE_TOPC: 18;
then U
c= O by
A276;
then U
misses A9 by
SUBSET_1: 23;
then not a
in U by
A291,
XBOOLE_0: 3;
hence thesis by
A279,
A278,
A281,
A288,
A292,
A293;
end;
take k;
cT
= (
dom (
dist (pmet,p))) by
FUNCT_2:def 1;
then (
lower_bound ((
dist (pmet,p))
.: A9))
>= 1 by
A289,
SEQ_4: 43;
hence thesis by
A284,
A287,
Def3;
end;
for k holds ex pmet st (F9
. k)
= pmet & pmet
is_a_pseudometric_of cT & (for pq holds (pmet
. pq)
<= 1) & for pmet9 st pmet
= pmet9 holds pmet9 is
continuous
proof
let k;
A294: k
in
NAT by
ORDINAL1:def 12;
then
consider Fk be
RealMap of
[:T, T:] such that
A295: Fk
= (F
. k) and
A296: for n, m st ((
PairFunc
" )
. k)
=
[n, m] holds
NN[n, m, Fk] by
A270;
NAT
= (
rng
PairFunc ) by
Th2,
FUNCT_2:def 3;
then
consider nm be
object such that
A297: nm
in (
dom
PairFunc ) and
A298: k
= (
PairFunc
. nm) by
FUNCT_1:def 3,
A294;
consider n,m be
object such that
A299: n
in
NAT & m
in
NAT and
A300: nm
=
[n, m] by
A297,
ZFMISC_1:def 2;
[n, m]
= ((
PairFunc
" )
. k) by
A297,
A298,
A300,
Lm2,
Th2,
FUNCT_1: 32;
then
consider pmet such that
A301: Fk
= pmet and
A302: Fk is
continuous and
A303: pmet
is_a_pseudometric_of cT and
A304: for p, q holds (pmet
.
[p, q])
<= 1 & for p, q st ex A, B st A is
open & B is
open & A
in (Bn
. m) & B
in (Bn
. n) & p
in A & (
Cl A)
c= B & not q
in B holds (pmet
.
[p, q])
= 1 by
A299,
A296;
take pmet;
thus (F9
. k)
= pmet & pmet
is_a_pseudometric_of cT by
A295,
A301,
A303;
thus for pq holds (pmet
. pq)
<= 1
proof
let pq;
ex p,q be
object st p
in cT & q
in cT & pq
=
[p, q] by
ZFMISC_1:def 2;
hence thesis by
A304;
end;
thus thesis by
A301,
A302;
end;
hence thesis by
A2,
A272,
Th17;
end;
thus thesis by
NAGATA_1: 15,
NAGATA_1: 16;
end;
theorem ::
NAGATA_2:20
Th20: T is
metrizable implies for FX be
Subset-Family of T st FX is
Cover of T & FX is
open holds ex Un be
FamilySequence of T st (
Union Un) is
open & (
Union Un) is
Cover of T & (
Union Un)
is_finer_than FX & Un is
sigma_discrete
proof
set cT = the
carrier of T;
assume T is
metrizable;
then
consider metr be
Function of
[:cT, cT:],
REAL such that
A1: metr
is_metric_of cT and
A2: (
Family_open_set (
SpaceMetr (cT,metr)))
= the
topology of T by
PCOMPS_1:def 8;
reconsider PM = (
SpaceMetr (cT,metr)) as non
empty
MetrSpace by
A1,
PCOMPS_1: 36;
set cPM = the
carrier of PM;
let FX be
Subset-Family of T such that
A3: FX is
Cover of T and
A4: FX is
open;
defpred
P1[
set] means $1
in FX;
deffunc
F1(
Point of PM,
Nat) = (
Ball ($1,(1
/ (2
|^ ($2
+ 1)))));
consider R be
Relation such that
A5: R
well_orders FX by
WELLORD2: 17;
consider Mn be
Relation such that
A6: Mn
= (R
|_2 FX);
set UB = { (
union { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V }) where V be
Subset of PM : V
in FX };
UB
c= (
bool the
carrier of PM)
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in UB;
then
consider V be
Subset of PM such that
A7: x
= (
union { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V }) and V
in FX;
xx
c= cPM
proof
let y be
object;
assume y
in xx;
then
consider W be
set such that
A8: y
in W and
A9: W
in { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V } by
A7,
TARSKI:def 4;
ex c be
Point of PM st W
= (
Ball (c,(1
/ 2))) & c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V by
A9;
hence thesis by
A8;
end;
hence thesis;
end;
then
reconsider UB as
Subset-Family of PM;
defpred
Q1[
Point of PM,
Subset of PM,
Nat] means $1
in ($2
\ (
PartUnion ($2,Mn))) & (
Ball ($1,(3
/ (2
|^ ($3
+ 1)))))
c= $2;
consider Un be
sequence of (
bool (
bool cPM)) such that
A10: (Un
.
0 )
= UB & for n be
Nat holds (Un
. (n
+ 1))
= { (
union {
F1(c,n) where c be
Point of PM :
Q1[c, V, n] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= n }) }) where V be
Subset of PM :
P1[V] } from
PCOMPS_2:sch 3;
reconsider Un9 = Un as
FamilySequence of T by
A1,
PCOMPS_2: 4;
take Un9;
thus (
Union Un9) is
open
proof
let A;
assume A
in (
Union Un9);
then
consider n such that
A11: A
in (Un
. n) by
PROB_1: 12;
per cases ;
suppose n
=
0 ;
then
consider V be
Subset of PM such that
A12: A
= (
union { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V }) and V
in FX by
A10,
A11;
set BALL = { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V };
BALL
c= (
bool the
carrier of PM)
proof
let x be
object;
assume x
in BALL;
then ex c be
Point of PM st x
= (
Ball (c,(1
/ 2))) & c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V;
hence thesis;
end;
then
reconsider BALL as
Subset-Family of PM;
BALL
c= (
Family_open_set PM)
proof
let x be
object;
assume x
in BALL;
then ex c be
Point of PM st x
= (
Ball (c,(1
/ 2))) & c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V;
hence thesis by
PCOMPS_1: 29;
end;
then A
in the
topology of T by
A2,
A12,
PCOMPS_1: 32;
hence thesis by
PRE_TOPC:def 2;
end;
suppose n
>
0 ;
then
consider m be
Nat such that
A13: n
= (m
+ 1) by
NAT_1: 6;
reconsider m as
Element of
NAT by
ORDINAL1:def 12;
A
in { (
union {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) }) where V be
Subset of PM :
P1[V] } by
A10,
A11,
A13;
then
consider V be
Subset of PM such that
A14: A
= (
union {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) }) &
P1[V];
set BALL = {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) };
BALL
c= (
bool the
carrier of PM)
proof
let x be
object;
assume x
in BALL;
then ex c be
Point of PM st x
=
F1(c,m) &
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m });
hence thesis;
end;
then
reconsider BALL as
Subset-Family of PM;
BALL
c= (
Family_open_set PM)
proof
let x be
object;
assume x
in BALL;
then ex c be
Point of PM st x
=
F1(c,m) &
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m });
hence thesis by
PCOMPS_1: 29;
end;
then A
in the
topology of T by
A2,
A14,
PCOMPS_1: 32;
hence thesis by
PRE_TOPC:def 2;
end;
end;
A15: Mn
well_orders FX by
A5,
A6,
PCOMPS_2: 1;
(
[#] T)
c= (
union (
Union Un9))
proof
let x be
object such that
A16: x
in (
[#] T);
reconsider x9 = x as
Element of PM by
A1,
A16,
PCOMPS_2: 4;
defpred
P2[
set] means x
in $1;
ex G be
Subset of T st x
in G & G
in FX by
A3,
A16,
PCOMPS_1: 3;
then
A17: ex G be
set st G
in FX &
P2[G];
consider X such that
A18: X
in FX &
P2[X] & for Y be
set st Y
in FX &
P2[Y] holds
[X, Y]
in Mn from
PCOMPS_2:sch 1(
A15,
A17);
assume
A19: not x
in (
union (
Union Un9));
A20: for V be
set, n be
Nat st V
in (Un9
. n) holds not x
in V
proof
let V be
set, n be
Nat;
assume V
in (Un9
. n);
then V
in (
Union Un) by
PROB_1: 12;
hence thesis by
A19,
TARSKI:def 4;
end;
A21: for n holds not x
in (
union (Un9
. n))
proof
let n;
assume x
in (
union (Un9
. n));
then ex V be
set st x
in V & V
in (Un9
. n) by
TARSKI:def 4;
hence contradiction by
A20;
end;
reconsider X as
Subset of T by
A18;
X is
open by
A4,
A18;
then
A22: X
in (
Family_open_set PM) by
A2,
PRE_TOPC:def 2;
reconsider X as
Subset of PM by
A1,
PCOMPS_2: 4;
consider r such that
A23: r
>
0 and
A24: (
Ball (x9,r))
c= X by
A18,
A22,
PCOMPS_1:def 4;
defpred
P3[
Nat] means (3
/ (2
|^ $1))
<= r;
ex k st
P3[k] by
A23,
PREPOWER: 92;
then
A25: ex k be
Nat st
P3[k];
consider k be
Nat such that
A26:
P3[k] & for i be
Nat st
P3[i] holds k
<= i from
NAT_1:sch 5(
A25);
set W = (
union {
F1(y,k) where y be
Point of PM :
Q1[y, X, k] & not y
in (
union { (
union (Un
. i)) where i be
Nat : i
<= k }) });
(2
|^ (k
+ 1))
= ((2
|^ k)
* 2) by
NEWTON: 6;
then (2
|^ k)
>
0 & (2
|^ (k
+ 1))
>= (2
|^ k) by
PREPOWER: 6,
XREAL_1: 151;
then (3
/ (2
|^ (k
+ 1)))
<= (3
/ (2
|^ k)) by
XREAL_1: 118;
then
A27: (3
/ (2
|^ (k
+ 1)))
<= r by
A26,
XXREAL_0: 2;
A28: x
in W
proof
not x9
in (
PartUnion (X,Mn))
proof
assume x9
in (
PartUnion (X,Mn));
then x9
in (
union (Mn
-Seg X)) by
PCOMPS_2:def 1;
then
consider M be
set such that
A29: x9
in M and
A30: M
in (Mn
-Seg X) by
TARSKI:def 4;
A31: M
<> X by
A30,
WELLORD1: 1;
A32: Mn
is_antisymmetric_in FX by
A15,
WELLORD1:def 5;
A33:
[M, X]
in Mn by
A30,
WELLORD1: 1;
then M
in (
field Mn) by
RELAT_1: 15;
then
A34: M
in FX by
A5,
A6,
PCOMPS_2: 1;
then
[X, M]
in Mn by
A18,
A29;
hence contradiction by
A18,
A31,
A33,
A34,
A32,
RELAT_2:def 4;
end;
then
A35: x9
in (X
\ (
PartUnion (X,Mn))) by
A18,
XBOOLE_0:def 5;
set A = (
Ball (x9,(1
/ (2
|^ (k
+ 1)))));
0
< (2
|^ (k
+ 1)) by
PREPOWER: 6;
then
A36: x9
in A by
TBSP_1: 11,
XREAL_1: 139;
A37: not x9
in (
union { (
union (Un9
. i)) where i be
Nat : i
<= k })
proof
assume x9
in (
union { (
union (Un9
. i)) where i be
Nat : i
<= k });
then
consider D be
set such that
A38: x9
in D & D
in { (
union (Un9
. i)) where i be
Nat : i
<= k } by
TARSKI:def 4;
ex i be
Nat st D
= (
union (Un9
. i)) & i
<= k by
A38;
hence contradiction by
A21,
A38;
end;
(
Ball (x9,(3
/ (2
|^ (k
+ 1)))))
c= (
Ball (x9,r)) by
A27,
PCOMPS_1: 1;
then (
Ball (x9,(3
/ (2
|^ (k
+ 1)))))
c= X by
A24;
then A
in {
F1(y,k) where y be
Point of PM :
Q1[y, X, k] & not y
in (
union { (
union (Un9
. i)) where i be
Nat : i
<= k }) } by
A35,
A37;
hence thesis by
A36,
TARSKI:def 4;
end;
k
in
NAT & W
in { (
union {
F1(y,k) where y be
Point of PM :
Q1[y, V, k] & not y
in (
union { (
union (Un
. q)) where q be
Nat : q
<= k }) }) where V be
Subset of PM : V
in FX } by
A18,
ORDINAL1:def 12;
then W
in (Un9
. (k
+ 1)) by
A10;
hence thesis by
A20,
A28;
end;
then (
[#] T)
= (
union (
Union Un9));
hence (
Union Un9) is
Cover of T by
SETFAM_1: 45;
for X be
set st X
in (
Union Un9) holds ex Y be
set st Y
in FX & X
c= Y
proof
let X be
set;
assume X
in (
Union Un9);
then
consider n such that
A39: X
in (Un
. n) by
PROB_1: 12;
per cases ;
suppose n
=
0 ;
then
consider V be
Subset of PM such that
A40: X
= (
union { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V }) and
A41: V
in FX by
A10,
A39;
set BALL = { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V };
BALL
c= (
bool the
carrier of PM)
proof
let x be
object;
assume x
in BALL;
then ex c be
Point of PM st x
= (
Ball (c,(1
/ 2))) & c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V;
hence thesis;
end;
then
reconsider BALL as
Subset-Family of PM;
for W be
set st W
in BALL holds W
c= V
proof
let W be
set;
assume W
in BALL;
then
consider c be
Element of PM such that
A42: W
= (
Ball (c,(1
/ 2))) and c
in (V
\ (
PartUnion (V,Mn))) and
A43: (
Ball (c,(3
/ 2)))
c= V;
(
Ball (c,(1
/ 2)))
c= (
Ball (c,(3
/ 2))) by
PCOMPS_1: 1;
hence thesis by
A42,
A43;
end;
then X
c= V by
A40,
ZFMISC_1: 76;
hence thesis by
A41;
end;
suppose n
>
0 ;
then
consider m be
Nat such that
A44: n
= (m
+ 1) by
NAT_1: 6;
reconsider m as
Element of
NAT by
ORDINAL1:def 12;
X
in { (
union {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) }) where V be
Subset of PM :
P1[V] } by
A10,
A39,
A44;
then
consider V be
Subset of PM such that
A45: X
= (
union {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) }) &
P1[V];
set BALL = {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) };
BALL
c= (
bool the
carrier of PM)
proof
let x be
object;
assume x
in BALL;
then ex c be
Point of PM st x
=
F1(c,m) &
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m });
hence thesis;
end;
then
reconsider BALL as
Subset-Family of PM;
for W be
set st W
in BALL holds W
c= V
proof
let W be
set;
assume W
in BALL;
then
consider c be
Element of PM such that
A46: W
=
F1(c,m) &
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m });
0
< (2
|^ (m
+ 1)) by
PREPOWER: 6;
then (1
/ (2
|^ (m
+ 1)))
< (3
/ (2
|^ (m
+ 1))) by
XREAL_1: 74;
then
F1(c,m)
c= (
Ball (c,(3
/ (2
|^ (m
+ 1))))) by
PCOMPS_1: 1;
hence thesis by
A46,
XBOOLE_1: 1;
end;
then X
c= V by
A45,
ZFMISC_1: 76;
hence thesis by
A45;
end;
end;
hence (
Union Un9)
is_finer_than FX by
SETFAM_1:def 2;
for n be
Element of
NAT holds (Un9
. n) is
discrete
proof
let n be
Element of
NAT ;
for p holds ex O be
open
Subset of T st p
in O & for A, B st A
in (Un9
. n) & B
in (Un9
. n) holds O
meets A & O
meets B implies A
= B
proof
let p;
reconsider p9 = p as
Point of PM by
A1,
PCOMPS_2: 4;
set O = (
Ball (p9,(1
/ (2
|^ (n
+ 2)))));
O
in (
Family_open_set PM) by
PCOMPS_1: 29;
then
reconsider O as
open
Subset of T by
A2,
PRE_TOPC:def 2;
take O;
A47:
now
let A, B such that
A48: A
in (Un9
. n) and
A49: B
in (Un9
. n);
assume that
A50: O
meets A and
A51: O
meets B;
consider a be
object such that
A52: a
in O and
A53: a
in A by
A50,
XBOOLE_0: 3;
consider b be
object such that
A54: b
in O and
A55: b
in B by
A51,
XBOOLE_0: 3;
reconsider a, b as
Point of PM by
A52,
A54;
A56: (
dist (p9,b))
< (1
/ (2
|^ (n
+ 2))) by
A54,
METRIC_1: 11;
A57: (
dist (a,b))
<= ((
dist (a,p9))
+ (
dist (p9,b))) & (2
|^ ((n
+ 1)
+ 1))
= ((2
|^ (n
+ 1))
* 2) by
METRIC_1: 4,
NEWTON: 6;
(
dist (p9,a))
< (1
/ (2
|^ (n
+ 2))) by
A52,
METRIC_1: 11;
then ((
dist (a,p9))
+ (
dist (p9,b)))
< ((1
/ (2
|^ (n
+ 2)))
+ (1
/ (2
|^ (n
+ 2)))) by
A56,
XREAL_1: 8;
then (
dist (a,b))
< (2
* (1
/ (2
* (2
|^ (n
+ 1))))) by
A57,
XXREAL_0: 2;
then (
dist (a,b))
< ((2
* 1)
/ (2
* (2
|^ (n
+ 1)))) by
XCMPLX_1: 74;
then
A58: (
dist (a,b))
< (((2
/ 2)
* 1)
/ (2
|^ (n
+ 1))) by
XCMPLX_1: 83;
now
per cases ;
suppose
A59: n
=
0 ;
then
A60: (
dist (a,b))
< (1
/ 2) by
A58;
consider V be
Subset of PM such that
A61: A
= (
union { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V }) and
A62: V
in FX by
A10,
A48,
A59;
consider Ba be
set such that
A63: a
in Ba and
A64: Ba
in { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (V
\ (
PartUnion (V,Mn))) & (
Ball (c,(3
/ 2)))
c= V } by
A53,
A61,
TARSKI:def 4;
consider ca be
Point of PM such that
A65: Ba
= (
Ball (ca,(1
/ 2))) and
A66: ca
in (V
\ (
PartUnion (V,Mn))) and
A67: (
Ball (ca,(3
/ 2)))
c= V by
A64;
(
dist (ca,a))
< (1
/ 2) by
A63,
A65,
METRIC_1: 11;
then
A68: ((
dist (ca,a))
+ (
dist (a,b)))
< ((1
/ 2)
+ (1
/ 2)) by
A60,
XREAL_1: 8;
(
dist (ca,b))
<= ((
dist (ca,a))
+ (
dist (a,b))) by
METRIC_1: 4;
then
A69: (
dist (ca,b))
< 1 by
A68,
XXREAL_0: 2;
consider W be
Subset of PM such that
A70: B
= (
union { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (W
\ (
PartUnion (W,Mn))) & (
Ball (c,(3
/ 2)))
c= W }) and
A71: W
in FX by
A10,
A49,
A59;
consider Bb be
set such that
A72: b
in Bb and
A73: Bb
in { (
Ball (c,(1
/ 2))) where c be
Point of PM : c
in (W
\ (
PartUnion (W,Mn))) & (
Ball (c,(3
/ 2)))
c= W } by
A55,
A70,
TARSKI:def 4;
consider cb be
Point of PM such that
A74: Bb
= (
Ball (cb,(1
/ 2))) and
A75: cb
in (W
\ (
PartUnion (W,Mn))) and
A76: (
Ball (cb,(3
/ 2)))
c= W by
A73;
A77: (
dist (ca,cb))
<= ((
dist (ca,b))
+ (
dist (b,cb))) by
METRIC_1: 4;
(
dist (cb,b))
< (1
/ 2) by
A72,
A74,
METRIC_1: 11;
then ((
dist (ca,b))
+ (
dist (b,cb)))
< (1
+ (1
/ 2)) by
A69,
XREAL_1: 8;
then (
dist (ca,cb))
< (3
/ 2) by
A77,
XXREAL_0: 2;
then
A78: ca
in (
Ball (cb,(3
/ 2))) & cb
in (
Ball (ca,(3
/ 2))) by
METRIC_1: 11;
V
= W
proof
assume
A79: V
<> W;
Mn
is_connected_in FX by
A15,
WELLORD1:def 5;
then
[V, W]
in Mn or
[W, V]
in Mn by
A62,
A71,
A79,
RELAT_2:def 6;
then V
in (Mn
-Seg W) or W
in (Mn
-Seg V) by
A79,
WELLORD1: 1;
then cb
in (
union (Mn
-Seg W)) or ca
in (
union (Mn
-Seg V)) by
A67,
A76,
A78,
TARSKI:def 4;
then cb
in (
PartUnion (W,Mn)) or ca
in (
PartUnion (V,Mn)) by
PCOMPS_2:def 1;
hence thesis by
A66,
A75,
XBOOLE_0:def 5;
end;
hence A
= B by
A61,
A70;
end;
suppose n
>
0 ;
then
consider m be
Nat such that
A80: n
= (m
+ 1) by
NAT_1: 6;
set r = (1
/ (2
|^ n));
A81: (3
* r)
= ((3
* 1)
/ (2
|^ n)) by
XCMPLX_1: 74;
(2
|^ (n
+ 1))
= ((2
|^ n)
* 2) by
NEWTON: 6;
then (2
|^ n)
>
0 & (2
|^ (n
+ 1))
>= (2
|^ n) by
PREPOWER: 6,
XREAL_1: 151;
then (1
/ (2
|^ (n
+ 1)))
<= r by
XREAL_1: 118;
then
A82: (
dist (a,b))
< r by
A58,
XXREAL_0: 2;
reconsider m as
Element of
NAT by
ORDINAL1:def 12;
A
in { (
union {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) }) where V be
Subset of PM :
P1[V] } by
A10,
A48,
A80;
then
consider V be
Subset of PM such that
A83: A
= (
union {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) }) &
P1[V];
consider Ba be
set such that
A84: a
in Ba & Ba
in {
F1(c,m) where c be
Point of PM :
Q1[c, V, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) } by
A53,
A83,
TARSKI:def 4;
consider ca be
Point of PM such that
A85: Ba
=
F1(ca,m) &
Q1[ca, V, m] & not ca
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) by
A84;
(
dist (ca,a))
< r by
A80,
A84,
A85,
METRIC_1: 11;
then
A86: ((
dist (ca,a))
+ (
dist (a,b)))
< (r
+ r) by
A82,
XREAL_1: 8;
(
dist (ca,b))
<= ((
dist (ca,a))
+ (
dist (a,b))) by
METRIC_1: 4;
then
A87: (
dist (ca,b))
< (r
+ r) by
A86,
XXREAL_0: 2;
B
in { (
union {
F1(c,m) where c be
Point of PM :
Q1[c, W, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) }) where W be
Subset of PM :
P1[W] } by
A10,
A49,
A80;
then
consider W be
Subset of PM such that
A88: B
= (
union {
F1(c,m) where c be
Point of PM :
Q1[c, W, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) }) &
P1[W];
consider Bb be
set such that
A89: b
in Bb & Bb
in {
F1(c,m) where c be
Point of PM :
Q1[c, W, m] & not c
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) } by
A55,
A88,
TARSKI:def 4;
consider cb be
Point of PM such that
A90: Bb
=
F1(cb,m) &
Q1[cb, W, m] & not cb
in (
union { (
union (Un
. k)) where k be
Nat : k
<= m }) by
A89;
A91: (
dist (ca,cb))
<= ((
dist (ca,b))
+ (
dist (b,cb))) by
METRIC_1: 4;
(
dist (cb,b))
< r by
A80,
A89,
A90,
METRIC_1: 11;
then ((
dist (ca,b))
+ (
dist (b,cb)))
< ((r
+ r)
+ r) by
A87,
XREAL_1: 8;
then (
dist (ca,cb))
< (3
* r) by
A91,
XXREAL_0: 2;
then
A92: ca
in (
Ball (cb,(3
/ (2
|^ (m
+ 1))))) & cb
in (
Ball (ca,(3
/ (2
|^ (m
+ 1))))) by
A80,
A81,
METRIC_1: 11;
V
= W
proof
assume
A93: V
<> W;
Mn
is_connected_in FX by
A15,
WELLORD1:def 5;
then
[V, W]
in Mn or
[W, V]
in Mn by
A83,
A88,
A93,
RELAT_2:def 6;
then V
in (Mn
-Seg W) or W
in (Mn
-Seg V) by
A93,
WELLORD1: 1;
then cb
in (
union (Mn
-Seg W)) or ca
in (
union (Mn
-Seg V)) by
A85,
A90,
A92,
TARSKI:def 4;
then cb
in (
PartUnion (W,Mn)) or ca
in (
PartUnion (V,Mn)) by
PCOMPS_2:def 1;
hence thesis by
A85,
A90,
XBOOLE_0:def 5;
end;
hence A
= B by
A83,
A88;
end;
end;
hence A
= B;
end;
0
< (2
|^ (n
+ 2)) by
PREPOWER: 6;
hence thesis by
A47,
TBSP_1: 11,
XREAL_1: 139;
end;
hence thesis by
NAGATA_1:def 1;
end;
hence Un9 is
sigma_discrete by
NAGATA_1:def 2;
end;
theorem ::
NAGATA_2:21
Th21: for T st T is
metrizable holds ex Un be
FamilySequence of T st Un is
Basis_sigma_discrete
proof
let T such that
A1: T is
metrizable;
consider metr be
Function of
[:the
carrier of T, the
carrier of T:],
REAL such that
A2: metr
is_metric_of the
carrier of T and
A3: (
Family_open_set (
SpaceMetr (the
carrier of T,metr)))
= the
topology of T by
A1,
PCOMPS_1:def 8;
set bbcT = (
bool (
bool the
carrier of T));
reconsider PM = (
SpaceMetr (the
carrier of T,metr)) as non
empty
MetrSpace by
A2,
PCOMPS_1: 36;
deffunc
BALL(
object) = { (
Ball (x,(1
/ (2
|^ (
In ($1,
NAT )))))) where x be
Point of PM : x is
Point of PM };
A4: for k be
object st k
in
NAT holds
BALL(k)
in (
bool (
bool the
carrier of T))
proof
let k be
object;
assume k
in
NAT ;
then
reconsider k as
Element of
NAT ;
BALL(k)
c= (
bool the
carrier of T)
proof
let B be
object;
assume B
in
BALL(k);
then ex x be
Point of PM st B
= (
Ball (x,(1
/ (2
|^ k)))) & x is
Point of PM;
then B
in (
Family_open_set PM) by
PCOMPS_1: 29;
hence thesis by
A3;
end;
hence thesis;
end;
consider FB be
FamilySequence of T such that
A5: for k be
object st k
in
NAT holds (FB
. k)
=
BALL(k) from
FUNCT_2:sch 2(
A4);
defpred
U[
set,
set] means ex FS be
FamilySequence of T st $2
= FS & (
Union FS) is
open & (
Union FS) is
Cover of T & (
Union FS)
is_finer_than (FB
. $1) & FS is
sigma_discrete;
set TPM = (
TopSpaceMetr PM);
A6: TPM
=
TopStruct (# the
carrier of PM, (
Family_open_set PM) #) by
PCOMPS_1:def 5;
then
A7: (
[#] T)
= (
[#] TPM) by
A2,
PCOMPS_2: 4;
A8: for n be
Element of
NAT holds ex Un be
Element of (
Funcs (
NAT ,bbcT)) st
U[n, Un]
proof
let n be
Element of
NAT ;
now
let U be
Subset of T;
assume U
in (FB
. n);
then U
in
BALL(n) by
A5;
then ex x be
Point of PM st U
= (
Ball (x,(1
/ (2
|^ n)))) & x is
Point of PM;
then U
in the
topology of T by
A3,
PCOMPS_1: 29;
hence U is
open by
PRE_TOPC:def 2;
end;
then
A9: (FB
. n) is
open;
A10: (
[#] TPM)
c= (
union (FB
. n))
proof
let x be
object;
assume x
in (
[#] TPM);
then
reconsider x9 = x as
Element of PM by
A6;
(2
|^ n)
>
0 by
NEWTON: 83;
then
A11: x9
in (
Ball (x9,(1
/ (2
|^ n)))) by
TBSP_1: 11,
XREAL_1: 139;
(
Ball (x9,(1
/ (2
|^ n))))
in
BALL(n);
then (
Ball (x9,(1
/ (2
|^ n))))
in (FB
. n) by
A5;
hence thesis by
A11,
TARSKI:def 4;
end;
(
union (FB
. n))
c= (
[#] TPM)
proof
given x be
object such that
A12: x
in (
union (FB
. n)) and
A13: not x
in (
[#] TPM);
consider A be
set such that
A14: x
in A and
A15: A
in (FB
. n) by
A12,
TARSKI:def 4;
A
in
BALL(n) by
A5,
A15;
then ex y be
Point of PM st A
= (
Ball (y,(1
/ (2
|^ n)))) & y is
Point of PM;
hence thesis by
A6,
A13,
A14;
end;
then (
[#] TPM)
= (
union (FB
. n)) by
A10;
then (FB
. n) is
Cover of T by
A7,
SETFAM_1: 45;
then
consider Un be
FamilySequence of T such that
A16: (
Union Un) is
open & (
Union Un) is
Cover of T & (
Union Un)
is_finer_than (FB
. n) & Un is
sigma_discrete by
A1,
A9,
Th20;
Un
in (
Funcs (
NAT ,bbcT)) by
FUNCT_2: 8;
hence thesis by
A16;
end;
consider Un be
sequence of (
Funcs (
NAT ,bbcT)) such that
A17: for n be
Element of
NAT holds
U[n, (Un
. n)] from
FUNCT_2:sch 3(
A8);
defpred
X[
object,
object] means for n, m st (
PairFunc
.
[n, m])
= $1 holds for Unn be
FamilySequence of T st Unn
= (Un
. n) holds $2
= (Unn
. m);
A18: for k be
object st k
in
NAT holds ex Ux be
object st Ux
in bbcT &
X[k, Ux]
proof
let k be
object;
assume k
in
NAT ;
then
reconsider k9 = k as
Element of
NAT ;
NAT
= (
rng
PairFunc ) by
Th2,
FUNCT_2:def 3;
then
consider nm be
object such that
A19: nm
in (
dom
PairFunc ) and
A20: k9
= (
PairFunc
. nm) by
FUNCT_1:def 3;
consider n,m be
object such that
A21: n
in
NAT and
A22: m
in
NAT and
A23: nm
=
[n, m] by
A19,
ZFMISC_1:def 2;
reconsider Unn = (Un
. n) as
FamilySequence of T by
A21,
FUNCT_2: 5,
FUNCT_2: 66;
take Ux = (Unn
. m);
(
dom Unn)
=
NAT by
PARTFUN1:def 2;
then m
in (
dom Unn) by
A22;
then Ux
in (
rng Unn) by
FUNCT_1: 3;
hence Ux
in bbcT;
let n1,m1 be
Nat such that
A24: (
PairFunc
.
[n1, m1])
= k;
reconsider nn1 = n1, mm1 = m1 as
Element of
NAT by
ORDINAL1:def 12;
now
let Unn be
FamilySequence of T such that
A25: Unn
= (Un
. nn1);
A26:
[n, m]
=
[nn1, mm1] by
A19,
A20,
A23,
A24,
Th2,
FUNCT_2: 19;
then n1
= n by
XTUPLE_0: 1;
hence Ux
= (Unn
. mm1) by
A25,
A26,
XTUPLE_0: 1;
end;
hence for Unn be
FamilySequence of T st Unn
= (Un
. n1) holds Ux
= (Unn
. m1);
end;
consider UX be
sequence of bbcT such that
A27: for k be
object st k
in
NAT holds
X[k, (UX
. k)] from
FUNCT_2:sch 1(
A18);
A28: for A st A is
open holds for p st p
in A holds ex B st B
in (
Union UX) & p
in B & B
c= A
proof
let A;
assume A is
open;
then
A29: A
in (
Family_open_set PM) by
A3,
PRE_TOPC:def 2;
let p such that
A30: p
in A;
reconsider p as
Element of PM by
A30,
A29;
consider r such that
A31: r
>
0 and
A32: (
Ball (p,r))
c= A by
A30,
A29,
PCOMPS_1:def 4;
consider n such that
A33: (1
/ (2
|^ n))
<= r by
A31,
PREPOWER: 92;
consider Unn1 be
FamilySequence of T such that
A34: (Un
. (n
+ 1))
= Unn1 and (
Union Unn1) is
open and
A35: (
Union Unn1) is
Cover of T and
A36: (
Union Unn1)
is_finer_than (FB
. (n
+ 1)) and Unn1 is
sigma_discrete by
A17;
(
union (
Union Unn1))
= (
[#] T) by
A35,
SETFAM_1: 45;
then
consider B be
set such that
A37: p
in B and
A38: B
in (
Union Unn1) by
TARSKI:def 4;
reconsider B as
Subset of PM by
A2,
A38,
PCOMPS_2: 4;
consider B1 be
set such that
A39: B1
in (FB
. (n
+ 1)) and
A40: B
c= B1 by
A36,
A38,
SETFAM_1:def 2;
consider k such that
A41: B
in (Unn1
. k) by
A38,
PROB_1: 12;
(n
+ 1)
= (
In ((n
+ 1),
NAT )) & B1
in
BALL(+) by
A5,
A39;
then
consider q be
Point of PM such that
A42: B1
= (
Ball (q,(1
/ (2
|^ (n
+ 1))))) and q is
Element of PM;
now
let s be
Element of PM;
assume s
in B;
then
A43: (
dist (q,s))
< (1
/ (2
|^ (n
+ 1))) by
A40,
A42,
METRIC_1: 11;
(
dist (q,p))
< (1
/ (2
|^ (n
+ 1))) by
A37,
A40,
A42,
METRIC_1: 11;
then (
dist (p,s))
<= ((
dist (q,p))
+ (
dist (q,s))) & ((
dist (q,p))
+ (
dist (q,s)))
< ((1
/ (2
|^ (n
+ 1)))
+ (1
/ (2
|^ (n
+ 1)))) by
A43,
METRIC_1: 4,
XREAL_1: 8;
then (
dist (p,s))
< (2
* (1
/ (2
|^ (n
+ 1)))) by
XXREAL_0: 2;
then (
dist (p,s))
< ((1
/ ((2
|^ n)
* 2))
* 2) by
NEWTON: 6;
then (
dist (p,s))
< (1
/ (2
|^ n)) by
XCMPLX_1: 92;
then (
dist (p,s))
< r by
A33,
XXREAL_0: 2;
hence s
in (
Ball (p,r)) by
METRIC_1: 11;
end;
then
A44: B
c= (
Ball (p,r));
reconsider kk = k as
Element of
NAT by
ORDINAL1:def 12;
(UX
. (
PairFunc
.
[(n
+ 1), kk]))
= (Unn1
. kk) by
A27,
A34;
then B
in (
Union UX) by
A41,
PROB_1: 12;
hence thesis by
A32,
A37,
A44,
XBOOLE_1: 1;
end;
for k be
Element of
NAT holds (UX
. k) is
discrete
proof
let k;
A45: k
in
NAT by
ORDINAL1:def 12;
NAT
= (
rng
PairFunc ) by
Th2,
FUNCT_2:def 3;
then
consider nm be
object such that
A46: nm
in (
dom
PairFunc ) and
A47: k
= (
PairFunc
. nm) by
FUNCT_1:def 3,
A45;
consider n,m be
object such that
A48: n
in
NAT and
A49: m
in
NAT and
A50: nm
=
[n, m] by
A46,
ZFMISC_1:def 2;
consider FS be
FamilySequence of T such that
A51: (Un
. n)
= FS and (
Union FS) is
open and (
Union FS) is
Cover of T and (
Union FS)
is_finer_than (FB
. n) and
A52: FS is
sigma_discrete by
A17,
A48;
(
dom FS)
=
NAT by
PARTFUN1:def 2;
then m
in (
dom FS) by
A49;
then (FS
. m)
in (
rng FS) by
FUNCT_1: 3;
then (FS
. m)
in bbcT;
then
reconsider FSm = (FS
. m) as
Subset-Family of T;
FSm is
discrete by
A49,
A52,
NAGATA_1:def 2;
hence thesis by
A27,
A47,
A48,
A49,
A50,
A51;
end;
then
A53: UX is
sigma_discrete by
NAGATA_1:def 2;
(
Union UX)
c= the
topology of T
proof
let UXk be
object;
assume UXk
in (
Union UX);
then
consider k such that
A54: UXk
in (UX
. k) by
PROB_1: 12;
reconsider UXk9 = UXk as
Subset of T by
A54;
A55: k
in
NAT by
ORDINAL1:def 12;
NAT
= (
rng
PairFunc ) by
Th2,
FUNCT_2:def 3;
then
consider nm be
object such that
A56: nm
in (
dom
PairFunc ) and
A57: k
= (
PairFunc
. nm) by
FUNCT_1:def 3,
A55;
consider n,m be
object such that
A58: n
in
NAT and
A59: m
in
NAT and
A60: nm
=
[n, m] by
A56,
ZFMISC_1:def 2;
reconsider Unn = (Un
. n) as
FamilySequence of T by
A58,
FUNCT_2: 5,
FUNCT_2: 66;
UXk
in (Unn
. m) by
A27,
A54,
A57,
A58,
A59,
A60,
A55;
then
A61: UXk
in (
Union Unn) by
A59,
PROB_1: 12;
ex FS be
FamilySequence of T st (Un
. n)
= FS & (
Union FS) is
open & (
Union FS) is
Cover of T & (
Union FS)
is_finer_than (FB
. n) & FS is
sigma_discrete by
A17,
A58;
then UXk9 is
open by
A61;
hence thesis by
PRE_TOPC:def 2;
end;
then (
Union UX) is
Basis of T by
A28,
YELLOW_9: 32;
then UX is
Basis_sigma_discrete by
A53,
NAGATA_1:def 5;
hence thesis;
end;
::$Notion-Name
theorem ::
NAGATA_2:22
for T holds (T is
regular & T is
T_1 & ex Bn be
FamilySequence of T st Bn is
Basis_sigma_discrete) iff T is
metrizable
proof
let T;
now
assume that
A1: T is
regular & T is
T_1 and
A2: ex Bn be
FamilySequence of T st Bn is
Basis_sigma_discrete;
consider Bn be
FamilySequence of T such that
A3: Bn is
Basis_sigma_discrete by
A2;
Bn is
sigma_discrete by
A3,
NAGATA_1:def 5;
then
A4: Bn is
sigma_locally_finite by
NAGATA_1: 12;
(
Union Bn) is
Basis of T by
A3,
NAGATA_1:def 5;
then Bn is
Basis_sigma_locally_finite by
A4,
NAGATA_1:def 6;
hence T is
metrizable by
A1,
Th19;
end;
hence thesis by
Th21,
NAGATA_1: 15;
end;