---

Step * of Lemma mfun-class-strong-subtype

∀[X,Y:Type]. ∀[d:metric(X)]. ∀[d':metric(Y)]. ∀[A:Type].
  strong-subtype(mfun-class(X;d;A;d');mfun-class(X;d;Y;d')) supposing metric-subspace(Y;d';A)
BY
{ (Intros
   THEN D 0
   THEN (Unhide THENW Auto)
   THEN D 6
   THEN ((D 0 THENA Auto) ORELSE Auto)
   THEN D -1
   THEN Try ((EqTypeCD THEN Auto))
   THEN ExRepD) }

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. mfun-class(X;d;A;d') ⊆r mfun-class(X;d;Y;d')
9. x : mfun-class(X;d;Y;d')
10. a : mfun-class(X;d;A;d')
11. x = a ∈ mfun-class(X;d;Y;d')
⊢ x ∈ mfun-class(X;d;A;d')

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  D  0
  THEN  (Unhide  THENW  Auto)
  THEN  D  6
  THEN  ((D  0  THENA  Auto)  ORELSE  Auto)
  THEN  D  -1
  THEN  Try  ((EqTypeCD  THEN  Auto))
  THEN  ExRepD)

---

Home Index