Step
*
1
of Lemma
vs-map-image-iff-surject
1. [K] : Rng
2. [A] : VectorSpace(K)
3. [B] : VectorSpace(K)
4. [f] : A ⟶ B
5. Surj(Point(A);Point(B);f)
6. b : Point(B)
⊢ b ∈ Img(f)
BY
{ (D -2 With ⌜b⌝  THEN Auto) }
Latex:
Latex:
1.  [K]  :  Rng
2.  [A]  :  VectorSpace(K)
3.  [B]  :  VectorSpace(K)
4.  [f]  :  A  {}\mrightarrow{}  B
5.  Surj(Point(A);Point(B);f)
6.  b  :  Point(B)
\mvdash{}  b  \mmember{}  Img(f)
By
Latex:
(D  -2  With  \mkleeneopen{}b\mkleeneclose{}    THEN  Auto)
Home
Index