filter_apply_neg — Mathlib

English

Let f be a finitely supported function f: α →₀ M. For any a ∈ α with not p(a), the filtered value at a is zero.

Русский

Пусть f: α →₀ M — функция с конечной опорой. Для любого a ∈ α, если ¬p(a), то значение f на a после фильтрации равно нулю.

LaTeX

$$$$ \\forall a, \\neg p(a) \\to (f.filter p)\\,a = 0. $$$$

Lean4

@[simp]
theorem filter_apply_neg {a : α} (h : ¬p a) : f.filter p a = 0 :=
  if_neg h

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