### Nuprl Lemma : fpf-join-list-ap2

`∀[A:Type]`
`  ∀eq:EqDecider(A)`
`    ∀[B:A ⟶ Type]`
`      ∀L:a:A fp-> B[a] List. ∀x:A.  ((x ∈ fpf-domain(⊕(L))) `` (∃f∈L. (↑x ∈ dom(f)) ∧ (⊕(L)(x) = f(x) ∈ B[x])))`

Proof

Definitions occuring in Statement :  fpf-join-list: `⊕(L)` fpf-ap: `f(x)` fpf-domain: `fpf-domain(f)` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` l_exists: `(∃x∈L. P[x])` l_member: `(x ∈ l)` list: `T List` deq: `EqDecider(T)` assert: `↑b` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` uimplies: `b supposing a` subtype_rel: `A ⊆r B` top: `Top` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  fpf-join-list-ap list_wf fpf_wf deq_wf l_member_wf fpf-domain_wf fpf-join-list_wf top_wf subtype_rel_list subtype-fpf2 member-fpf-domain
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation dependent_functionElimination sqequalRule lambdaEquality applyEquality functionEquality cumulativity universeEquality independent_isectElimination because_Cache isect_memberEquality voidElimination voidEquality productElimination independent_functionElimination

Latex:
\mforall{}[A:Type]
\mforall{}eq:EqDecider(A)
\mforall{}[B:A  {}\mrightarrow{}  Type]
\mforall{}L:a:A  fp->  B[a]  List.  \mforall{}x:A.
((x  \mmember{}  fpf-domain(\moplus{}(L)))  {}\mRightarrow{}  (\mexists{}f\mmember{}L.  (\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\moplus{}(L)(x)  =  f(x))))

Date html generated: 2018_05_21-PM-09_22_59
Last ObjectModification: 2018_02_09-AM-10_19_02

Theory : finite!partial!functions

Home Index