Step
*
of Lemma
rminus_wf
∀[x:ℝ]. (-(x) ∈ ℝ)
BY
{ (ProveWfLemma THEN D 1 THEN MemTypeCD THEN Auto) }
1
.....set predicate.....
1. x : ℕ+ ⟶ ℤ
2. regular-seq(x)
⊢ regular-seq(λn.(-(x n)))
Latex:
Latex:
\mforall{}[x:\mBbbR{}]. (-(x) \mmember{} \mBbbR{})
By
Latex:
(ProveWfLemma THEN D 1 THEN MemTypeCD THEN Auto)
Home
Index