let S, T be non empty /\-complete Poset; :: thesis: 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; :: thesis: 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; :: thesis: lim_inf (f * (X opp+id )) = inf (f .: X)
set M = X opp+id ;
set N = f * (X opp+id );
deffunc H₁( Element of (f * (X opp+id ))) -> set = { ((f * (X opp+id )) . i) where i is Element of (f * (X opp+id )) : i >= $1 } ;
deffunc H₂( Element of (f * (X opp+id ))) -> Element of the carrier of T = "/\" H₁($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 ) #) & the mapping of (f * (X opp+id )) = f * the mapping of (X opp+id ) ) by WAYBEL_9:def 8;
A2: ( the carrier of (X opp+id ) = X & the mapping of (X opp+id ) = id X ) by WAYBEL19:27, YELLOW_9:7;
defpred S₁[ set ] means verum;
deffunc H₃( set ) -> Element of the carrier of T = inf (f .: X);
A3: for j being Element of (f * (X opp+id )) st S₁[j] holds
H₂(j) = H₃(j)

proof

let j be Element of (f * (X opp+id )); :: thesis: ( S₁[j] implies H₂(j) = H₃(j) )
reconsider j = j as Element of (f * (X opp+id )) ;
A4: ( [#] (f * (X opp+id )) is directed & [#] (f * (X opp+id )) = the carrier of (f * (X opp+id )) ) by WAYBEL_0:def 6;
then consider i' being Element of (f * (X opp+id )) such that
A5: ( i' in [#] (f * (X opp+id )) & i' >= j & i' >= j ) by WAYBEL_0:def 1;
A6: H₁(j) c= f .: X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in H₁(j) or a in f .: X )
assume a in H₁(j) ; :: thesis: a in f .: X
then consider i being Element of (f * (X opp+id )) such that
A7: ( a = (f * (X opp+id )) . i & i >= j ) ;
reconsider i = i as Element of (f * (X opp+id )) ;
reconsider i' = i as Element of (X opp+id ) by A1;
A8: (f * (X opp+id )) . i = f . ((id X) . i) by A1, A2, FUNCT_2:21
.= f . i' by A2, FUNCT_1:35 ;
( i' in X & the carrier of T <> {} ) by A2;
hence a in f .: X by A7, A8, FUNCT_2:43; :: thesis: verum

end;

then ( H₁(j) c= the carrier of T & (f * (X opp+id )) . i' in H₁(j) ) by A5, XBOOLE_1:1;
then A9: ( ex_inf_of H₁(j),T & ex_inf_of f .: X,T ) by WAYBEL_0:76;
then A10: H₂(j) >= inf (f .: X) by A6, YELLOW_0:35;
H₂(j) is_<=_than f .: X

proof

let x be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not x in f .: X or H₂(j) <= x )
assume x in f .: X ; :: thesis: H₂(j) <= x
then consider y being set such that
A11: ( y in the carrier of S & y in X & x = f . y ) by FUNCT_2:115;
reconsider y = y as Element of (f * (X opp+id )) by A1, A11, YELLOW_9:7;
consider i being Element of (f * (X opp+id )) such that
A12: ( i in [#] (f * (X opp+id )) & i >= y & i >= j ) by A4, WAYBEL_0:def 1;
i in X by A1, A2;
then reconsider xi = i, xy = y as Element of S by A11;
X opp+id is full SubRelStr of S opp by YELLOW_9:7;
then ( f * (X opp+id ) is full SubRelStr of S opp & xi = xi ~ & xy = xy ~ ) by A1, Th12;
then xi ~ >= xy ~ by A12, YELLOW_0:60;
then xi <= xy by LATTICE3:9;
then A13: f . xi <= x by A11, WAYBEL_1:def 2;
(f * (X opp+id )) . i = f . ((id X) . i) by A1, A2, FUNCT_2:21
.= f . xi by A1, A2, FUNCT_1:35 ;
then f . xi in H₁(j) by A12;
then f . xi >= H₂(j) by A9, YELLOW_4:2;
hence H₂(j) <= x by A13, ORDERS_2:26; :: thesis: verum

end;

then H₂(j) <= inf (f .: X) by A9, YELLOW_0:31;
hence ( S₁[j] implies H₂(j) = H₃(j) ) by A10, ORDERS_2:25; :: thesis: verum

end;

A14: ex j being Element of (f * (X opp+id )) st S₁[j] ;
{ H₂(j) where j is Element of (f * (X opp+id )) : S₁[j] } = { H₃(j) where j is Element of (f * (X opp+id )) : S₁[j] } from FRAENKEL:sch 6(A3)
.= { (inf (f .: X)) where j is Element of (f * (X opp+id )) : S₁[j] }
.= {(inf (f .: X))} from LATTICE3:sch 1(A14) ;
hence lim_inf (f * (X opp+id )) = sup {(inf (f .: X))} by WAYBEL11:def 6
.= inf (f .: X) by YELLOW_0:39 ;
:: thesis: verum