mem_smul_set_inv — Mathlib

English

For a group acting on β, for any A ⊆ β and a ∈ α, the membership relation x ∈ a • A is equivalent to a⁻¹ • x ∈ A, reflecting that smul by a is a bijection of β.

Русский

Для группы, действующей на β, для подмножества A и элемента a ∈ α верно: x ∈ a•A ⇔ a⁻¹•x ∈ A, поскольку отображение умножения на a является биекцией.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mem_smul_set_inv {s : Set α} : a ∈ b • s⁻¹ ↔ b ∈ a • s := by simp [mem_smul_set_iff_inv_smul_mem]

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