### Nuprl Lemma : mkfpf_wf

`∀[A:Type]. ∀[a:A List]. ∀[b:a:{a@0:A| (a@0 ∈ a)}  ⟶ Top].  (mkfpf(a;b) ∈ a:A fp-> Top)`

Proof

Definitions occuring in Statement :  mkfpf: `mkfpf(a;b)` fpf: `a:A fp-> B[a]` l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` top: `Top` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  mkfpf: `mkfpf(a;b)` fpf: `a:A fp-> B[a]` uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ`
Lemmas referenced :  l_member_wf top_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut dependent_pairEquality hypothesisEquality functionEquality setEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[a:A  List].  \mforall{}[b:a:\{a@0:A|  (a@0  \mmember{}  a)\}    {}\mrightarrow{}  Top].    (mkfpf(a;b)  \mmember{}  a:A  fp->  Top)

Date html generated: 2018_05_21-PM-09_28_08
Last ObjectModification: 2018_02_09-AM-10_23_34

Theory : finite!partial!functions

Home Index