### Nuprl Lemma : finite-type-list

`∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) `` (∀L:T List. finite-type({x:T| (x ∈ L)} )))`

Proof

Definitions occuring in Statement :  finite-type: `finite-type(T)` l_member: `(x ∈ l)` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  cardinality-le-finite l_member_wf length_wf_nat list_wf all_wf decidable_wf equal_wf cardinality-le-list-set
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesisEquality hypothesis dependent_functionElimination independent_functionElimination sqequalRule lambdaEquality universeEquality

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}L:T  List.  finite-type(\{x:T|  (x  \mmember{}  L)\}  )))

Date html generated: 2016_05_14-PM-03_31_44
Last ObjectModification: 2015_12_26-PM-06_01_41

Theory : decidable!equality

Home Index