map_span_le — Mathlib

English

For a map f and a set s, span of preimage of s via f is contained in the comap of span of s by f.

Русский

Спан прообраза множества через f содержится в обратном образе спана через f.

LaTeX

$$$\operatorname{span}_R(f^{-1}(s)) \le (\operatorname{span}_{R'}(s)).{\!}\!{\text{comap}} f$$$

Lean4

theorem map_span_le [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) :
    map f (span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N :=
  image_span_subset f s N

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