smul_mem_smul_set_iff — Mathlib

English

Let α be a group acting on β. For any a ∈ α, and any x ∈ β and subset s ⊆ β, membership of a • x in a • s is equivalent to membership of x in s; i.e., a bijectively transfers membership via the action.

Русский

Пусть α — группа, действует на β. Для любого a ∈ α и любого x ∈ β и подмножества s ⊆ β верно: x ∈ s ⇔ a•x ∈ a•s; то есть действие сохраняет принадлежность через биекцию, заданную действием.

LaTeX

$$$\forall a\in α, \forall x\in β, \forall S\subseteq β:\ a\cdot x \in a\cdot S \;\Leftrightarrow\; x\in S.$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_mem_smul_set_iff : a • x ∈ a • s ↔ x ∈ s :=
  (MulAction.injective _).mem_set_image

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