index_stabilizer — Mathlib

English

For a finite Finset s, if every f i with i ∈ s has finite index, then iInf over i ∈ s f i has finite index.

Русский

Для конечного множества s, если для каждого i ∈ s у f i конечный индекс, то iInf по i ∈ s f i имеет конечный индекс.

LaTeX

$$(⨅ i ∈ s, f i).FiniteIndex$$

Lean4

@[to_additive]
theorem index_stabilizer : (stabilizer G x).index = (orbit G x).ncard :=
  (Nat.card_congr (MulAction.orbitEquivQuotientStabilizer G x)).symm.trans (Nat.card_coe_set_eq (orbit G x))

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