let L be complete LATTICE; :: thesis: for F being ultra Filter of (BoolePoset ([#] L))
for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)
let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)
let p be greater_or_equal_to_id Function of (a_net F),(a_net F); :: thesis: lim_inf F >= inf ((a_net F) * p)
set M = (a_net F) * p;
A1:
the carrier of ((a_net F) * p) = the carrier of (a_net F)
by WAYBEL28:7;
then reconsider g = p as Function of ((a_net F) * p),(a_net F) ;
set rM = rng the mapping of ((a_net F) * p);
consider C being Element of F;
F c= the carrier of (BoolePoset ([#] L))
;
then
F c= bool ([#] L)
by WAYBEL_7:4;
then
C in bool ([#] L)
by TARSKI:def 3;
then A2:
( C \ (rng the mapping of ((a_net F) * p)) c= [#] L & C /\ (rng the mapping of ((a_net F) * p)) c= [#] L )
by XBOOLE_1:1;
then reconsider D = C \ (rng the mapping of ((a_net F) * p)), A = C /\ (rng the mapping of ((a_net F) * p)) as Element of (BoolePoset ([#] L)) by WAYBEL_7:4;
reconsider A' = A as Subset of L ;
A3:
F is prime
by WAYBEL_7:26;
A4: D "\/" A =
D \/ A
by YELLOW_1:17
.=
C
by XBOOLE_1:51
;
now assume A5:
D in F
;
:: thesis: contradictionconsider d being
Element of
D;
not
Bottom (BoolePoset ([#] L)) in F
by WAYBEL_7:8;
then A6:
D <> {}
by A5, YELLOW_1:18;
then
d in D
;
then reconsider d =
d as
Element of
L by A2;
reconsider D =
D as
Element of
F by A5;
[d,D] in { [a,f] where a is Element of L, f is Element of F : a in f }
by A6;
then reconsider dD =
[d,D] as
Element of
(a_net F) by YELLOW19:def 4;
reconsider dD' =
dD as
Element of
((a_net F) * p) by WAYBEL28:7;
ex
i being
Element of
((a_net F) * p) st
for
j being
Element of
((a_net F) * p) st
j >= i holds
g . j >= dD
then consider i being
Element of
((a_net F) * p) such that A11:
for
j being
Element of
((a_net F) * p) st
j >= i holds
g . j >= dD
;
RelStr(# the
carrier of
((a_net F) * p),the
InternalRel of
((a_net F) * p) #)
= RelStr(# the
carrier of
(a_net F),the
InternalRel of
(a_net F) #)
by WAYBEL28:def 2;
then
(a_net F) * p is
reflexive
by WAYBEL_8:12;
then
i >= i
by YELLOW_0:def 1;
then A12:
g . i >= dD
by A11;
reconsider G =
g . i as
Element of
(a_net F) ;
g . i in the
carrier of
(a_net F)
;
then
g . i in { [a,f] where a is Element of L, f is Element of F : a in f }
by YELLOW19:def 4;
then consider a being
Element of
L,
f being
Element of
F such that A13:
(
g . i = [a,f] &
a in f )
;
A14:
(
(g . i) `1 = a &
(g . i) `2 = f )
by A13, MCART_1:def 1, MCART_1:def 2;
(
(g . i) `2 = (p . i) `2 &
dD `2 = D )
by MCART_1:def 2;
then A15:
(
(p . i) `2 c= D &
(p . i) `1 in (p . i) `2 )
by A12, A13, A14, YELLOW19:def 4;
A16:
dom p = the
carrier of
(a_net F)
by FUNCT_2:67;
((a_net F) * p) . i =
(the mapping of (a_net F) * p) . i
by WAYBEL28:def 2
.=
(a_net F) . G
by A1, A16, FUNCT_1:23
.=
(p . i) `1
by YELLOW19:def 4
;
then
not
((a_net F) * p) . i in rng the
mapping of
((a_net F) * p)
by A15, XBOOLE_0:def 5;
hence
contradiction
by FUNCT_2:6;
:: thesis: verum end;
then A17:
( A c= rng the mapping of ((a_net F) * p) & A in F )
by A3, A4, WAYBEL_7:def 2, XBOOLE_1:17;
inf ((a_net F) * p) =
Inf
by WAYBEL_9:def 2
.=
"/\" (rng the mapping of ((a_net F) * p)),L
by YELLOW_2:def 6
;
then A18:
inf ((a_net F) * p) <= inf A'
by A17, WAYBEL_7:3;
set Y = { (inf B) where B is Subset of L : B in F } ;
A19:
inf A' in { (inf B) where B is Subset of L : B in F }
by A17;
ex_sup_of { (inf B) where B is Subset of L : B in F } ,L
by YELLOW_0:17;
then
inf A' <= lim_inf F
by A19, YELLOW_4:1;
hence
lim_inf F >= inf ((a_net F) * p)
by A18, YELLOW_0:def 2; :: thesis: verum