toFinsupp_support

Mathlib.Data.List.ToFinsupp

URI: https://scilib.ai/kg/mathlib#List.toFinsupp_support

English

Theorem identifying the explicit expression for the support set of l.toFinsupp.

Русский

Теорема, задающая явное множество поддержки l.toFinsupp.

LaTeX

$$$$ \\operatorname{supp}(l\\toFinsupp) = \\{ i \\in \\mathrm{Finset.range}(\\mathrm{length}(l)) \\mid l_i \\neq 0 \\}. $$$$

Lean4

theorem toFinsupp_support : l.toFinsupp.support = {i ∈ Finset.range l.length | getD l i 0 ≠ 0} :=
  rfl

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

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

Разделы

Аффилиация

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