### Nuprl Lemma : finite-fun-deq_wf

`∀[T:Type]. ∀[k:ℕ]. ∀[eq:EqDecider(T)].  (finite-fun-deq(k;eq) ∈ EqDecider(ℕk ⟶ T))`

Proof

Definitions occuring in Statement :  finite-fun-deq: `finite-fun-deq(k;eq)` deq: `EqDecider(T)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` finite-fun-deq: `finite-fun-deq(k;eq)` deq: `EqDecider(T)` so_lambda: `λ2x.t[x]` nat: `ℕ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` eqof: `eqof(d)` rev_implies: `P `` Q` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` uimplies: `b supposing a`
Lemmas referenced :  bdd-all_wf int_seg_wf istype-assert deq_wf istype-nat istype-universe assert-bdd-all eqof_wf safe-assert-deq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut dependent_set_memberEquality_alt lambdaEquality_alt extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule applyEquality setElimination rename hypothesis universeIsType natural_numberEquality inhabitedIsType functionIsType lambdaFormation_alt independent_pairFormation equalityIstype because_Cache productIsType axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality_alt isectIsTypeImplies instantiate universeEquality dependent_functionElimination productElimination independent_functionElimination independent_isectElimination applyLambdaEquality functionExtensionality

Latex:
\mforall{}[T:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[eq:EqDecider(T)].    (finite-fun-deq(k;eq)  \mmember{}  EqDecider(\mBbbN{}k  {}\mrightarrow{}  T))

Date html generated: 2020_05_19-PM-09_36_35
Last ObjectModification: 2019_10_18-AM-11_58_52

Theory : equality!deciders

Home Index