let L be complete LATTICE; :: thesis: for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)
let N be net of L; :: thesis: lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)
set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ;
set Y = { (inf (N | i)) where i is Element of N : verum } ;
for x being object st x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } holds
x in { (inf (N | i)) where i is Element of N : verum }
proof
let x be object ; :: thesis: ( x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } implies x in { (inf (N | i)) where i is Element of N : verum } )
assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ; :: thesis: x in { (inf (N | i)) where i is Element of N : verum }
then consider j being Element of N such that
A1: x = "/\" ( { (N . i) where i is Element of N : i >= j } ,L) ;
reconsider x = x as Element of L by A1;
set S = { (N . i) where i is Element of N : i >= j } ;
reconsider i = j as Element of N ;
for b being object st b in rng the mapping of (N | i) holds
b in { (N . i) where i is Element of N : i >= j }
proof
let b be object ; :: thesis: ( b in rng the mapping of (N | i) implies b in { (N . i) where i is Element of N : i >= j } )
assume b in rng the mapping of (N | i) ; :: thesis: b in { (N . i) where i is Element of N : i >= j }
then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;
then consider k being Element of (N | i) such that
A2: b = (N | i) . k ;
the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;
then reconsider l = k as Element of N ;
k in the carrier of (N | i) ;
then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;
then A3: ex y being Element of N st
( k = y & i <= y ) ;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
hence b in { (N . i) where i is Element of N : i >= j } by A2, A3; :: thesis: verum
end;
then A4: rng the mapping of (N | i) c= { (N . i) where i is Element of N : i >= j } ;
A5: ex_inf_of { (N . i) where i is Element of N : i >= j } ,L by YELLOW_0:17;
then A6: { (N . i) where i is Element of N : i >= j } is_>=_than x by A1, YELLOW_0:def 10;
A7: rng the mapping of (N | i) is_>=_than x by A6, A4;
for b being object st b in { (N . i) where i is Element of N : i >= j } holds
b in rng the mapping of (N | i)
proof
let b be object ; :: thesis: ( b in { (N . i) where i is Element of N : i >= j } implies b in rng the mapping of (N | i) )
assume b in { (N . i) where i is Element of N : i >= j } ; :: thesis: b in rng the mapping of (N | i)
then consider k being Element of N such that
A8: b = N . k and
A9: k >= j ;
reconsider l = k as Element of N ;
l in { y where y is Element of N : i <= y } by A9;
then reconsider k = k as Element of (N | i) by WAYBEL_9:12;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A8;
hence b in rng the mapping of (N | i) by WAYBEL11:19; :: thesis: verum
end;
then { (N . i) where i is Element of N : i >= j } c= rng the mapping of (N | i) ;
then { (N . i) where i is Element of N : i >= j } = rng the mapping of (N | i) by A4;
then for a being Element of L st rng the mapping of (N | i) is_>=_than a holds
a <= x by A1, A5, YELLOW_0:def 10;
then consider i being Element of N such that
A10: ( ex_inf_of rng the mapping of (N | i),L & rng the mapping of (N | i) is_>=_than x & ( for a being Element of L st rng the mapping of (N | i) is_>=_than a holds
a <= x ) ) by A7, YELLOW_0:17;
A11: inf (N | i) = Inf by WAYBEL_9:def 2
.= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def 6 ;
x = "/\" ((rng the mapping of (N | i)),L) by A10, YELLOW_0:def 10;
hence x in { (inf (N | i)) where i is Element of N : verum } by A11; :: thesis: verum
end;
then A12: ( lim_inf N = "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ,L) & { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } c= { (inf (N | i)) where i is Element of N : verum } ) by WAYBEL11:def 6;
for x being object st x in { (inf (N | i)) where i is Element of N : verum } holds
x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }
proof
let x be object ; :: thesis: ( x in { (inf (N | i)) where i is Element of N : verum } implies x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } )
assume x in { (inf (N | i)) where i is Element of N : verum } ; :: thesis: x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }
then consider i being Element of N such that
A13: x = inf (N | i) ;
set S = { (N . j) where j is Element of N : j >= i } ;
for b being object st b in rng the mapping of (N | i) holds
b in { (N . j) where j is Element of N : j >= i }
proof
let b be object ; :: thesis: ( b in rng the mapping of (N | i) implies b in { (N . j) where j is Element of N : j >= i } )
assume b in rng the mapping of (N | i) ; :: thesis: b in { (N . j) where j is Element of N : j >= i }
then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;
then consider k being Element of (N | i) such that
A14: b = (N | i) . k ;
the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;
then reconsider l = k as Element of N ;
k in the carrier of (N | i) ;
then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;
then A15: ex y being Element of N st
( k = y & i <= y ) ;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
hence b in { (N . j) where j is Element of N : j >= i } by A14, A15; :: thesis: verum
end;
then A16: rng the mapping of (N | i) c= { (N . j) where j is Element of N : j >= i } ;
reconsider x = x as Element of L by A13;
A17: x = Inf by A13, WAYBEL_9:def 2
.= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def 6 ;
for b being object st b in { (N . j) where j is Element of N : j >= i } holds
b in rng the mapping of (N | i)
proof
let b be object ; :: thesis: ( b in { (N . j) where j is Element of N : j >= i } implies b in rng the mapping of (N | i) )
assume b in { (N . j) where j is Element of N : j >= i } ; :: thesis: b in rng the mapping of (N | i)
then consider k being Element of N such that
A18: b = N . k and
A19: k >= i ;
reconsider l = k as Element of N ;
l in { y where y is Element of N : i <= y } by A19;
then reconsider k = k as Element of (N | i) by WAYBEL_9:12;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A18;
hence b in rng the mapping of (N | i) by WAYBEL11:19; :: thesis: verum
end;
then { (N . j) where j is Element of N : j >= i } c= rng the mapping of (N | i) ;
then rng the mapping of (N | i) = { (N . j) where j is Element of N : j >= i } by A16;
hence x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } by A17; :: thesis: verum
end;
then { (inf (N | i)) where i is Element of N : verum } c= { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ;
hence lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L) by A12, XBOOLE_0:def 10; :: thesis: verum