mem_stabilizer_iff — Mathlib

English

Let G act on α. The stabilizer of a ∈ α consists of those g ∈ G with g • a = a. Equivalently, g ∈ Stab_G(a) if and only if g • a = a.

Русский

Пусть G действует на α. Stabilizer точки a ∈ α состоит из таких элементов g ∈ G, что g • a = a. Эквивалентно: g ∈ Stab_G(a) тогда и только тогда, когда g • a = a.

LaTeX

$$$g \in \operatorname{Stab}_G(a) \iff g \cdot a = a$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_stabilizer_iff {a : α} {g : G} : g ∈ stabilizer G a ↔ g • a = a :=
  Iff.rfl

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