isMinFilter — Mathlib

English

If g ≤^l f and f is a max-filter, then g is also a max-filter; dual statements hold for min-filter.

Русский

Если g неравно меньше f вдоль l и f — максимумный фильтр, то и g — максимумный фильтр; симметрично для минимумов.

LaTeX

$$$g \\le^l f \\land f \\text{ adj } a \\Rightarrow \\mathrm{IsMaxFilter}(g,l,a) \\,;\\; \\text{(аналогично для минимального)}$$$

Lean4

theorem isMinFilter {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (hle : f ≤ᶠ[l] g) (hfga : f a = g a)
    (h : IsMinFilter f l a) : IsMinFilter g l a :=
  @Filter.EventuallyLE.isMaxFilter _ βᵒᵈ _ _ _ _ _ hle hfga h

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