---

Step * of Lemma metric-strong-extensionality

∀[X:Type]
  ∀d:metric(X)
    (mcomplete(X with d)
    ⇒ (∀Y:Type. ∀d':metric(Y). ∀f:X ⟶ Y.
          ((∀x1,x2:X.  (x1 ≡ x2 ⇒ f[x1] ≡ f[x2])) ⇒ (∀x1,x2:X.  (f[x1] # f[x2] ⇒ x1 # x2)))))
BY
{ (InstLemma `metric-weak-Markov` [] THEN RepeatFor 3 (ParallelLast') THEN Auto THEN BackThruSomeHyp THEN Auto) }

1
1. [X] : Type
2. d : metric(X)
3. mcomplete(X with d)
4. ∀x,y:X.  ((∀z:X. ((¬z ≡ x) ∨ (¬z ≡ y))) ⇒ x # y)
5. Y : Type
6. d' : metric(Y)
7. f : X ⟶ Y
8. ∀x1,x2:X.  (x1 ≡ x2 ⇒ f[x1] ≡ f[x2])
9. x1 : X
10. x2 : X
11. f[x1] # f[x2]
12. z : X
⊢ (¬z ≡ x1) ∨ (¬z ≡ x2)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X)
        (mcomplete(X  with  d)
        {}\mRightarrow{}  (\mforall{}Y:Type.  \mforall{}d':metric(Y).  \mforall{}f:X  {}\mrightarrow{}  Y.
                    ((\mforall{}x1,x2:X.    (x1  \mequiv{}  x2  {}\mRightarrow{}  f[x1]  \mequiv{}  f[x2]))  {}\mRightarrow{}  (\mforall{}x1,x2:X.    (f[x1]  \#  f[x2]  {}\mRightarrow{}  x1  \#  x2)))))


By

---

Latex:
(InstLemma  `metric-weak-Markov`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index