compl_filter — Mathlib

English

The complement of a universal filter equals the filter by negated predicate: (univ.filter p)ᶜ = univ.filter (fun x => ¬p x).

Русский

Дополнение всеобъемлющего фильтра равняется фильтру по отрицательному предикату: (univ.filter p)ᶜ = univ.filter (¬p).

LaTeX

$$$ (univ.filter p)^{c} = univ.filter (\\lambda x \\,. \\neg p x)$$$

Lean4

@[simp]
theorem compl_filter (p : α → Prop) [DecidablePred p] [∀ x, Decidable ¬p x] :
    (univ.filter p)ᶜ = univ.filter fun x => ¬p x :=
  ext <| by simp

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