### Nuprl Lemma : lsum_wf

`∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)}  ⟶ ℤ].  (Σ(f[x] | x ∈ L) ∈ ℤ)`

Proof

Definitions occuring in Statement :  lsum: `Σ(f[x] | x ∈ L)` l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` lsum: `Σ(f[x] | x ∈ L)` member: `t ∈ T` prop: `ℙ` so_apply: `x[s]`
Lemmas referenced :  list-subtype l_sum_wf map_wf l_member_wf istype-int list_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setEquality intEquality lambdaEquality_alt applyEquality setIsType universeIsType functionIsType instantiate universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}(f[x]  |  x  \mmember{}  L)  \mmember{}  \mBbbZ{})

Date html generated: 2020_05_19-PM-09_46_35
Last ObjectModification: 2019_11_12-PM-11_12_32

Theory : list_1

Home Index