subtypeDomain_piecewise — Mathlib

English

Let f be a finitely supported function from the subtype P to M, and g from the complementary subtype to M. Then the subtypeDomain of f.piecewise g with respect to P equals f.

Русский

Пусть f: Subtype P →₀ M, и g: {a // ¬P a} →₀ M. Тогда subtypeDomain P (f.piecewise g) = f.

LaTeX

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

Lean4

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

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