support_eq_empty_iff — Mathlib

English

For any permutation p, the set of elements moved by p equals the set moved by p^{-1}.

Русский

Для любой перестановки p множество перемещаемых элементов одинаково для p и p^{-1}.

LaTeX

$$$$ \operatorname{support}(p) = \operatorname{support}(p^{-1}). $$$$

Lean4

@[simp]
theorem support_eq_empty_iff {σ : Perm α} : σ.support = ∅ ↔ σ = 1 := by
  simp_rw [Finset.ext_iff, mem_support, Finset.notMem_empty, iff_false, not_not, Equiv.Perm.ext_iff, one_apply]

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