---

Step * of Lemma mfun-strong-subtype

∀[X,Y:Type]. ∀[d:metric(X)]. ∀[d':metric(Y)]. ∀[A:Type].
  strong-subtype(FUN(X ⟶ A);FUN(X ⟶ Y)) supposing metric-subspace(Y;d';A)
BY
{ (Intros
   THEN D 0
   THEN (Unhide THENW Auto)
   THEN (D 6 THEN Auto)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN DVar `x'
   THEN DVar `a'
   THEN (EqTypeHD (-1) THENA Auto)
   THEN (MemTypeCD THENW Auto)
   THEN Try (ParallelLast)) }

1
1. X : Type
2. Y : Type
3. d : metric(X)
4. d' : metric(Y)
5. A : Type
6. strong-subtype(A;Y)
7. ∀a:A. ∀x:Y.  (x ≡ a ⇒ (x ∈ A))
8. FUN(X ⟶ A) ⊆r FUN(X ⟶ Y)
9. x : X ⟶ Y
10. x:FUN(X;Y)
11. a : X ⟶ A
12. a:FUN(X;A)
13. x = a ∈ (X ⟶ Y)
14. x:FUN(X;Y)
⊢ x ∈ X ⟶ A

---

Latex:

---

Latex:
\mforall{}[X,Y:Type].  \mforall{}[d:metric(X)].  \mforall{}[d':metric(Y)].  \mforall{}[A:Type].
    strong-subtype(FUN(X  {}\mrightarrow{}  A);FUN(X  {}\mrightarrow{}  Y))  supposing  metric-subspace(Y;d';A)


By

---

Latex:
(Intros
  THEN  D  0
  THEN  (Unhide  THENW  Auto)
  THEN  (D  6  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  DVar  `x'
  THEN  DVar  `a'
  THEN  (EqTypeHD  (-1)  THENA  Auto)
  THEN  (MemTypeCD  THENW  Auto)
  THEN  Try  (ParallelLast))

---

Home Index