span_preimage_le — Mathlib

English

A variation of the previous span-leq lemma without requiring surjectivity; the equivalence of span inclusion is characterized by pointwise membership on generators.

Русский

Без предположения про суръективность, эквивалентность включения спана определяется по образам базисных элементов.

LaTeX

$$$ (\operatorname{span}_R(s))\!\!{\map} f \le N \iff \forall m\in s, f(m) \in N $$$

Lean4

/-- See also `Submodule.span_preimage_eq`. -/
theorem span_preimage_le (f : F) (s : Set M₂) : span R (f ⁻¹' s) ≤ (span R₂ s).comap f :=
  by
  rw [span_le, comap_coe]
  exact preimage_mono subset_span

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