English
For a nonempty β and any function f: β → α with range bounded above, sInf(upperBounds(range f)) equals ⨆ i, f(i).
Русский
Для непустого множества β и любой функции f: β → α, если диапазон f ограничен сверху, то sInf(upperBounds(range f)) = ⨆ i, f(i).
LaTeX
$$$[Nonempty\ β] \rightarrow (hf : BddAbove(\mathrm{range}(f))) : \mathrm{sInf}(\mathrm{upperBounds}(\mathrm{range}(f))) = \bigsqcup_{i} f(i)$$$
Lean4
theorem csInf_upperBounds_range [Nonempty β] {f : β → α} (hf : BddAbove (range f)) :
sInf (upperBounds (range f)) = ⨆ i, f i :=
csInf_upperBounds_eq_csSup hf <| range_nonempty _