lt_top_of_ne — Mathlib

English

Let β be a partial order with a top element ⊤. If a function f: α → β is not equal to ⊤ eventually along a filter l on α, then f(x) < ⊤ eventually along l.

Русский

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

LaTeX

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

Lean4

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

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