ne_top_of_lt — Mathlib

English

Let β be a preorder with a top element ⊤. For any filter l on α and any functions f, g: α → β, if f(x) < g(x) holds eventually along l, then f(x) ≠ ⊤ holds eventually along l.

Русский

Пусть β упорядочено с верхним элементом ⊤. Для любого фильтра l на α и функций f, g: α → β, если f(x) < g(x) выполняется почти повсюду вдоль l, то f(x) ≠ ⊤ выполняется почти повсюду вдоль l.

LaTeX

$$$$(\\forall \\text{ᶠ } x \\in l,\\, f(x) < g(x)) \\Rightarrow (\\forall \\text{ᶠ } x \\in l,\\, f(x) \\neq \\top)$$$$

Lean4

theorem ne_top_of_lt [Preorder β] [OrderTop β] {l : Filter α} {f g : α → β} (h : ∀ᶠ x in l, f x < g x) :
    ∀ᶠ x in l, f x ≠ ⊤ :=
  h.mono fun _ hx => hx.ne_top

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