fixed_point_card_lt_of_ne_one — Mathlib

English

The number of fixed points of a non-identity permutation on a finite set is strictly less than the size of the set minus one.

Русский

Число фиксированных точек конечного множества перестановки не-тождественной строго меньше размера множества минус единица.

LaTeX

$$$\#\{x \mid \sigma x = x\} < |\alpha| - 1$$$

Lean4

theorem fixed_point_card_lt_of_ne_one [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
    #{x | σ x = x} < Fintype.card α - 1 :=
  by
  rw [Nat.lt_sub_iff_add_lt, ← Nat.lt_sub_iff_add_lt', ← Finset.card_compl, Finset.compl_filter]
  exact one_lt_card_support_of_ne_one h

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