---

Step * of Lemma fs-in-subtype-subspace

∀[K:CRng]. ∀[S,T:Type].  vs-subspace(K;free-vs(K;S);f.fs-in-subtype(K;S;T;f)) supposing strong-subtype(T;S)
BY
{ (Auto
   THEN DupHyp 4
   THEN (RWO "strong-subtype-iff-respects-equality" (-1) THENA Auto)
   THEN InstLemma `equal-wf` [⌜S⌝;⌜S⌝;⌜T⌝]⋅
   THEN Auto
   THEN D 0
   THEN Auto) }

1
1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. T ⊆r S
6. respects-equality(S;T)
7. ∀[a,b:S].  (a = b ∈ T ∈ ℙ)
⊢ fs-in-subtype(K;S;T;0)

2
1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. T ⊆r S
6. respects-equality(S;T)
7. ∀[a,b:S].  (a = b ∈ T ∈ ℙ)
8. f : Point(free-vs(K;S))
9. y : Point(free-vs(K;S))
10. fs-in-subtype(K;S;T;f)
11. fs-in-subtype(K;S;T;y)
⊢ fs-in-subtype(K;S;T;f + y)

3
1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. T ⊆r S
6. respects-equality(S;T)
7. ∀[a,b:S].  (a = b ∈ T ∈ ℙ)
8. ∀f,y:Point(free-vs(K;S)).  (fs-in-subtype(K;S;T;f) ⇒ fs-in-subtype(K;S;T;y) ⇒ fs-in-subtype(K;S;T;f + y))
9. f : Point(free-vs(K;S))
10. a : |K|
11. fs-in-subtype(K;S;T;f)
⊢ fs-in-subtype(K;S;T;a * f)

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[S,T:Type].
    vs-subspace(K;free-vs(K;S);f.fs-in-subtype(K;S;T;f))  supposing  strong-subtype(T;S)


By

---

Latex:
(Auto
  THEN  DupHyp  4
  THEN  (RWO  "strong-subtype-iff-respects-equality"  (-1)  THENA  Auto)
  THEN  InstLemma  `equal-wf`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index