let L be complete LATTICE; :: thesis: for F being proper Filter of (BoolePoset ([#] L)) holds lim_inf F = lim_inf ()
let F be proper Filter of (BoolePoset ([#] L)); :: thesis: lim_inf F = lim_inf ()
set X = { (inf (() | i)) where i is Element of () : verum } ;
set Y = { (inf B) where B is Subset of L : B in F } ;
for x being object st x in { (inf (() | i)) where i is Element of () : verum } holds
x in { (inf B) where B is Subset of L : B in F }
proof
let x be object ; :: thesis: ( x in { (inf (() | i)) where i is Element of () : verum } implies x in { (inf B) where B is Subset of L : B in F } )
assume x in { (inf (() | i)) where i is Element of () : verum } ; :: thesis: x in { (inf B) where B is Subset of L : B in F }
then consider i being Element of () such that
A1: x = inf (() | i) ;
reconsider i = i as Element of () ;
i in the carrier of () ;
then i in { [b,g] where b is Element of L, g is Element of F : b in g } by YELLOW19:def 4;
then consider a being Element of L, f being Element of F such that
A2: i = [a,f] and
a in f ;
reconsider i = i as Element of () ;
reconsider f = f as Element of (BoolePoset ([#] L)) ;
reconsider f = f as Subset of L by WAYBEL_7:2;
[a,f] `2 = f ;
then inf f = inf (() | i) by ;
hence x in { (inf B) where B is Subset of L : B in F } by A1; :: thesis: verum
end;
then A3: { (inf (() | i)) where i is Element of () : verum } c= { (inf B) where B is Subset of L : B in F } ;
for x being object st x in { (inf B) where B is Subset of L : B in F } holds
x in { (inf (() | i)) where i is Element of () : verum }
proof
let x be object ; :: thesis: ( x in { (inf B) where B is Subset of L : B in F } implies x in { (inf (() | i)) where i is Element of () : verum } )
assume x in { (inf B) where B is Subset of L : B in F } ; :: thesis: x in { (inf (() | i)) where i is Element of () : verum }
then consider B being Subset of L such that
A4: x = inf B and
A5: B in F ;
not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;
then B <> {} by ;
then consider a being Element of L such that
A6: a in B by SUBSET_1:4;
reconsider B = B as Element of F by A5;
[a,B] in { [b,f] where b is Element of L, f is Element of F : b in f } by A6;
then reconsider i = [a,B] as Element of () by YELLOW19:def 4;
[a,B] `2 = B ;
then x = inf (() | i) by ;
hence x in { (inf (() | i)) where i is Element of () : verum } ; :: thesis: verum
end;
then A7: { (inf B) where B is Subset of L : B in F } c= { (inf (() | i)) where i is Element of () : verum } ;
lim_inf () = "\/" ( { (inf (() | i)) where i is Element of () : verum } ,L) by Th11;
hence lim_inf F = lim_inf () by ; :: thesis: verum