vectorSpan_image_eq_submodule_map

English

The image of a vectorSpan under an affine map equals the vectorSpan of the image set.

Русский

Образ векторSpan под аффинным отображением равен векторSpan образа множества.

LaTeX

$$$\\operatorname{Submodule.map} f.linear (\\operatorname{vectorSpan}_k s) = \\operatorname{vectorSpan}_k (f '' s)$$$

Lean4

@[simp]
theorem vectorSpan_image_eq_submodule_map {s : Set P₁} :
    Submodule.map f.linear (vectorSpan k s) = vectorSpan k (f '' s) := by simp [vectorSpan_def, f.image_vsub_image]

Похожие утверждения