Nuprl Lemma : finite-type-iff-list

`∀[T:Type]. (finite-type(T) `⇐⇒` ∃L:T List. ∀x:T. (x ∈ L))`

Proof

Definitions occuring in Statement :  finite-type: `finite-type(T)` l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` rev_implies: `P `` Q` exists: `∃x:A. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` finite-type: `finite-type(T)` all: `∀x:A. B[x]` cardinality-le: `|T| ≤ n`
Lemmas referenced :  finite-type_wf exists_wf list_wf all_wf l_member_wf cardinality-le-list list-cardinality-le length_wf_nat cardinality-le_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productElimination sqequalRule lambdaEquality universeEquality dependent_functionElimination independent_functionElimination dependent_pairFormation

Latex:
\mforall{}[T:Type].  (finite-type(T)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L))

Date html generated: 2016_05_14-PM-01_52_08
Last ObjectModification: 2015_12_26-PM-05_38_03

Theory : list_1

Home Index