filter_apply_pos — Mathlib

English

If p i holds, then applying the filter p preserves the value: f.filter p i = f i.

Русский

Если p i истинно, то применение фильтра сохраняет значение: f.filter p i = f i.

LaTeX

$$$ f.filter p\, i = f i \quad \text{if } p i $$$

Lean4

theorem filter_apply_pos [∀ i, Zero (β i)] {p : ι → Prop} [DecidablePred p] (f : Π₀ i, β i) {i : ι} (h : p i) :
    f.filter p i = f i := by simp only [filter_apply, if_pos h]

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