---

Step * of Lemma m-retraction_functionality

No Annotations
∀[X,Y:Type].
  ∀[A,B:Type].  ∀[d:metric(X)]. Retract(X ⟶ A) ≡ Retract(Y ⟶ B) supposing A ⊆r X supposing A ≡ B supposing X ≡ Y
BY
{ (Intros
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN D 6
   THEN RepeatFor 2 (D -1)
   THEN MemTypeCD
   THEN Auto
   THEN RepeatFor 2 (ParallelOp -2)
   THEN ParallelLast) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:Type].
    \mforall{}[A,B:Type].    \mforall{}[d:metric(X)].  Retract(X  {}\mrightarrow{}  A)  \mequiv{}  Retract(Y  {}\mrightarrow{}  B)  supposing  A  \msubseteq{}r  X  supposing  A  \mequiv{}  B 
    supposing  X  \mequiv{}  Y


By

---

Latex:
(Intros
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  D  6
  THEN  RepeatFor  2  (D  -1)
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  ParallelLast)

---

Home Index