Step
*
of Lemma
r-list-sum_wf
∀[L:ℝ List]. (r-list-sum(L) ∈ ℝ)
BY
{ ((Assert λx,y. (x + y) ∈ ℝ ⟶ ℝ ⟶ ℝ BY Auto) THEN ProveWfLemma) }
Latex:
Latex:
\mforall{}[L:\mBbbR{} List]. (r-list-sum(L) \mmember{} \mBbbR{})
By
Latex:
((Assert \mlambda{}x,y. (x + y) \mmember{} \mBbbR{} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{} BY Auto) THEN ProveWfLemma)
Home
Index