sign_ofSubtype — Mathlib

English

Sign is preserved when extending to a subtype via the subtype embedding.

Русский

Знак сохраняется при переходе к подтипу через встраивание подтипа.

LaTeX

$$$\\operatorname{sign}(\\operatorname{ofSubtype}(f)) = \\operatorname{sign}(f)$$$

Lean4

@[simp]
theorem sign_ofSubtype {p : α → Prop} [DecidablePred p] (f : Equiv.Perm (Subtype p)) : sign (ofSubtype f) = sign f :=
  sign_extendDomain f (Equiv.refl (Subtype p))

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