set US = Pervin_quasi_uniformity T;
set FMT = FMT_Space_Str(# the carrier of (Pervin_quasi_uniformity T),(Neighborhood (Pervin_quasi_uniformity T)) #);
reconsider UT = FMT_Space_Str(# the carrier of (Pervin_quasi_uniformity T),(Neighborhood (Pervin_quasi_uniformity T)) #) as non empty strict FMT_Space_Str ;
A1:
for x being Element of UT ex y being Element of (Pervin_quasi_uniformity T) st
( x = y & U_FMT x = Neighborhood y )
now ( UT is U_FMT_local & UT is U_FMT_with_point & UT is U_FMT_filter )
for
x being
Element of
UT for
V being
Element of
U_FMT x ex
W being
Element of
U_FMT x st
for
y being
Element of
UT st
y is
Element of
W holds
V is
Element of
U_FMT y
proof
let x be
Element of
UT;
for V being Element of U_FMT x ex W being Element of U_FMT x st
for y being Element of UT st y is Element of W holds
V is Element of U_FMT ylet V be
Element of
U_FMT x;
ex W being Element of U_FMT x st
for y being Element of UT st y is Element of W holds
V is Element of U_FMT y
consider y being
Element of
(Pervin_quasi_uniformity T) such that
x = y
and A4:
U_FMT x = Neighborhood y
by A1;
A5:
V in Neighborhood y
by A4;
then consider V0 being
Element of the
entourages of
(Pervin_quasi_uniformity T) such that A6:
V = Neighborhood (
V0,
y)
;
Pervin_quasi_uniformity T is
axiom_U3
;
then consider W being
Element of the
entourages of
(Pervin_quasi_uniformity T) such that A7:
W * W c= V0
;
Neighborhood (
W,
y)
in { (Neighborhood (V,y)) where V is Element of the entourages of (Pervin_quasi_uniformity T) : verum }
;
then reconsider WN =
Neighborhood (
W,
y) as
Element of
Neighborhood y ;
A8:
for
x,
y,
z being
object st
[x,y] in W &
[y,z] in W holds
[x,z] in V0
proof
let x,
y,
z be
object ;
( [x,y] in W & [y,z] in W implies [x,z] in V0 )
assume that A9:
[x,y] in W
and A10:
[y,z] in W
;
[x,z] in V0
[x,z] in W * W
by A9, A10, RELAT_1:def 8;
hence
[x,z] in V0
by A7;
verum
end;
reconsider WN =
WN as
Element of
U_FMT x by A4;
take
WN
;
for y being Element of UT st y is Element of WN holds
V is Element of U_FMT y
hereby verum
let z be
Element of
UT;
( z is Element of WN implies V is Element of U_FMT z )assume
z is
Element of
WN
;
V is Element of U_FMT zthen
z in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in W }
;
then consider z0 being
Element of
(Pervin_quasi_uniformity T) such that A13:
z = z0
and A14:
[y,z0] in W
;
consider z1 being
Element of
(Pervin_quasi_uniformity T) such that A15:
z = z1
and A16:
U_FMT z = Neighborhood z1
by A1;
A17:
Neighborhood (
W,
z1)
c= Neighborhood (
V0,
y)
proof
let t be
object ;
TARSKI:def 3 ( not t in Neighborhood (W,z1) or t in Neighborhood (V0,y) )
assume
t in Neighborhood (
W,
z1)
;
t in Neighborhood (V0,y)
then consider y0 being
Element of
(Pervin_quasi_uniformity T) such that A18:
t = y0
and A19:
[z1,y0] in W
;
[y,t] in V0
by A18, A19, A15, A13, A14, A8;
hence
t in Neighborhood (
V0,
y)
by A18;
verum
end;
Neighborhood (
W,
z1)
in Neighborhood z1
;
then reconsider WW =
Neighborhood (
W,
z1) as
Element of
Neighborhood z1 ;
reconsider WW2 =
WW,
V2 =
V as
Subset of
(Pervin_quasi_uniformity T) by A5;
A20:
WW2 c= V2
by A6, A17;
Neighborhood z1 is
upper
by Th15;
hence
V is
Element of
U_FMT z
by A16, A20;
verum
end;
end; hence
UT is
U_FMT_local
;
( UT is U_FMT_with_point & UT is U_FMT_filter )
for
x being
Element of
UT for
V being
Element of
U_FMT x holds
x in V
hence
UT is
U_FMT_with_point
;
UT is U_FMT_filter
for
x being
Element of
UT holds
U_FMT x is
Filter of the
carrier of
UT
hence
UT is
U_FMT_filter
;
verum
hence
Pervin_quasi_uniformity T is topological
; verum