mem_smul_pointwise_iff_exists — Mathlib

English

Let S be a subgroup of G, a be a scalar from α, and m be an element of G. Then m lies in the image a · S if and only if there exists s in S with a · s = m.

Русский

Пусть S — подгруппа G, а — скаляр из α, и m — элемент G. Тогда m принадлежит изображению a · S тогда и только тогда, когда существует s ∈ S такое, что a · s = m.

LaTeX

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

Lean4

theorem mem_smul_pointwise_iff_exists (m : G) (a : α) (S : Subgroup G) : m ∈ a • S ↔ ∃ s : G, s ∈ S ∧ a • s = m :=
  (Set.mem_smul_set : m ∈ a • (S : Set G) ↔ _)

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