English
Filtering a singleton by p yields either the singleton or zero depending on whether p i holds.
Русский
Фильтрация одиночного по p даёт либо сам одиночный элемент, либо ноль, в зависимости от того, выполняется ли p i.
LaTeX
$$$(\mathrm{single}\ i\ x).\mathrm{filter} p = \mathrm{ite}(p i) (\mathrm{single}\ i\ x) 0$$$
Lean4
theorem filter_single (p : ι → Prop) [DecidablePred p] (i : ι) (x : β i) :
(single i x).filter p = if p i then single i x else 0 :=
by
ext j
have := apply_ite (fun x : Π₀ i, β i => x j) (p i) (single i x) 0
dsimp at this
rw [filter_apply, this]
obtain rfl | hij := Decidable.eq_or_ne j i
· rfl
· rw [single_eq_of_ne hij, ite_self, ite_self]
