---

Step * of Lemma m-retraction-subtype1

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

---

Latex:

---

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


By

---

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

---

Home Index