iSup_eq_top — Mathlib

English

Let f: ι → α with α a complete linear order. Then iSup f = ⊤ if and only if for every b < ⊤ there exists i with b < f(i).

Русский

Пусть f: ι → α, где α — полная линейная упорядоченная совокупность. Тогда iSup f = ⊤ тогда и только тогда, когда для каждого b < ⊤ существует i, для которого b < f(i).

LaTeX

$$$\\displaystyle \\iota\\sup f = \\top \\iff \\forall b < \\top, \\exists i, b < f(i)$$$

Lean4

theorem iSup_eq_top (f : ι → α) : iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i := by
  simp only [← sSup_range, sSup_eq_top, Set.exists_range_iff]

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