let R be non empty /\-complete Poset; for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F
let F be non empty filtered Subset of R; lim_inf (F opp+id) = inf F
set N = F opp+id ;
defpred S1[ set ] means verum;
deffunc H1( Element of (F opp+id)) -> Element of the carrier of R = inf F;
deffunc H2( Element of (F opp+id)) -> Element of the carrier of R = "/\" ( { ((F opp+id) . i) where i is Element of (F opp+id) : i >= $1 } ,R);
A1:
for v being Element of (F opp+id) st S1[v] holds
H1(v) = H2(v)
proof
let v be
Element of
(F opp+id);
( S1[v] implies H1(v) = H2(v) )
set X =
{ ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } ;
A2:
the
carrier of
(F opp+id) = F
by YELLOW_9:7;
then
v in F
;
then reconsider j =
v as
Element of
R ;
reconsider vv =
v as
Element of
(F opp+id) ;
A3:
{ ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } c= F
vv <= vv
;
then
(F opp+id) . v in { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v }
;
then reconsider X =
{ ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } as non
empty Subset of
R by A3, XBOOLE_1:1;
A5:
ex_inf_of F,
R
by WAYBEL_0:76;
A6:
ex_inf_of X,
R
by WAYBEL_0:76;
then A7:
inf X >= inf F
by A3, A5, YELLOW_0:35;
F is_>=_than inf X
proof
let a be
Element of
R;
LATTICE3:def 8 ( not a in F or inf X <= a )
assume
a in F
;
inf X <= a
then consider b being
Element of
R such that A8:
b in F
and A9:
a >= b
and A10:
j >= b
by A2, WAYBEL_0:def 2;
reconsider k =
b as
Element of
(F opp+id) by A8, YELLOW_9:7;
A11:
F opp+id is
full SubRelStr of
R opp
by YELLOW_9:7;
A12:
j ~ <= b ~
by A10, LATTICE3:9;
A13:
(F opp+id) . k = b
by YELLOW_9:7;
k >= vv
by A11, A12, YELLOW_0:60;
then
b in X
by A13;
then A14:
{b} c= X
by ZFMISC_1:31;
A15:
ex_inf_of {b},
R
by YELLOW_0:38;
inf {b} = b
by YELLOW_0:39;
then
b >= inf X
by A6, A14, A15, YELLOW_0:35;
hence
inf X <= a
by A9, YELLOW_0:def 2;
verum
end;
then
inf F >= "/\" (
X,
R)
by A5, YELLOW_0:31;
hence
(
S1[
v] implies
H1(
v)
= H2(
v) )
by A7, ORDERS_2:2;
verum
end;
A16:
{ H1(j) where j is Element of (F opp+id) : S1[j] } = { H2(k) where k is Element of (F opp+id) : S1[k] }
from FRAENKEL:sch 6(A1);
A17:
ex j being Element of (F opp+id) st S1[j]
;
{ (inf F) where j is Element of (F opp+id) : S1[j] } = {(inf F)}
from LATTICE3:sch 1(A17);
hence lim_inf (F opp+id) =
"\/" ({(inf F)},R)
by A16, WAYBEL11:def 6
.=
inf F
by YELLOW_0:39
;
verum