toSubtype_eq_desc — Mathlib

English

For a decidable predicate p, biproduct.toSubtype f p equals biproduct.desc with injections for those j satisfying p j.

Русский

Для решаемого предиката p, biproduct.toSubtype f p эквивалентно biproduct.desc с инъекциями для тех j, что удовлетворяют p j.

LaTeX

$$$\\text{biproduct.toSubtype } f p = \\text{biproduct.desc }(\\lambda j. if p j then \\text{biproduct.ι } (Subtype.restrict p f) ⟨j, h⟩ else 0).$$$

Lean4

theorem toSubtype_eq_desc [DecidablePred p] :
    biproduct.toSubtype f p =
      biproduct.desc fun j => if h : p j then biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0 :=
  biproduct.hom_ext' _ _ (by simp)

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