Nuprl Lemma : fpf-vals-singleton

[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[P:A ⟶ 𝔹]. ∀[f:x:A fp-> B[x]]. ∀[a:A].
  (fpf-vals(eq;P;f) [<a, f(a)>] ∈ ((x:A × B[x]) List)) supposing ((∀b:A. (↑(P b) ⇐⇒ a ∈ A)) and (↑a ∈ dom(f)))


Definitions occuring in Statement :  fpf-vals: fpf-vals(eq;P;f) fpf-ap: f(x) fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] cons: [a b] nil: [] list: List deq: EqDecider(T) assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q apply: a function: x:A ⟶ B[x] pair: <a, b> product: x:A × B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  fpf-vals: fpf-vals(eq;P;f) let: let fpf: a:A fp-> B[a] pi1: fst(t) pi2: snd(t) all: x:A. B[x] member: t ∈ T top: Top uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B uimplies: supposing a prop: and: P ∧ Q cand: c∧ B iff: ⇐⇒ Q rev_implies:  Q implies:  Q fpf-dom: x ∈ dom(f) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff not: ¬A false: False uiff: uiff(P;Q) exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b nat: ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) cons: [a b] colength: colength(L) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] decidable: Dec(P) nil: [] less_than: a < b squash: T less_than': less_than'(a;b)
Lemmas referenced :  fpf_ap_pair_lemma all_wf iff_wf assert_wf equal_wf fpf-dom_wf subtype-fpf2 top_wf fpf_wf bool_wf deq_wf remove-repeats_property assert-deq-member deq-member_wf equal-wf-T-base l_member_wf bnot_wf not_wf cons_wf nil_wf iff_transitivity iff_weakening_uiff eqtt_to_assert eqff_to_assert assert_of_bnot list_wf nil_member false_wf filter_nil_lemma no_repeats_wf cons_member filter_cons_lemma no_repeats_cons uiff_transitivity or_wf list_induction filter_wf5 subtype_rel_dep_function subtype_rel_self set_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot and_wf remove-repeats_wf bool_cases nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf nat_wf colength_wf_list less_than_transitivity1 less_than_irreflexivity list-cases equal-wf-base-T product_subtype_list spread_cons_lemma intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma decidable__le intformnot_wf int_formula_prop_not_lemma le_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma set_subtype_base int_subtype_base decidable__equal_int reduce_hd_cons_lemma hd_wf squash_wf length_wf length_cons_ge_one subtype_rel_list null_nil_lemma btrue_wf reduce_tl_cons_lemma tl_wf null_wf3 null_cons_lemma bfalse_wf btrue_neq_bfalse map_cons_lemma map_nil_lemma zip_cons_cons_lemma zip_nil_lemma member-remove-repeats
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalHypSubstitution productElimination thin sqequalRule cut introduction extract_by_obid dependent_functionElimination isect_memberEquality voidElimination voidEquality hypothesis isectElimination cumulativity hypothesisEquality lambdaEquality applyEquality functionExtensionality because_Cache independent_isectElimination lambdaFormation functionEquality universeEquality isect_memberFormation axiomEquality equalityTransitivity equalitySymmetry independent_functionElimination independent_pairFormation hyp_replacement applyLambdaEquality baseClosed unionElimination equalityElimination impliesFunctionality promote_hyp setEquality setElimination rename dependent_pairFormation instantiate dependent_set_memberEquality inrFormation inlFormation intWeakElimination natural_numberEquality int_eqEquality intEquality computeAll hypothesis_subsumption addEquality imageElimination imageMemberEquality productEquality dependent_pairEquality

\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:x:A  fp->  B[x]].  \mforall{}[a:A].
    (fpf-vals(eq;P;f)  =  [<a,  f(a)>])  supposing  ((\mforall{}b:A.  (\muparrow{}(P  b)  \mLeftarrow{}{}\mRightarrow{}  b  =  a))  and  (\muparrow{}a  \mmember{}  dom(f)))

Date html generated: 2018_05_21-PM-09_26_08
Last ObjectModification: 2018_02_09-AM-10_21_37

Theory : finite!partial!functions

Home Index