le_span_singleton_iff — Mathlib

English

For any submodule s and v0 ∈ M, s ≤ R ∙ v0 iff ∀ v ∈ s, ∃ r ∈ R with r • v0 = v.

Русский

Для подмодуля s и вектора v0 ∈ M верно: s ≤ R ∙ v0 тогда и только тогда, когда ∀ v ∈ s существует r ∈ R такое, что r • v0 = v.

LaTeX

$$$$ s \\le R \\cdot v_0 \\iff \\forall v \\in s, \\exists r \\in R, r \\cdot v_0 = v. $$$$

Lean4

theorem le_span_singleton_iff {s : Submodule R M} {v₀ : M} : (s ≤ R ∙ v₀) ↔ ∀ v ∈ s, ∃ r : R, r • v₀ = v := by
  simp_rw [SetLike.le_def, mem_span_singleton]

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