csInf_upperBounds_range — Mathlib

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 _

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