mem_smul_set_iff_inv_smul_mem — Mathlib

English

If a group α acts on β, then for any a ∈ α and A ⊆ β we have x ∈ a • A if and only if a⁻¹ • x ∈ A; equivalently, a • x ∈ a • A ⇔ x ∈ A.

Русский

Пусть α действует на β. Тогда для любого a ∈ α и подмножества A ⊆ β: x ∈ a•A ⇔ a⁻¹•x ∈ A; то есть переносMembership через обратное действие сохраняется.

LaTeX

$$$\forall a\in α,\forall A\subseteq β:\ x\in a\cdot A \Leftrightarrow a^{-1}\cdot x\in A.$$$

Lean4

@[to_additive]
theorem mem_smul_set_iff_inv_smul_mem : x ∈ a • A ↔ a⁻¹ • x ∈ A :=
  show x ∈ MulAction.toPerm a '' A ↔ _ from mem_image_equiv

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