subtypeDomain_extendDomain

Mathlib.Data.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.subtypeDomain_extendDomain

English

For f : Subtype P →₀ M, the subtypeDomain of the extension equals f.

Русский

Для f: Subtype P →₀ M, subtypeDomain P f.extendDomain = f.

LaTeX

$$$\\mathrm{subtypeDomain} P (f.\\extendDomain) = f$$$

Lean4

@[simp]
theorem subtypeDomain_extendDomain (f : Subtype P →₀ M) : subtypeDomain P f.extendDomain = f :=
  subtypeDomain_piecewise _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru