let L be complete LATTICE; :: thesis: for F being proper Filter of (BoolePoset ([#] L))
for f being Subset of L st f in F holds
for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
let F be proper Filter of (BoolePoset ([#] L)); :: thesis: for f being Subset of L st f in F holds
for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
let f be Subset of L; :: thesis: ( f in F implies for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i) )
assume A1:
f in F
; :: thesis: for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
let i be Element of (a_net F); :: thesis: ( i `2 = f implies inf f = inf ((a_net F) | i) )
assume A2:
i `2 = f
; :: thesis: inf f = inf ((a_net F) | i)
A3: inf ((a_net F) | i) =
Inf
by WAYBEL_9:def 2
.=
"/\" (rng the mapping of ((a_net F) | i)),L
by YELLOW_2:def 6
;
for b being set st b in rng the mapping of ((a_net F) | i) holds
b in f
proof
let b be
set ;
:: thesis: ( b in rng the mapping of ((a_net F) | i) implies b in f )
assume
b in rng the
mapping of
((a_net F) | i)
;
:: thesis: b in f
then
b in { (((a_net F) | i) . k) where k is Element of the carrier of ((a_net F) | i) : verum }
by WAYBEL11:19;
then consider k being
Element of
((a_net F) | i) such that A4:
b = ((a_net F) | i) . k
;
A5:
the
carrier of
((a_net F) | i) c= the
carrier of
(a_net F)
by WAYBEL_9:13;
then A6:
k in the
carrier of
(a_net F)
by TARSKI:def 3;
reconsider l =
k as
Element of
(a_net F) by A5, TARSKI:def 3;
k in { [c,g] where c is Element of L, g is Element of F : c in g }
by A6, YELLOW19:def 4;
then consider c being
Element of
L,
g being
Element of
F such that A7:
(
k = [c,g] &
c in g )
;
A8:
(
k `1 = c &
k `2 = g )
by A7, MCART_1:def 1, MCART_1:def 2;
k in the
carrier of
((a_net F) | i)
;
then
k in { y where y is Element of (a_net F) : i <= y }
by WAYBEL_9:12;
then consider y being
Element of
(a_net F) such that A9:
(
k = y &
i <= y )
;
A10:
l `2 c= f
by A2, A9, YELLOW19:def 4;
reconsider k =
k as
Element of
((a_net F) | i) ;
(a_net F) . l = ((a_net F) | i) . k
by WAYBEL_9:16;
then
b = l `1
by A4, YELLOW19:def 4;
hence
b in f
by A7, A8, A10;
:: thesis: verum
end;
then A11:
rng the mapping of ((a_net F) | i) c= f
by TARSKI:def 3;
for b being set st b in f holds
b in rng the mapping of ((a_net F) | i)
then
f c= rng the mapping of ((a_net F) | i)
by TARSKI:def 3;
hence
inf f = inf ((a_net F) | i)
by A3, A11, XBOOLE_0:def 10; :: thesis: verum