Nuprl Lemma : fpf-ap-equal

[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[x:A]. ∀[v:B[x]].
  (f(x) v ∈ B[x]) supposing ((↑x ∈ dom(f)) and || v)


Definitions occuring in Statement :  fpf-single: v fpf-compatible: || g fpf-ap: f(x) fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] deq: EqDecider(T) assert: b uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a fpf-compatible: || g all: x:A. B[x] top: Top implies:  Q and: P ∧ Q cand: c∧ B uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  fpf_ap_single_lemma fpf-single-dom assert_wf fpf-dom_wf subtype-fpf2 top_wf fpf-compatible_wf fpf-single_wf fpf_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution sqequalRule lemma_by_obid dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis hypothesisEquality independent_functionElimination independent_pairFormation isectElimination because_Cache productElimination independent_isectElimination applyEquality lambdaEquality lambdaFormation axiomEquality equalityTransitivity equalitySymmetry instantiate functionEquality cumulativity universeEquality

\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[x:A].  \mforall{}[v:B[x]].
    (f(x)  =  v)  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  f  ||  x  :  v)

Date html generated: 2018_05_21-PM-09_29_46
Last ObjectModification: 2018_02_09-AM-10_24_27

Theory : finite!partial!functions

Home Index