---

Step * of Lemma vs-map-into-subspace

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index