filter_singleton — Mathlib

English

Filtering a singleton yields a singleton or zero depending on p a.

Русский

Фильтрация множества из одного элемента даёт либо это множество, либо ноль в зависимости от p a.

LaTeX

$$$\\mathrm{filter}_p(\\{a\\}) = \\begin{cases} \\{a\\}, & p(a) \\n \\ 0, & \\neg p(a) \\end{cases}$$$

Lean4

theorem filter_singleton {a : α} (p : α → Prop) [DecidablePred p] : filter p { a } = if p a then { a } else ∅ := by
  simp only [singleton, filter_cons, filter_zero, Multiset.add_zero, empty_eq_zero]

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