let S, T be non empty /\-complete Poset; for X being non empty filtered Subset of S
for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X)
let X be non empty filtered Subset of S; for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X)
let f be monotone Function of S,T; lim_inf (f * (X opp+id)) = inf (f .: X)
set M = X opp+id ;
set N = f * (X opp+id);
deffunc H1( Element of (f * (X opp+id))) -> set = { ((f * (X opp+id)) . i) where i is Element of (f * (X opp+id)) : i >= $1 } ;
deffunc H2( Element of (f * (X opp+id))) -> Element of the carrier of T = "/\" (H1($1),T);
A1:
RelStr(# the carrier of (f * (X opp+id)), the InternalRel of (f * (X opp+id)) #) = RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #)
by WAYBEL_9:def 8;
A2:
the mapping of (f * (X opp+id)) = f * the mapping of (X opp+id)
by WAYBEL_9:def 8;
A3:
the carrier of (X opp+id) = X
by YELLOW_9:7;
A4:
the mapping of (X opp+id) = id X
by WAYBEL19:27;
defpred S1[ set ] means verum;
deffunc H3( set ) -> Element of the carrier of T = inf (f .: X);
A5:
for j being Element of (f * (X opp+id)) st S1[j] holds
H2(j) = H3(j)
proof
let j be
Element of
(f * (X opp+id));
( S1[j] implies H2(j) = H3(j) )
reconsider j =
j as
Element of
(f * (X opp+id)) ;
A6:
[#] (f * (X opp+id)) is
directed
by WAYBEL_0:def 6;
then consider i9 being
Element of
(f * (X opp+id)) such that
i9 in [#] (f * (X opp+id))
and A7:
i9 >= j
and
i9 >= j
;
A8:
H1(
j)
c= f .: X
then A11:
H1(
j)
c= the
carrier of
T
by XBOOLE_1:1;
(f * (X opp+id)) . i9 in H1(
j)
by A7;
then A12:
ex_inf_of H1(
j),
T
by A11, WAYBEL_0:76;
A13:
ex_inf_of f .: X,
T
by WAYBEL_0:76;
then A14:
H2(
j)
>= inf (f .: X)
by A8, A12, YELLOW_0:35;
H2(
j)
is_<=_than f .: X
proof
let x be
Element of
T;
LATTICE3:def 8 ( not x in f .: X or H2(j) <= x )
assume
x in f .: X
;
H2(j) <= x
then consider y being
object such that A15:
y in the
carrier of
S
and A16:
y in X
and A17:
x = f . y
by FUNCT_2:64;
reconsider y =
y as
Element of
(f * (X opp+id)) by A1, A16, YELLOW_9:7;
consider i being
Element of
(f * (X opp+id)) such that
i in [#] (f * (X opp+id))
and A18:
i >= y
and A19:
i >= j
by A6;
i in X
by A1, A3;
then reconsider xi =
i,
xy =
y as
Element of
S by A15;
X opp+id is
full SubRelStr of
S opp
by YELLOW_9:7;
then
f * (X opp+id) is
full SubRelStr of
S opp
by A1, Th12;
then
xi ~ >= xy ~
by A18, YELLOW_0:59;
then
xi <= xy
by LATTICE3:9;
then A20:
f . xi <= x
by A17, WAYBEL_1:def 2;
(f * (X opp+id)) . i =
f . ((id X) . i)
by A1, A2, A4, FUNCT_2:15
.=
f . xi
by A1, A3
;
then
f . xi in H1(
j)
by A19;
then
f . xi >= H2(
j)
by A12, YELLOW_4:2;
hence
H2(
j)
<= x
by A20, ORDERS_2:3;
verum
end;
then
H2(
j)
<= inf (f .: X)
by A13, YELLOW_0:31;
hence
(
S1[
j] implies
H2(
j)
= H3(
j) )
by A14, ORDERS_2:2;
verum
end;
A21:
ex j being Element of (f * (X opp+id)) st S1[j]
;
{ H2(j) where j is Element of (f * (X opp+id)) : S1[j] } =
{ H3(j) where j is Element of (f * (X opp+id)) : S1[j] }
from FRAENKEL:sch 6(A5)
.=
{ (inf (f .: X)) where j is Element of (f * (X opp+id)) : S1[j] }
.=
{(inf (f .: X))}
from LATTICE3:sch 1(A21)
;
hence lim_inf (f * (X opp+id)) =
sup {(inf (f .: X))}
by WAYBEL11:def 6
.=
inf (f .: X)
by YELLOW_0:39
;
verum