---

Step * of Lemma vs-map-from-subspace

∀[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[P:Point(A) ⟶ ℙ].
  f ∈ (a:A | P[a]) ⟶ B supposing vs-subspace(K;A;a.P[a])
BY
{ Auto }

1
1. K : Rng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. f : A ⟶ B
5. P : Point(A) ⟶ ℙ
6. vs-subspace(K;A;a.P[a])
⊢ f ∈ (a:A | P[a]) ⟶ B

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[A,B:VectorSpace(K)].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[P:Point(A)  {}\mrightarrow{}  \mBbbP{}].
    f  \mmember{}  (a:A  |  P[a])  {}\mrightarrow{}  B  supposing  vs-subspace(K;A;a.P[a])


By

---

Latex:
Auto

---

Home Index