mem_stabilizer_set' — Mathlib

English

Let G act on α and s ⊆ α be finite. Then a ∈ stabilizer G s iff for every b ∈ s, a · b ∈ s.

Русский

Пусть G действует на α и s ⊆ α конечно. Тогда a ∈ стабилизатор G s тогда и только тогда, когда для каждого b ∈ s выполняется a · b ∈ s.

LaTeX

$$$a \in \mathrm{Stab}_G(s) \iff \forall \; b \; (b \in s \rightarrow a \cdot b \in s)$$$

Lean4

@[to_additive]
theorem mem_stabilizer_set' {s : Set α} (hs : s.Finite) : a ∈ stabilizer G s ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ s :=
  by
  lift s to Finset α using hs
  classical simp [-mem_stabilizer_iff, mem_stabilizer_finset']

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