---

Step * 1 1 1 1 2 of Lemma m-closed-iff-complete


1. [X] : Type
2. d : metric(X)
3. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
4. [A] : Type
5. metric-subspace(X;d;A)
6. d ∈ metric(A)
7. x : ℕ ⟶ A
8. mcauchy(d;n.x n)
9. y : X
10. k : ℕ+
11. N : ℕ
12. [%11] : ∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x n;y) ≤ (r1/r(k))))
⊢ mdist(d;y;x N) ≤ (r1/r(k))
BY
{ ((Assert x N ∈ X BY Auto) THEN (Unhide THENA Auto) THEN RWO "mdist-symm" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  d  :  metric(X)
3.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
4.  [A]  :  Type
5.  metric-subspace(X;d;A)
6.  d  \mmember{}  metric(A)
7.  x  :  \mBbbN{}  {}\mrightarrow{}  A
8.  mcauchy(d;n.x  n)
9.  y  :  X
10.  k  :  \mBbbN{}\msupplus{}
11.  N  :  \mBbbN{}
12.  [\%11]  :  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(d;x  n;y)  \mleq{}  (r1/r(k))))
\mvdash{}  mdist(d;y;x  N)  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  x  N  \mmember{}  X  BY  Auto)  THEN  (Unhide  THENA  Auto)  THEN  RWO  "mdist-symm"  0  THEN  Auto)

---

Home Index