mem_smul_pointwise_iff_exists — Mathlib

English

For any a ∈ A, m ∈ M, S a-subset, x ∈ m • S iff ∃ s ∈ S with m • s = a.

Русский

Для любого a ∈ A, m ∈ M, существует s ∈ S такое, что m • s = a тогда и только тогда a ∈ m • S.

LaTeX

$$$ a \in m \cdot S \iff \exists s \in S,\; m \cdot s = a $$$

Lean4

theorem mem_smul_pointwise_iff_exists (a : A) (m : M) (S : AddSubmonoid A) : a ∈ m • S ↔ ∃ s : A, s ∈ S ∧ m • s = a :=
  (Set.mem_smul_set : a ∈ m • (S : Set A) ↔ _)

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