lt_top_iff_ne_top — Mathlib

English

For β with a top element ⊤, and any filter l on α, f: α → β satisfies: f(x) < ⊤ eventually if and only if f(x) ≠ ⊤ eventually along l.

Русский

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

LaTeX

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

Lean4

theorem lt_top_iff_ne_top [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} :
    (∀ᶠ x in l, f x < ⊤) ↔ ∀ᶠ x in l, f x ≠ ⊤ :=
  ⟨Eventually.ne_of_lt, Eventually.lt_top_of_ne⟩

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