let L be complete lim-inf TopLattice; for A being non empty Subset of L holds
( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A )
let A be non empty Subset of L; ( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A )
xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L))
by WAYBEL28:def 4;
then A1:
xi L = { V where V is Subset of L : for p being Element of L st p in V holds
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in V }
by YELLOW_6:def 24;
set V = A ` ;
A2:
the topology of L = xi L
by Def2;
hereby ( ( for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A ) implies A is closed )
assume
A is
closed
;
for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in Athen
A ` in xi L
by A2, PRE_TOPC:def 2;
then A3:
ex
V being
Subset of
L st
(
V = A ` & ( for
p being
Element of
L st
p in V holds
for
N being
net of
L st
[N,p] in lim_inf-Convergence L holds
N is_eventually_in V ) )
by A1;
let F be
ultra Filter of
(BoolePoset ([#] L));
( A in F implies lim_inf F in A )assume A4:
A in F
;
lim_inf F in A
( ( for
M being
subnet of
a_net F holds
lim_inf F = lim_inf M ) &
a_net F in NetUniv L )
by Th14, Th16;
then A5:
[(a_net F),(lim_inf F)] in lim_inf-Convergence L
by WAYBEL28:def 3;
assume
not
lim_inf F in A
;
contradictionthen
lim_inf F in A `
by XBOOLE_0:def 5;
then
a_net F is_eventually_in A `
by A3, A5;
then consider i being
Element of
(a_net F) such that A6:
for
j being
Element of
(a_net F) st
i <= j holds
(a_net F) . j in A `
;
A7:
the
carrier of
(a_net F) = { [a,f] where a is Element of L, f is Element of F : a in f }
by YELLOW19:def 4;
i in the
carrier of
(a_net F)
;
then consider a being
Element of
L,
f being
Element of
F such that A8:
i = [a,f]
and
a in f
by A7;
reconsider A9 =
A,
f9 =
f as
Element of
(BoolePoset ([#] L)) by A4;
consider B being
Element of
(BoolePoset ([#] L)) such that A9:
B in F
and A10:
A9 >= B
and A11:
f9 >= B
by A4, WAYBEL_0:def 2;
set b = the
Element of
B;
not
Bottom (BoolePoset ([#] L)) in F
by WAYBEL_7:4;
then
not
B is
empty
by A9, YELLOW_1:18;
then A12:
the
Element of
B in B
;
the
carrier of
(BoolePoset ([#] L)) = bool the
carrier of
L
by WAYBEL_7:2;
then
[ the Element of B,B] in the
carrier of
(a_net F)
by A7, A9, A12;
then reconsider j =
[ the Element of B,B] as
Element of
(a_net F) ;
B c= f
by A11, YELLOW_1:2;
then
j `2 c= f
;
then
j `2 c= i `2
by A8;
then
j >= i
by YELLOW19:def 4;
then
(a_net F) . j in A `
by A6;
then
j `1 in A `
by YELLOW19:def 4;
then A13:
the
Element of
B in A `
;
B c= A
by A10, YELLOW_1:2;
hence
contradiction
by A12, A13, XBOOLE_0:def 5;
verum
end;
assume A14:
for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A
; A is closed
now for p being Element of L st p in A ` holds
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in A ` let p be
Element of
L;
( p in A ` implies for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in A ` )assume
p in A `
;
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in A ` then A15:
not
p in (A `) `
by XBOOLE_0:def 5;
reconsider x =
p as
Element of
L ;
let N be
net of
L;
( [N,p] in lim_inf-Convergence L implies N is_eventually_in A ` )assume A16:
[N,p] in lim_inf-Convergence L
;
N is_eventually_in A ` assume
not
N is_eventually_in A `
;
contradictionthen
N is_often_in A
by WAYBEL_0:10;
then consider N9 being
strict subnet of
N such that A17:
rng the
mapping of
N9 c= A
and A18:
N9 is
SubNetStr of
N
by Th17;
lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:]
by YELLOW_6:def 18;
then A19:
N in NetUniv L
by A16, ZFMISC_1:87;
then A20:
ex
N1 being
strict net of
L st
(
N1 = N & the
carrier of
N1 in the_universe_of the
carrier of
L )
by YELLOW_6:def 11;
set j0 = the
Element of
N9;
reconsider rj =
rng the
mapping of
(N9 | the Element of N9),
a =
A as
Element of
(BoolePoset ([#] L)) by WAYBEL_7:2;
set j2 = the
Element of
N9;
set G =
{ (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ;
set g =
rng the
mapping of
(N9 | the Element of N9);
A21:
rng the
mapping of
(N9 | the Element of N9) in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum }
;
for
g being
object st
g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } holds
g in the
carrier of
(BoolePoset ([#] L))
then reconsider G =
{ (rng the mapping of (N9 | j)) where j is Element of N9 : verum } as non
empty Subset of
(BoolePoset ([#] L)) by A21, TARSKI:def 3;
A22:
G c= fininfs G
by WAYBEL_0:50;
then
rj c= rng the
mapping of
N9
;
then
rj c= a
by A17;
then
(
rng the
mapping of
(N9 | the Element of N9) in G &
rj <= a )
by YELLOW_1:2;
then A26:
a in uparrow (fininfs G)
by A22, WAYBEL_0:def 16;
A27:
x = lim_inf N9
by A16, A19, WAYBEL28:def 3;
then A28:
x = "\/" (
{ (inf (N9 | j)) where j is Element of N9 : verum } ,
L)
by Th11;
the
carrier of
N9 c= the
carrier of
N
by A18, YELLOW_6:10;
then
the
carrier of
N9 in the_universe_of the
carrier of
L
by A20, CLASSES1:def 1;
then A29:
N9 in NetUniv L
by YELLOW_6:def 11;
A30:
not
{} in fininfs G
proof
assume
{} in fininfs G
;
contradiction
then consider Y being
finite Subset of
G such that A31:
{} = "/\" (
Y,
(BoolePoset ([#] L)))
and
ex_inf_of Y,
BoolePoset ([#] L)
;
defpred S1[
object ,
object ]
means ex
j being
Element of
N9 st
(
j = $2 & $1
= rng the
mapping of
(N9 | j) );
A32:
"/\" (
{},
(BoolePoset ([#] L))) =
Top (BoolePoset ([#] L))
by YELLOW_0:def 12
.=
[#] L
by YELLOW_1:19
;
reconsider Y =
Y as
finite Subset of
(BoolePoset ([#] L)) by XBOOLE_1:1;
A33:
for
x being
object st
x in Y holds
ex
y being
object st
(
y in the
carrier of
N9 &
S1[
x,
y] )
consider f being
Function such that A35:
(
dom f = Y &
rng f c= the
carrier of
N9 )
and A36:
for
x being
object st
x in Y holds
S1[
x,
f . x]
from FUNCT_1:sch 6(A33);
reconsider C =
rng f as
finite Subset of
([#] N9) by A35, FINSET_1:8;
[#] N9 is
directed
by WAYBEL_0:def 6;
then consider j0 being
Element of
N9 such that
j0 in [#] N9
and A37:
j0 is_>=_than C
by WAYBEL_0:1;
for
y being
set st
y in Y holds
rng the
mapping of
(N9 | j0) c= y
proof
let y be
set ;
( y in Y implies rng the mapping of (N9 | j0) c= y )
assume A38:
y in Y
;
rng the mapping of (N9 | j0) c= y
consider j1 being
Element of
N9 such that A39:
j1 = f . y
and A40:
y = rng the
mapping of
(N9 | j1)
by A36, A38;
A41:
f . y in rng f
by A35, A38, FUNCT_1:3;
then reconsider f1 =
f . y as
Element of
N9 by A35;
A42:
f1 <= j0
by A37, A41;
for
p being
object st
p in rng the
mapping of
(N9 | j0) holds
p in y
proof
let p be
object ;
( p in rng the mapping of (N9 | j0) implies p in y )
assume
p in rng the
mapping of
(N9 | j0)
;
p in y
then
p in rng ( the mapping of N9 | the carrier of (N9 | j0))
by WAYBEL_9:def 7;
then consider q being
object such that A43:
q in dom ( the mapping of N9 | the carrier of (N9 | j0))
and A44:
p = ( the mapping of N9 | the carrier of (N9 | j0)) . q
by FUNCT_1:def 3;
A45:
q in (dom the mapping of N9) /\ the
carrier of
(N9 | j0)
by A43, RELAT_1:61;
then
q in the
carrier of
(N9 | j0)
by XBOOLE_0:def 4;
then
q in { n9 where n9 is Element of N9 : j0 <= n9 }
by WAYBEL_9:12;
then consider n9 being
Element of
N9 such that A46:
q = n9
and A47:
j0 <= n9
;
f1 <= n9
by A42, A47, YELLOW_0:def 2;
then
q in { m9 where m9 is Element of N9 : j1 <= m9 }
by A39, A46;
then A48:
q in the
carrier of
(N9 | j1)
by WAYBEL_9:12;
q in dom the
mapping of
N9
by A45, XBOOLE_0:def 4;
then
q in (dom the mapping of N9) /\ the
carrier of
(N9 | j1)
by A48, XBOOLE_0:def 4;
then A49:
q in dom ( the mapping of N9 | the carrier of (N9 | j1))
by RELAT_1:61;
p = the
mapping of
N9 . q
by A43, A44, FUNCT_1:47;
then
p = ( the mapping of N9 | the carrier of (N9 | j1)) . q
by A49, FUNCT_1:47;
then
p in rng ( the mapping of N9 | the carrier of (N9 | j1))
by A49, FUNCT_1:3;
hence
p in y
by A40, WAYBEL_9:def 7;
verum
end;
hence
rng the
mapping of
(N9 | j0) c= y
;
verum
end;
then
rng the
mapping of
(N9 | j0) c= meet Y
by A31, A32, SETFAM_1:5;
then
rng the
mapping of
(N9 | j0) c= {}
by A31, A32, YELLOW_1:20;
hence
contradiction
;
verum
end;
for
y being
Element of
(BoolePoset ([#] L)) st
Bottom (BoolePoset ([#] L)) >= y holds
not
y in fininfs G
then
not
Bottom (BoolePoset ([#] L)) in uparrow (fininfs G)
by WAYBEL_0:def 16;
then
uparrow (fininfs G) is
proper
;
then consider F being
Filter of
(BoolePoset ([#] L)) such that A50:
uparrow (fininfs G) c= F
and A51:
F is
ultra
by WAYBEL_7:26;
A52:
fininfs G c= uparrow (fininfs G)
by WAYBEL_0:16;
A53:
{ (inf (N9 | j)) where j is Element of N9 : verum } c= { (inf f) where f is Subset of L : f in F }
then A56:
for
M being
subnet of
N9 st
M in NetUniv L holds
x = lim_inf M
;
{ (inf f) where f is Subset of L : f in F } is_<=_than x
proof
let y be
Element of
L;
LATTICE3:def 9 ( not y in { (inf f) where f is Subset of L : f in F } or y <= x )
assume
y in { (inf f) where f is Subset of L : f in F }
;
y <= x
then consider f0 being
Subset of
L such that A57:
y = inf f0
and A58:
f0 in F
;
defpred S1[
Element of
N9,
Element of
N9]
means ( $1
<= $2 &
N9 . $2
in f0 );
A59:
now for j being Element of N9 ex pj being Element of N9 st S1[j,pj]let j be
Element of
N9;
ex pj being Element of N9 st S1[j,pj]
not
Bottom (BoolePoset ([#] L)) in F
by A51, WAYBEL_7:4;
then A60:
not
{} in F
by YELLOW_1:18;
G c= uparrow (fininfs G)
by A22, A52;
then A61:
G c= F
by A50;
rng the
mapping of
(N9 | j) in G
;
then
f0 /\ (rng the mapping of (N9 | j)) in F
by A58, A61, WAYBEL_7:9;
then consider nj being
Element of
L such that A62:
nj in f0 /\ (rng the mapping of (N9 | j))
by A60, SUBSET_1:4;
nj in rng the
mapping of
(N9 | j)
by A62, XBOOLE_0:def 4;
then consider pj9 being
object such that A63:
pj9 in dom the
mapping of
(N9 | j)
and A64:
nj = the
mapping of
(N9 | j) . pj9
by FUNCT_1:def 3;
pj9 in the
carrier of
(N9 | j)
by A63;
then
pj9 in { y9 where y9 is Element of N9 : j <= y9 }
by WAYBEL_9:12;
then consider pj being
Element of
N9 such that A65:
pj = pj9
and A66:
j <= pj
;
reconsider pj9 =
pj9 as
Element of
(N9 | j) by A63;
take pj =
pj;
S1[j,pj]N9 . pj =
(N9 | j) . pj9
by A65, WAYBEL_9:16
.=
the
mapping of
(N9 | j) . pj9
;
hence
S1[
j,
pj]
by A62, A64, A66, XBOOLE_0:def 4;
verum end;
consider p being
Function of
N9,
N9 such that A67:
for
j being
Element of
N9 holds
S1[
j,
p . j]
from FUNCT_2:sch 3(A59);
for
b being
object st
b in rng the
mapping of
(N9 * p) holds
b in f0
then
rng the
mapping of
(N9 * p) c= f0
;
then A70:
"/\" (
f0,
L)
<= "/\" (
(rng the mapping of (N9 * p)),
L)
by WAYBEL_7:1;
A71:
for
M being
subnet of
N9 st
M in NetUniv L holds
x >= inf M
by A29, A56, WAYBEL28:3;
p is
greater_or_equal_to_id
by A67, WAYBEL28:def 1;
then A72:
inf (N9 * p) <= x
by A29, A27, A71, WAYBEL28:13;
inf (N9 * p) =
Inf
by WAYBEL_9:def 2
.=
"/\" (
(rng the mapping of (N9 * p)),
L)
by YELLOW_2:def 6
;
hence
y <= x
by A57, A72, A70, YELLOW_0:def 2;
verum
end; then A73:
lim_inf F <= x
by YELLOW_0:32;
(
ex_sup_of { (inf f) where f is Subset of L : f in F } ,
L &
ex_sup_of { (inf (N9 | j)) where j is Element of N9 : verum } ,
L )
by YELLOW_0:17;
then
x <= lim_inf F
by A28, A53, YELLOW_0:34;
then
x = lim_inf F
by A73, YELLOW_0:def 3;
hence
contradiction
by A14, A50, A51, A26, A15;
verum end;
then
A ` in xi L
by A1;
then
A ` is open
by A2;
hence
A is closed
; verum