ciSup_set_le_iff — Mathlib

English

The coercion of the supremum equals the supremum taken in WithTop α for a bounded-above family.

Русский

Приведение к WithTop сохраняет супремум: ↑(⨆ i, f i) = ⨆ i, f i в WithTop α.

LaTeX

$$$\uparrow\left(\sup_i f(i)\right) = \sup_i f(i) \quad\text{in } WithTop(\alpha)$$$

Lean4

theorem ciSup_set_le_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty) (hf : BddAbove (f '' s)) :
    ⨆ i : s, f i ≤ a ↔ ∀ i ∈ s, f i ≤ a :=
  (isLUB_le_iff <| isLUB_ciSup_set hf hs).trans forall_mem_image

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