inv_subtypePerm — Mathlib

English

The inverse identity for subtypePerm: the inverse of the restricted permutation equals the restriction of the inverse with the appropriately transformed predicate.

Русский

Обратная перестановка по подтипу равна ограничению обратной перестановки на подтипе с корректно преобразованным условием.

LaTeX

$$$$ (f.subtypePerm hf)^{-1} = f^{-1}.subtypePerm (inv\_aux.1 hf). $$$$

Lean4

/-- See `Equiv.Perm.subtypePerm_inv`. -/
@[simp]
theorem inv_subtypePerm (f : Perm α) (hf) : (f.subtypePerm hf : Perm { x // p x })⁻¹ = f⁻¹.subtypePerm (inv_aux.1 hf) :=
  rfl

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