isMaxFilter_iff — Mathlib

English

If f is an extrFilter and f equals g along l with equal value at a, then g is an extrFilter at a.

Русский

Если f — экстрФильтр и f и g эквивалентны вдоль l и имеют одинаковое значение в a, то g также является экстрФильтром в a.

LaTeX

$$$\\mathrm{IsExtrFilter}(f,l,a) \\land (f =^l g) \\land (f(a)=g(a)) \\Rightarrow \\mathrm{IsExtrFilter}(g,l,a)$$$

Lean4

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

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