Nuprl Lemma : fpf-as-apply-alist
∀[A,B:Type]. ∀[f:a:A fp-> B]. ∀[eq:EqDecider(A)].
(f = <fpf-domain(f), λx.outl(apply-alist(eq;map(λx.<x, f(x)>;fpf-domain(f));x))> ∈ a:A fp-> B)
Proof
Definitions occuring in Statement :
fpf-ap: f(x),
fpf-domain: fpf-domain(f),
fpf: a:A fp-> B[a],
apply-alist: apply-alist(eq;L;x),
deq: EqDecider(T),
map: map(f;as),
outl: outl(x),
uall: ∀[x:A]. B[x],
lambda: λx.A[x],
pair: <a, b>,
universe: Type,
equal: s = t ∈ T
Lemmas :
map_wf,
l_member_wf,
list-subtype,
set_wf,
deq_wf,
fpf_wf,
apply-alist-cases,
subtype_rel_list,
top_wf,
subtype_rel_product,
alist-domain-first,
map-length,
lelt_wf,
length_wf,
map_select,
select_wf,
sq_stable__le,
and_wf,
equal_wf,
pi1_wf_top,
pi2_wf
\mforall{}[A,B:Type]. \mforall{}[f:a:A fp-> B]. \mforall{}[eq:EqDecider(A)].
(f = <fpf-domain(f), \mlambda{}x.outl(apply-alist(eq;map(\mlambda{}x.<x, f(x)>fpf-domain(f));x))>)
Date html generated:
2015_07_17-AM-09_16_36
Last ObjectModification:
2015_01_28-AM-07_53_40
Home
Index