fun_support_eq

Mathlib.Data.Finsupp.Defs

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

English

The set-theoretic support of the underlying function equals the finsupp support.

Русский

Множество поддержки функции совпадает с опорой finsupp.

LaTeX

$$$\\operatorname{support}(f) = f\\operatorname{support}$$$

Lean4

@[simp, norm_cast]
theorem fun_support_eq (f : α →₀ M) : Function.support f = f.support :=
  Set.ext fun _x => mem_support_iff.symm

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

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

Разделы

Аффилиация

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