English
Let R act on M and let N be a subset of M that is closed under this action. Then, for any x in M, x belongs to N if and only if a·x belongs to N for every a in R.
Русский
Пусть R действует на M и N ⊆ M замкнуется относительно этого действия. Тогда для любого x ∈ M верно: x ∈ N тогда и только тогда, когда для всех a ∈ R имеется a·x ∈ N.
LaTeX
$$$\\forall R M S [Monoid R] [MulAction R M] [SetLike S M] [SMulMemClass S R M] \\forall {N : S} \\forall {x : M}, (\\forall a : R, a \\cdot x \\in N) \\leftrightarrow x \\in N$$$
Lean4
@[simp]
theorem forall_smul_mem_iff {R M S : Type*} [Monoid R] [MulAction R M] [SetLike S M] [SMulMemClass S R M] {N : S}
{x : M} : (∀ a : R, a • x ∈ N) ↔ x ∈ N :=
⟨fun h => by simpa using h 1, fun h a => SMulMemClass.smul_mem a h⟩
