---

Step * 1 of Lemma metric-strong-extensionality


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)
BY
{ ((InstLemma `msep-or` [⌜Y⌝;⌜d'⌝;⌜f[x1]⌝;⌜f[x2]⌝;⌜f[z]⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN (D 0 THENA Auto)
   THEN FHyp 8 [-1]
   THEN Auto
   THEN Unfold `msep` -3
   THEN Unfold `meq` -1
   THEN Fold `mdist` (-1)
   THEN Auto
   THEN RWO "mdist-symm" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  d  :  metric(X)
3.  mcomplete(X  with  d)
4.  \mforall{}x,y:X.    ((\mforall{}z:X.  ((\mneg{}z  \mequiv{}  x)  \mvee{}  (\mneg{}z  \mequiv{}  y)))  {}\mRightarrow{}  x  \#  y)
5.  Y  :  Type
6.  d'  :  metric(Y)
7.  f  :  X  {}\mrightarrow{}  Y
8.  \mforall{}x1,x2:X.    (x1  \mequiv{}  x2  {}\mRightarrow{}  f[x1]  \mequiv{}  f[x2])
9.  x1  :  X
10.  x2  :  X
11.  f[x1]  \#  f[x2]
12.  z  :  X
\mvdash{}  (\mneg{}z  \mequiv{}  x1)  \mvee{}  (\mneg{}z  \mequiv{}  x2)


By

---

Latex:
((InstLemma  `msep-or`  [\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f[x1]\mkleeneclose{};\mkleeneopen{}f[x2]\mkleeneclose{};\mkleeneopen{}f[z]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  (D  0  THENA  Auto)
  THEN  FHyp  8  [-1]
  THEN  Auto
  THEN  Unfold  `msep`  -3
  THEN  Unfold  `meq`  -1
  THEN  Fold  `mdist`  (-1)
  THEN  Auto
  THEN  RWO  "mdist-symm"  (-1)
  THEN  Auto)

---

Home Index