support_filter

Mathlib.Data.Finsupp.Basic

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

English

The support of the filtered function f.filter p is exactly the elements of the original support that satisfy p.

Русский

Опора фильтрованной функции f.filter p равна точкам из опоры f, удовлетворяющим p.

LaTeX

$$$$ (f.filter p).\\mathrm{support} = \\{ x \\in f.support \\mid p\\,x \\}. $$$$

Lean4

@[simp]
theorem support_filter : (f.filter p).support = {x ∈ f.support | p x} :=
  rfl

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

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

Разделы

Аффилиация

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