filter_eq_nil — Mathlib

English

Filter equals zero iff every element in s fails p.

Русский

Фильтр равен нулю тогда и только тогда, когда для каждого элемента s неверно p.

LaTeX

$$$\\mathrm{filter}_p(s) = 0 \\iff \\forall a \in s, \\neg p(a)$$$

Lean4

@[simp]
theorem filter_eq_nil {s} : filter p s = 0 ↔ ∀ a ∈ s, ¬p a :=
  Quot.inductionOn s fun _l =>
    Iff.trans ⟨fun h => eq_nil_of_length_eq_zero (congr_arg card h), congr_arg ofList⟩ (by simp)

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