finite_compl_fixedBy — Mathlib

English

A swap is contained in the closure of a set of swaps; equivalently the fixed-by complement is finite.

Русский

Транспозиция входит в замыкание множества транспозиций; эквивалентно конечности дополнения фиксирования.

LaTeX

$$theorem closure_prime_cycle_swap ...$$

Lean4

theorem finite_compl_fixedBy {σ : Perm α} (h : σ.IsSwap) : (fixedBy α σ)ᶜ.Finite :=
  by
  obtain ⟨x, y, -, rfl⟩ := h
  exact finite_compl_fixedBy_swap

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