Nuprl Lemma : fpf-restrict_wf
[A:Type]. [B:A 
Type]. [f:x:A fp-> B[x]]. [P:A 
]. (fpf-restrict(f;P) 
x:{x:A| 
(P x)} fp-> B[x])
Proof not projected
Definitions occuring in Statement :
fpf-restrict: fpf-restrict(f;P),
fpf: a:A fp-> B[a],
assert: b,
bool: ,
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
universe: Type
Definitions :
so_lambda: 
x.t[x],
pi1: fst(t),
pi2: snd(t),
fpf-domain: fpf-domain(f),
mk_fpf: mk_fpf(L;f),
fpf-restrict: fpf-restrict(f;P),
member: t T,
so_apply: x[s],
fpf: a:A fp-> B[a],
uall: [x:A]. B[x],
prop: 
,
all: x:A. B[x],
uimplies: b supposing a,
implies: P 
Q,
and: P 
Q,
iff: P 
Q
Lemmas :
fpf_wf,
bool_wf,
l_member_wf,
assert_wf,
filter_type,
subtype_rel_self,
subtype_rel_dep_function,
l_member-settype,
member_filter
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[f:x:A fp-> B[x]]. \mforall{}[P:A {}\mrightarrow{} \mBbbB{}].
(fpf-restrict(f;P) \mmember{} x:\{x:A| \muparrow{}(P x)\} fp-> B[x])
Date html generated:
2012_01_23-AM-11_55_59
Last ObjectModification:
2011_12_10-PM-12_50_09
Home
Index