let LUS be Locally-UniformSpace; LUS is topological
set UT = FMT_Space_Str(# the carrier of LUS,(Neighborhood LUS) #);
reconsider UT = FMT_Space_Str(# the carrier of LUS,(Neighborhood LUS) #) as non empty strict FMT_Space_Str ;
A1:
for x being Element of UT ex y being Element of LUS 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
LUS 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
LUS such that A6:
V = Neighborhood (
V0,
y)
;
LUS is
axiom_UL
;
then consider W being
Element of the
entourages of
LUS such that A7:
{ z where z is Element of LUS : [y,z] in W * W } c= Neighborhood (
V0,
y)
;
Neighborhood (
W,
y)
in { (Neighborhood (V,y)) where V is Element of the entourages of LUS : verum }
;
then reconsider WN =
Neighborhood (
W,
y) as
Element of
Neighborhood y ;
A8:
for
t,
z being
object st
[y,t] in W &
[t,z] in W holds
[y,z] in V0
proof
let t,
z be
object ;
( [y,t] in W & [t,z] in W implies [y,z] in V0 )
assume that A9:
[y,t] in W
and A10:
[t,z] in W
;
[y,z] in V0
consider R1,
R2 being
Relation of the
carrier of
LUS such that A11:
W = R1
and A12:
W = R2
and
W * W = R1 * R2
;
AAA:
[y,z] in R1 * R2
by A9, A10, A11, A12, RELAT_1:def 8;
consider a,
b being
object such that
a in the
carrier of
LUS
and A12B:
b in the
carrier of
LUS
and A12C:
[t,z] = [a,b]
by A10, ZFMISC_1:def 2;
reconsider z =
z as
Element of
LUS by A12C, A12B, XTUPLE_0:1;
z in { z where z is Element of LUS : [y,z] in W * W }
by AAA, A11, A12;
then
z in Neighborhood (
V0,
y)
by A7;
then
ex
z0 being
Element of
LUS st
(
z = z0 &
[y,z0] in V0 )
;
hence
[y,z] in V0
;
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 LUS : [y,z] in W }
;
then consider z0 being
Element of
LUS such that A13:
z = z0
and A14:
[y,z0] in W
;
consider z1 being
Element of
LUS 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
LUS 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
LUS 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
LUS is topological
; verum