filter_def — Mathlib

English

Filtering a DFinsupp by a predicate p yields a new DFinsupp supported exactly on those indices in the original support that satisfy p.

Русский

Фильтрация DFinsupp по предикату p даёт новый DFinsupp, опора которого точно состоит из тех индексов исходной опоры, где выполняется p.

LaTeX

$$$\\mathrm{filter}\\,p\\;f = \\mathrm{mk}(f.{\\mathrm{support}}.\\mathrm{filter}\\ p)\\; (\\lambda i, f i.1)$$$

Lean4

theorem filter_def (f : Π₀ i, β i) : f.filter p = mk (f.support.filter p) fun i => f i.1 := by ext i;
  by_cases h1 : p i <;> by_cases h2 : f i ≠ 0 <;> simp at h2 <;> simp [h1, h2]

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