support_filter — Mathlib

English

The support of the filtered DFinsupp is the set of those x in the original support with p(x) true.

Русский

Опора отфильтрованного DFinsupp равна множеству тех x из исходной опоры, для которых p(x) истина.

LaTeX

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

Lean4

@[simp]
theorem support_filter (f : Π₀ i, β i) : (f.filter p).support = {x ∈ f.support | p x} := by ext i;
  by_cases h : p i <;> simp [h]

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