Nuprl Lemma : fpf-restrict_wf2
[A:Type]. [B:A 
Type]. [f:x:A fp-> B[x]]. [P:A 
]. (fpf-restrict(f;P) 
x:A fp-> B[x])
Proof not projected
Definitions occuring in Statement :
fpf-restrict: fpf-restrict(f;P),
fpf: a:A fp-> B[a],
bool: ,
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
fpf-domain: fpf-domain(f),
mk_fpf: mk_fpf(L;f),
fpf-restrict: fpf-restrict(f;P),
fpf: a:A fp-> B[a],
implies: P 
Q,
prop: 
,
so_lambda: 
x.t[x],
all: x:A. B[x],
pi2: snd(t),
pi1: fst(t),
member: t T,
so_apply: x[s],
uall: [x:A]. B[x],
uimplies: b supposing a,
iff: P 
Q,
and: P 
Q
Lemmas :
bool_wf,
subtype_rel_self,
subtype_rel_sets,
l_member_wf,
subtype_rel_dep_function,
filter_wf,
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:A fp-> B[x])
Date html generated:
2012_01_23-AM-11_56_03
Last ObjectModification:
2011_12_12-PM-06_57_11
Home
Index