sup_eq_top_iff — Mathlib

English

For a nonempty finite s, s.sup f equals the top iff there exists b ∈ s with f(b) = ⊤.

Русский

Для непустого конечного s: s.sup f = ⊤ ⇔ ∃ b ∈ s, f(b) = ⊤.

LaTeX

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

Lean4

protected theorem sup_eq_top_iff {α : Type*} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ι → α}
    (hs : s.Nonempty) : s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤ :=
  by
  cases subsingleton_or_nontrivial α
  · simpa [Subsingleton.elim _ (⊤ : α)]
  · exact Finset.sup_eq_top_iff

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