---

Step * of Lemma m-retraction-subtype2

No Annotations
∀[X,A,B:Type].  ∀[d:metric(X)]. Retract(X ⟶ A) ⊆r Retract(X ⟶ B) supposing B ⊆r X supposing A ≡ B
BY
{ (InstLemma `m-retraction_functionality` []
   THEN ParallelLast'
   THEN (D -1 With ⌜X⌝  THENA Auto)
   THEN (D -1 THENA (D 0 THEN Auto))
   THEN RepeatFor 5 (ParallelLast')) }

1
.....antecedent..... 
1. X : Type
2. A : Type
3. B : Type
4. A ≡ B
5. d : metric(X)
6. B ⊆r X
⊢ A ⊆r X

2
1. X : Type
2. A : Type
3. B : Type
4. A ≡ B
5. d : metric(X)
6. B ⊆r X
7. Retract(X ⟶ A) ≡ Retract(X ⟶ B)
⊢ Retract(X ⟶ A) ⊆r Retract(X ⟶ B)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `m-retraction\_functionality`  []
  THEN  ParallelLast'
  THEN  (D  -1  With  \mkleeneopen{}X\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  THENA  (D  0  THEN  Auto))
  THEN  RepeatFor  5  (ParallelLast'))

---

Home Index