support_subtypeDomain

Mathlib.Data.DFinsupp.Defs

URI: https://scilib.ai/kg/mathlib#DFinsupp.support_subtypeDomain

English

The support of subtypeDomain p f equals f.support.subtype p.

Русский

Опора subtypeDomain p f равна f.support.subtype p.

LaTeX

$$$\\mathrm{support}(\\mathrm{subtypeDomain}\\;p\\ f) = f.{\\mathrm{support}}.\\mathrm{subtype}\\ p$$$

Lean4

@[simp]
theorem support_subtypeDomain {f : Π₀ i, β i} : (subtypeDomain p f).support = f.support.subtype p :=
  by
  ext i
  simp

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

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

Разделы

Аффилиация

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