subtypeDomain_not_piecewise — Mathlib

English

Let f be a finitely supported function on the subtype P and g on the complementary subtype. Then the subtypeDomain for not-P of f.piecewise g equals g.

Русский

Пусть f— finitely supported функция на подтипе P, а g — на комплементарном подтипе. Тогда subtypeDomain (¬P) (f.piecewise g) = g.

LaTeX

$$$\\mathrm{subtypeDomain}(\\,\\neg P\\,\\,)(f.\\mathrm{piecewise} g) = g$$$

Lean4

@[simp]
theorem subtypeDomain_not_piecewise (f : Subtype P →₀ M) (g : { a // ¬P a } →₀ M) :
    subtypeDomain (¬P ·) (f.piecewise g) = g :=
  Finsupp.ext fun a => dif_neg a.prop

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