smul_mem_pointwise_smul_iff — Mathlib

English

Let a ∈ α and S a Submonoid of M. Then for any x ∈ M, x ∈ a · S iff x can be written as a · s for some s ∈ S.

Русский

Пусть a ∈ α и S — подмоноид в M. Тогда для любого x ∈ M выполняется: x ∈ a · S тогда и только тогда, когда x имеет вид a · s для некоторого s ∈ S.

LaTeX

$$$(\\forall a \\in α)(\\forall S \\subseteq M)(x \\in a \\cdot S \\;\\iff\\; x = a \\cdot s \\text{ для некоторого } s \\in S)$$$

Lean4

@[simp]
theorem smul_mem_pointwise_smul_iff {a : α} {S : Submonoid M} {x : M} : a • x ∈ a • S ↔ x ∈ S :=
  smul_mem_smul_set_iff

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