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