subtypePerm_inv — Mathlib

English

The inverse of the induced subtype permutation corresponds to the induced permutation of the inverse, with the appropriate transformed predicate.

Русский

Обратная подтиповой перестановке соответствует подтиповая перестановка от обратной операции, с подходящим преобразованием условия.

LaTeX

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

Lean4

/-- See `Equiv.Perm.inv_subtypePerm`. -/
theorem subtypePerm_inv (f : Perm α) (hf) :
    f⁻¹.subtypePerm hf = (f.subtypePerm <| inv_aux.2 hf : Perm { x // p x })⁻¹ :=
  rfl

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