fromSubtype_π_subtype — Mathlib

English

The canonical map biproduct.toSubtype f p equals biproduct.desc with a piecewise description by p.

Русский

Каноническое отображение biproduct.toSubtype f p равно biproduct.desc с разложением по p.

LaTeX

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

Lean4

@[reassoc] -- Not `@[simp]` because `simp` can prove this

theorem fromSubtype_π_subtype (j : Subtype p) :
    biproduct.fromSubtype f p ≫ biproduct.π f j = biproduct.π (Subtype.restrict p f) j := by
  classical
  ext
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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