let L be complete LATTICE; for N being net of L
for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds
for M being subnet of N holds x = lim_inf M
let N be net of L; for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds
for M being subnet of N holds x = lim_inf M
let x be Element of L; ( x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) implies for M being subnet of N holds x = lim_inf M )
assume that
A1:
x = lim_inf N
and
A2:
for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p)
; for M being subnet of N holds x = lim_inf M
let M be subnet of N; x = lim_inf M
consider f being Function of M,N such that
A3:
the mapping of M = the mapping of N * f
and
A4:
for j being Element of N ex k being Element of M st
for m being Element of M st k <= m holds
j <= f . m
by YELLOW_6:def 9;
A5:
x <= lim_inf M
by A1, WAYBEL21:37;
A6:
for k0 being Element of M holds "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x
proof
let k0 be
Element of
M;
"/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x
defpred S1[
object ,
object ]
means for
j being
Element of
N for
v,
v9 being
Element of
M st $1
= j & $2
= v &
v9 >= v holds
(
v >= k0 &
f . v9 >= j &
f . v >= j );
A7:
for
j being
Element of
N ex
v being
Element of
M st
(
v >= k0 & ( for
v9 being
Element of
M st
v9 >= v holds
(
f . v9 >= j &
f . v >= j ) ) )
A11:
for
e being
object st
e in the
carrier of
N holds
ex
u being
object st
(
u in the
carrier of
M &
S1[
e,
u] )
proof
let e be
object ;
( e in the carrier of N implies ex u being object st
( u in the carrier of M & S1[e,u] ) )
assume
e in the
carrier of
N
;
ex u being object st
( u in the carrier of M & S1[e,u] )
then reconsider e9 =
e as
Element of
N ;
consider u being
Element of
M such that A12:
u >= k0
and A13:
for
v9 being
Element of
M st
v9 >= u holds
(
f . v9 >= e9 &
f . u >= e9 )
by A7;
take
u
;
( u in the carrier of M & S1[e,u] )
thus
u in the
carrier of
M
;
S1[e,u]
let j be
Element of
N;
for v, v9 being Element of M st e = j & u = v & v9 >= v holds
( v >= k0 & f . v9 >= j & f . v >= j )let v,
v9 be
Element of
M;
( e = j & u = v & v9 >= v implies ( v >= k0 & f . v9 >= j & f . v >= j ) )
assume that A14:
e = j
and A15:
u = v
and A16:
v9 >= v
;
( v >= k0 & f . v9 >= j & f . v >= j )
thus
v >= k0
by A12, A15;
( f . v9 >= j & f . v >= j )
thus
f . v9 >= j
by A13, A14, A15, A16;
f . v >= j
thus
f . v >= j
by A13, A14, A15, A16;
verum
end;
consider g being
Function such that A17:
dom g = the
carrier of
N
and A18:
rng g c= the
carrier of
M
and A19:
for
e being
object st
e in the
carrier of
N holds
S1[
e,
g . e]
from FUNCT_1:sch 6(A11);
reconsider g =
g as
Function of the
carrier of
N, the
carrier of
M by A17, A18, FUNCT_2:2;
A20:
for
j being
Element of
N holds
g . j >= k0
reconsider g =
g as
Function of
N,
M ;
reconsider p =
f * g as
Function of
N,
N ;
for
j being
Element of
N holds
j <= p . j
then reconsider p =
p as
greater_or_equal_to_id Function of
N,
N by Def1;
A21:
{ ((N * p) . j) where j is Element of (N * p) : verum } c= { (M . k) where k is Element of M : k >= k0 }
A25:
(
ex_inf_of { ((N * p) . j) where j is Element of (N * p) : verum } ,
L &
ex_inf_of { (M . k) where k is Element of M : k >= k0 } ,
L )
by YELLOW_0:17;
A26:
dom the
mapping of
(N * p) = the
carrier of
(N * p)
by FUNCT_2:def 1;
A27:
rng the
mapping of
(N * p) = { ((N * p) . j) where j is Element of (N * p) : verum }
A31:
inf (N * p) <= x
by A2;
inf (N * p) =
Inf
by WAYBEL_9:def 2
.=
"/\" (
{ ((N * p) . j) where j is Element of (N * p) : verum } ,
L)
by A27, YELLOW_2:def 6
;
then
"/\" (
{ (M . k) where k is Element of M : k >= k0 } ,
L)
<= inf (N * p)
by A25, A21, YELLOW_0:35;
hence
"/\" (
{ (M . k) where k is Element of M : k >= k0 } ,
L)
<= x
by A31, YELLOW_0:def 2;
verum
end;
for b being Element of L st b in { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } holds
b <= x
then A32:
x is_>=_than { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum }
by LATTICE3:def 9;
ex_sup_of { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } ,L
by YELLOW_0:17;
then
"\/" ( { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } ,L) <= x
by A32, YELLOW_0:def 9;
hence
x = lim_inf M
by A5, ORDERS_2:2; verum