subsingleton_iff — Mathlib

English

Let S be a submonoid of R and g: M → M' a localized linear map. Then M' is subsingleton if and only if for every m ∈ M there exists r ∈ S with r • m = 0.

Русский

Пусть S — подмножество-подмоноид R, а g: M → M' локализовано. Тогда M' одноэлементный тогда и только тогда, когда для каждого m ∈ M существует r ∈ S such что r • m = 0.

LaTeX

$$$\operatorname{Subsingleton}(M') \iff \forall m:\, \exists r \in S,\ r \cdot m = 0$$$

Lean4

theorem subsingleton_iff (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g] :
    Subsingleton M' ↔ ∀ m : M, ∃ r ∈ S, r • m = 0 := by
  simp_rw [subsingleton_iff_ker_eq_top S g, ← top_le_iff, SetLike.le_def, mem_ker_iff S, Submodule.mem_top,
    true_implies]

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