apply_mem_span_image_of_mem_span — Mathlib

English

If x ∈ span_R s, then f x ∈ span_{R₂}(f''s).

Русский

Если x ∈ span_R s, то f x ∈ span_{R₂}(f''s).

LaTeX

$$$$ x \\in \\operatorname{span}_R s \\;\\Rightarrow\\; f(x) \\in \\operatorname{span}_{R_2}(f''s). $$$$

Lean4

theorem apply_mem_span_image_of_mem_span [RingHomSurjective σ₁₂] (f : F) {x : M} {s : Set M}
    (h : x ∈ Submodule.span R s) : f x ∈ Submodule.span R₂ (f '' s) :=
  by
  rw [Submodule.span_image]
  exact Submodule.mem_map_of_mem h

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