Step
*
of Lemma
cauchy-mlimit_wf
∀[X:Type]. ∀[d:metric(X)]. ∀[cmplt:mcomplete(X with d)]. ∀[x:ℕ ⟶ X]. ∀[c:mcauchy(d;n.x n)].
  (cauchy-mlimit(cmplt;x;c) ∈ X)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[cmplt:mcomplete(X  with  d)].  \mforall{}[x:\mBbbN{}  {}\mrightarrow{}  X].  \mforall{}[c:mcauchy(d;n.x  n)].
    (cauchy-mlimit(cmplt;x;c)  \mmember{}  X)
By
Latex:
ProveWfLemma
Home
Index