span_singleton_le_iff_mem — Mathlib

English

For any m ∈ M, (R ∙ m) ≤ p iff m ∈ p; equivalently, membership in a span generated by a singleton is determined by membership of the generator.

Русский

Для данного m ∈ M, (R∙m) ≤ p тогда и только тогда, что m ∈ p; то есть принадлежность к оболочке, порожденной единичной подпостановкой, определяется принадлежностью порождающего элемента.

LaTeX

$$$ (R \cdot m) \le p \iff m \in p $$$

Lean4

@[simp]
theorem span_singleton_le_iff_mem (m : M) (p : Submodule R M) : (R ∙ m) ≤ p ↔ m ∈ p := by
  rw [span_le, singleton_subset_iff, SetLike.mem_coe]

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