filter_eq_self_iff — Mathlib

English

The equality f.filter p = f holds exactly when for all x, f(x) ≠ 0 implies p x.

Русский

Равенство f.filter p = f верно тогда и только тогда, когда для всех x выполняется f(x) ≠ 0 ⇒ p x.

LaTeX

$$$$ f.filter p = f \iff \forall x, f x \neq 0 \rightarrow p x. $$$$

Lean4

theorem filter_eq_self_iff : f.filter p = f ↔ ∀ x, f x ≠ 0 → p x := by
  simp only [DFunLike.ext_iff, filter_eq_indicator, Set.indicator_apply_eq_self, Set.mem_setOf_eq, not_imp_comm]

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