isMaxFilter — Mathlib

English

If g ≤^l f holds eventually along l and f(a)=g(a), and f is a maximal filter at a, then g is also a maximal filter at a.

Русский

Если g неравно меньше f вплоть до эквивалентности вдоль фильтра l и f(a)=g(a) и f является максимальным фильтром в a, тогда g тоже максимальный фильтр в a.

LaTeX

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

Lean4

theorem isMaxFilter {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a)
    (h : IsMaxFilter f l a) : IsMaxFilter g l a :=
  by
  refine hle.mp (h.mono fun x hf hgf => ?_)
  rw [← hfga]
  exact le_trans hgf hf

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