Nuprl Lemma : fpf-vals-nil

[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[P:A ─→ 𝔹]. ∀[f:x:A fp-> B[x]]. ∀[a:A].
  (fpf-vals(eq;P;f) []) supposing ((∀b:A. (↑(P b) ⇐⇒ a ∈ A)) and (¬↑a ∈ dom(f)))


Definitions occuring in Statement :  fpf-vals: fpf-vals(eq;P;f) fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] deq: EqDecider(T) nil: [] assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A apply: a function: x:A ─→ B[x] universe: Type sqequal: t equal: t ∈ T
Lemmas :  deq-member_wf equal-wf-T-base assert_wf l_member_wf bnot_wf not_wf cons_wf iff_transitivity iff_weakening_uiff eqtt_to_assert assert-deq-member eqff_to_assert assert_of_bnot equal_wf nil_wf bool_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 list_wf and_wf remove-repeats_wf remove-repeats-no_repeats remove-repeats_property zip_nil_lemma list-cases equal-wf-base product_subtype_list null_nil_lemma btrue_wf null_wf3 subtype_rel_list top_wf null_cons_lemma bfalse_wf btrue_neq_bfalse
\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)  \msim{}  [])  supposing  ((\mforall{}b:A.  (\muparrow{}(P  b)  \mLeftarrow{}{}\mRightarrow{}  b  =  a))  and  (\mneg{}\muparrow{}a  \mmember{}  dom(f)))

Date html generated: 2015_07_17-AM-11_10_12
Last ObjectModification: 2015_01_28-AM-07_47_06

Home Index