isLUB_ciSup — Mathlib

English

For any nonempty index set and any function f with bounded above range, the range of f has as its least upper bound the supremum ⨆ i, f(i).

Русский

Пусть I непусто, f : I → α, диапазон ограничен сверху. Тогда множество {f(i)} имеет наименьшее верхнее границу, равную sup_i f(i).

LaTeX

$$$\text{IsLUB}(\operatorname{range}(f), \sup_i f(i))$$$

Lean4

theorem isLUB_ciSup [Nonempty ι] {f : ι → α} (H : BddAbove (range f)) : IsLUB (range f) (⨆ i, f i) :=
  isLUB_csSup (range_nonempty f) H

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