isMinFilter_iff — Mathlib

English

IsMaxFilter is preserved under eventual equality: f and g are interchangeable if they are eventually equal and agree at a.

Русский

Максимальное свойство сохраняется при эквивалентности по почти всей области: f и g совпадают по почти всей области и в a.

LaTeX

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

Lean4

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

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