sup_eq_top_iff — Mathlib

English

In a linear order with a top element, s.sup f equals the top element if and only if there exists some b ∈ s with f(b) = top.

Русский

В линейном порядке с верхним элементом, sup f = ⊤ тогда и только тогда, когда существует b ∈ s such that f(b) = ⊤.

LaTeX

$$$s.sup f = \top \iff \exists b \in s, f(b) = \top$$$

Lean4

protected theorem sup_eq_top_iff {α : Type*} [LinearOrder α] [BoundedOrder α] [Nontrivial α] {s : Finset ι}
    {f : ι → α} : s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤ :=
  by
  simp only [← top_le_iff]
  exact Finset.le_sup_iff bot_lt_top

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