image_span_subset — Mathlib

English

For a semilinear map f, a set s, and a submodule N, we have f''span(s) ⊆ N iff every generator maps into N.

Русский

Для полупрямой отображения f, множества s и подмодуля N, выполняется: образ-спан s ⊆ N тогда и только тогда, когда каждый элемент s образуется в N.

LaTeX

$$$ f''\operatorname{span}_R(s) \subseteq N \iff \forall m \in s, f(m) \in N $$$

Lean4

/-- A version of `Submodule.map_span_le` that does not require the `RingHomSurjective`
assumption. -/
theorem image_span_subset (f : F) (s : Set M) (N : Submodule R₂ M₂) : f '' span R s ⊆ N ↔ ∀ m ∈ s, f m ∈ N :=
  image_subset_iff.trans <| span_le (p := N.comap f)

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