{
[f,P:Top].
(fpf-domain(fpf-restrict(f;P))
~
filter(P;fpf-domain(f)))
}
{
Proof
}
Definitions occuring in Statement
:
fpf-restrict:
fpf-restrict(f;P)
,
fpf-domain:
fpf-domain(f)
,
uall:
[x:A].
B[x]
,
top:
Top
,
sqequal:
s
~
t
,
filter:
filter(P;l)
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
Lemmas
:
top_wf
\mforall{}[f,P:Top]. (fpf-domain(fpf-restrict(f;P)) \msim{} filter(P;fpf-domain(f)))
Date html generated: 2011_08_10-AM-08_09_37
Last ObjectModification: 2011_06_18-AM-08_25_54
Home
Index
[x:A]. B[x], [f,P:Top]. (fpf-domain(fpf-restrict(f;P)) ~ filter(P;fpf-domain(f))) }[x:A]. B[x], [x:A]. B[x], 
T