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 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)); :: thesis: ( 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
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in H1(j) or a in f .: X )
assume a in H1(j) ; :: thesis: a in f .: X
then consider i being Element of (f * (X opp+id)) such that
A9: a = (f * (X opp+id)) . i and
i >= j ;
reconsider i = i as Element of (f * (X opp+id)) ;
reconsider i9 = i as Element of (X opp+id) by A1;
A10: (f * (X opp+id)) . i = f . ((id X) . i) by A1, A2, A4, FUNCT_2:15
.= f . i9 by A3 ;
i9 in X by A3;
hence a in f .: X by A9, A10, FUNCT_2:35; :: thesis: verum
end;
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; :: according to LATTICE3:def 8 :: thesis: ( not x in f .: X or H2(j) <= x )
assume x in f .: X ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ;
:: thesis: verum