toDFinsupp_support

Mathlib.Data.Finsupp.ToDFinsupp

URI: https://scilib.ai/kg/mathlib#toDFinsupp_support

English

The support is preserved under the embedding: supp of toDFinsupp f equals supp of f.

Русский

Опора сохраняется при переходе к DFinsupp: поддержка (toDFinsupp f) равна поддержке f.

LaTeX

$$f.toDFinsupp.support = f.support$$

Lean4

@[simp]
theorem toDFinsupp_support (f : ι →₀ M) : f.toDFinsupp.support = f.support :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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