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