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