### Nuprl Lemma : fpf-normalize-ap

`∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[g:x:A fp-> B[x]]. ∀[x:A].`
`  fpf-normalize(eq;g)(x) = g(x) ∈ B[x] supposing ↑x ∈ dom(g)`

Proof

Definitions occuring in Statement :  fpf-normalize: `fpf-normalize(eq;g)` fpf-ap: `f(x)` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T`
Lemmas :  list_ind_cons_lemma list_ind_nil_lemma fpf_ap_pair_lemma deq_member_cons_lemma deq_member_nil_lemma assert_wf fpf-dom_wf subtype-fpf2 top_wf subtype_top fpf_wf deq_wf nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf equal-wf-T-base colength_wf_list list_wf list-cases reduce_nil_lemma product_subtype_list spread_cons_lemma sq_stable__le le_antisymmetry_iff add_functionality_wrt_le add-associates add-zero zero-add le-add-cancel nat_wf decidable__le false_wf not-le-2 condition-implies-le minus-add minus-one-mul add-commutes le_wf subtract_wf not-ge-2 less-iff-le minus-minus add-swap subtype_base_sq set_subtype_base int_subtype_base reduce_cons_lemma list-subtype l_member_wf deq-member_wf set_wf subtype_rel_list bool_wf uiff_transitivity equal_wf eqtt_to_assert safe-assert-deq iff_transitivity bnot_wf not_wf iff_weakening_uiff eqff_to_assert assert_of_bnot cons_wf member_wf subtype_rel_self subtype_rel_wf assert-deq-member cons_member
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[g:x:A  fp->  B[x]].  \mforall{}[x:A].
fpf-normalize(eq;g)(x)  =  g(x)  supposing  \muparrow{}x  \mmember{}  dom(g)

Date html generated: 2015_07_17-AM-11_16_57
Last ObjectModification: 2015_01_28-AM-07_38_05

Home Index