### Nuprl Lemma : assert-fpf-is-empty

`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:x:A fp-> B[x]].  uiff(↑fpf-is-empty(f);f = ⊗ ∈ x:A fp-> B[x])`

Proof

Definitions occuring in Statement :  fpf-is-empty: `fpf-is-empty(f)` fpf-empty: `⊗` fpf: `a:A fp-> B[a]` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  fpf: `a:A fp-> B[a]` fpf-is-empty: `fpf-is-empty(f)` pi1: `fst(t)` fpf-empty: `⊗` member: `t ∈ T` uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` uimplies: `b supposing a` squash: `↓T` prop: `ℙ` so_apply: `x[s]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` top: `Top` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` not: `¬A` false: `False`
Lemmas referenced :  eq_int_wf length_wf assert_of_eq_int equal_wf squash_wf true_wf length_of_null_list nil_wf and_wf list_wf l_member_wf pi1_wf_top subtype_rel_product top_wf iff_weakening_equal assert_wf assert_witness equal-wf-T-base fpf_wf length_zero null_nil_lemma btrue_wf member-implies-null-eq-bfalse null_wf3 subtype_rel_list btrue_neq_bfalse set_wf
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin sqequalRule cut introduction extract_by_obid isectElimination cumulativity hypothesisEquality hypothesis natural_numberEquality independent_isectElimination applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry because_Cache intEquality dependent_set_memberEquality independent_pairFormation productEquality functionEquality setEquality setElimination rename applyLambdaEquality functionExtensionality lambdaFormation isect_memberEquality voidElimination voidEquality imageMemberEquality baseClosed universeEquality independent_functionElimination isect_memberFormation independent_pairEquality axiomEquality dependent_pairEquality

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:x:A  fp->  B[x]].    uiff(\muparrow{}fpf-is-empty(f);f  =  \motimes{})

Date html generated: 2018_05_21-PM-09_17_43
Last ObjectModification: 2018_02_09-AM-10_16_42

Theory : finite!partial!functions

Home Index