span_single_image — Mathlib

English

The span of the images of a set under the single map equals the image under the single-map linear transformation of the span of the set.

Русский

Движение образов множества через отображение single равно изображению линейного отображения через single от линейной оболочки множества.

LaTeX

$$$\operatorname{span}_R(\mathrm{single}(a)'' S) = \operatorname{map}(\mathrm{lsingle} a) (\operatorname{span}_R S)$$$

Lean4

theorem span_single_image (s : Set M) (a : α) :
    Submodule.span R (single a '' s) = (Submodule.span R s).map (lsingle a : M →ₗ[R] α →₀ M) := by rw [← span_image];
  rfl

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