sign_extendDomain — Mathlib

English

For subtype-permutations ep and en, the sign of ep.subtypeCongr en equals the product of signs of ep and en.

Русский

Для подтипных перестановок ep и en знак ep.subtypeCongr en равен произведению знаков ep и en.

LaTeX

$$$\\operatorname{sign}(\\operatorname{subtypeCongr}(\\text{ep},\\text{en})) = \\operatorname{sign}(\\text{ep}) \\cdot \\operatorname{sign}(\\text{en})$$$

Lean4

@[simp]
theorem sign_extendDomain (e : Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
    Equiv.Perm.sign (e.extendDomain f) = Equiv.Perm.sign e := by
  simp only [Equiv.Perm.extendDomain, sign_subtypeCongr, sign_permCongr, sign_refl, mul_one]

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