isExtrFilter_iff — Mathlib

English

IsExtrFilter is preserved under eventual equality: if f and g are eventually equal, they share the extr-filter property at a.

Русский

Свойство ExtrFilter сохраняется при EventuallyEq между f и g.

LaTeX

$$$l.EventuallyEq f g \\Rightarrow (f(a)=g(a)) \\Rightarrow (\\mathrm{IsExtrFilter} f l a \\iff \\mathrm{IsExtrFilter} g l a)$$$

Lean4

theorem isExtrFilter_iff {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (heq : f =ᶠ[l] g)
    (hfga : f a = g a) : IsExtrFilter f l a ↔ IsExtrFilter g l a :=
  ⟨fun h => h.congr heq hfga, fun h => h.congr heq.symm hfga.symm⟩

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