let S, T be with_infima Poset; for a, b being Element of S
for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)
let a, b be Element of S; for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)
let f be Function of S,T; lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)
set N = Net-Str (a,b);
set fN = f * (Net-Str (a,b));
A1:
RelStr(# the carrier of (f * (Net-Str (a,b))), the InternalRel of (f * (Net-Str (a,b))) #) = RelStr(# the carrier of (Net-Str (a,b)), the InternalRel of (Net-Str (a,b)) #)
by WAYBEL_9:def 8;
A2:
for j being Element of (f * (Net-Str (a,b))) holds { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } = {(f . a),(f . b)}
proof
let j be
Element of
(f * (Net-Str (a,b)));
{ ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } = {(f . a),(f . b)}
reconsider jj =
j as
Element of
(Net-Str (a,b)) by A1;
thus
{ ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } c= {(f . a),(f . b)}
XBOOLE_0:def 10 {(f . a),(f . b)} c= { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } proof
let x be
object ;
TARSKI:def 3 ( not x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } or x in {(f . a),(f . b)} )
assume
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
;
x in {(f . a),(f . b)}
then consider i1 being
Element of
(f * (Net-Str (a,b))) such that A3:
x = (f * (Net-Str (a,b))) . i1
and
i1 >= j
;
reconsider I1 =
i1 as
Element of
(Net-Str (a,b)) by A1;
i1 in the
carrier of
(Net-Str (a,b))
by A1;
then A4:
i1 in dom the
mapping of
(Net-Str (a,b))
by FUNCT_2:def 1;
(f * (Net-Str (a,b))) . i1 =
(f * the mapping of (Net-Str (a,b))) . i1
by WAYBEL_9:def 8
.=
f . ((Net-Str (a,b)) . I1)
by A4, FUNCT_1:13
;
then
(
(f * (Net-Str (a,b))) . i1 = f . a or
(f * (Net-Str (a,b))) . i1 = f . b )
by Th5;
hence
x in {(f . a),(f . b)}
by A3, TARSKI:def 2;
verum
end;
thus
{(f . a),(f . b)} c= { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
verumproof
let x be
object ;
TARSKI:def 3 ( not x in {(f . a),(f . b)} or x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } )
assume A5:
x in {(f . a),(f . b)}
;
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
A6:
j in the
carrier of
(Net-Str (a,b))
by A1;
reconsider J =
j as
Element of
NAT by A1, Def3;
A7:
j in dom the
mapping of
(Net-Str (a,b))
by A6, FUNCT_2:def 1;
defpred S1[
Element of
NAT ]
means ex
k being
Element of
NAT st $1
= 2
* k;
per cases
( x = f . a or x = f . b )
by A5, TARSKI:def 2;
suppose A8:
x = f . a
;
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } reconsider jj =
j as
Element of
(Net-Str (a,b)) by A1;
now x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } per cases
( S1[J] or not S1[J] )
;
suppose A9:
S1[
J]
;
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A10:
(f * (Net-Str (a,b))) . j =
(f * the mapping of (Net-Str (a,b))) . j
by WAYBEL_9:def 8
.=
f . ( the mapping of (Net-Str (a,b)) . j)
by A7, FUNCT_1:13
.=
f . (((a,b) ,...) . j)
by Def3
.=
f . a
by A9, Def1
;
j <= j
;
hence
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
by A8, A10;
verum end; suppose A11:
not
S1[
J]
;
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A12:
(Net-Str (a,b)) . jj =
((a,b) ,...) . jj
by Def3
.=
b
by A11, Def1
;
reconsider k =
J + 1 as
Element of
(f * (Net-Str (a,b))) by A1, Def3;
reconsider kk =
k as
Element of
(Net-Str (a,b)) by A1;
kk in the
carrier of
(Net-Str (a,b))
;
then A13:
kk in dom the
mapping of
(Net-Str (a,b))
by FUNCT_2:def 1;
A14:
(f * (Net-Str (a,b))) . k =
(f * the mapping of (Net-Str (a,b))) . k
by WAYBEL_9:def 8
.=
f . ((Net-Str (a,b)) . kk)
by A13, FUNCT_1:13
.=
f . a
by A12, Th6
;
J + 1
>= J
by NAT_1:11;
then
kk >= jj
by Def3;
then
[jj,kk] in the
InternalRel of
(Net-Str (a,b))
by ORDERS_2:def 5;
then
k >= j
by A1, ORDERS_2:def 5;
hence
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
by A8, A14;
verum end; end; end; hence
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
;
verum end; suppose A15:
x = f . b
;
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } now x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } per cases
( not S1[J] or S1[J] )
;
suppose A16:
not
S1[
J]
;
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A17:
(f * (Net-Str (a,b))) . j =
(f * the mapping of (Net-Str (a,b))) . j
by WAYBEL_9:def 8
.=
f . ( the mapping of (Net-Str (a,b)) . j)
by A7, FUNCT_1:13
.=
f . (((a,b) ,...) . j)
by Def3
.=
f . b
by A16, Def1
;
j <= j
;
hence
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
by A15, A17;
verum end; suppose A18:
S1[
J]
;
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A19:
(Net-Str (a,b)) . jj =
((a,b) ,...) . j
by Def3
.=
a
by A18, Def1
;
reconsider k =
J + 1 as
Element of
(f * (Net-Str (a,b))) by A1, Def3;
reconsider kk =
k as
Element of
(Net-Str (a,b)) by Def3;
kk in the
carrier of
(Net-Str (a,b))
;
then A20:
kk in dom the
mapping of
(Net-Str (a,b))
by FUNCT_2:def 1;
A21:
(f * (Net-Str (a,b))) . k =
(f * the mapping of (Net-Str (a,b))) . k
by WAYBEL_9:def 8
.=
f . ((Net-Str (a,b)) . kk)
by A20, FUNCT_1:13
.=
f . b
by A19, Th6
;
J + 1
>= J
by NAT_1:11;
then
kk >= jj
by Def3;
then
[jj,kk] in the
InternalRel of
(Net-Str (a,b))
by ORDERS_2:def 5;
then
k >= j
by A1, ORDERS_2:def 5;
hence
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
by A15, A21;
verum end; end; end; hence
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
;
verum end; end;
end;
end;
defpred S1[ Element of (f * (Net-Str (a,b))), Element of (f * (Net-Str (a,b)))] means $1 >= $2;
deffunc H1( Element of (f * (Net-Str (a,b)))) -> set = { ((f * (Net-Str (a,b))) . i1) where i1 is Element of (f * (Net-Str (a,b))) : S1[i1,$1] } ;
defpred S2[ set ] means verum;
deffunc H2( Element of (f * (Net-Str (a,b)))) -> Element of K32( the carrier of T) = {(f . a),(f . b)};
deffunc H3( Element of (f * (Net-Str (a,b)))) -> Element of the carrier of T = "/\" (H1($1),T);
deffunc H4( Element of (f * (Net-Str (a,b)))) -> Element of the carrier of T = "/\" (H2($1),T);
deffunc H5( set ) -> Element of the carrier of T = (f . a) "/\" (f . b);
A22:
for jj being Element of (f * (Net-Str (a,b))) holds H3(jj) = H5(jj)
A23:
{ H3(j3) where j3 is Element of (f * (Net-Str (a,b))) : S2[j3] } = { H5(j4) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] }
from FRAENKEL:sch 5(A22);
A24:
{ ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } c= {((f . a) "/\" (f . b))}
{((f . a) "/\" (f . b))} c= { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] }
then
{ ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } = {((f . a) "/\" (f . b))}
by A24;
hence
lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)
by A23, YELLOW_0:39; verum