support_inv — Mathlib

English

The support of a permutation is the same as the support of its inverse: supp(σ^{-1}) = supp(σ).

Русский

Опора перестановки равна опоре её обратной: supp(σ^{-1}) = supp(σ).

LaTeX

$$$\operatorname{supp}(\sigma^{-1}) = \operatorname{supp}(\sigma).$$$

Lean4

@[simp]
theorem support_inv (σ : Perm α) : support σ⁻¹ = σ.support := by
  simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]

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