toNNReal_iSup — Mathlib

English

If every f(i) ≠ ∞, then the NNReal of the supremum equals the supremum of NNReal-values: (iSup f).toNNReal = ⨆ i, (f i).toNNReal.

Русский

Пусть все f(i) ≠ ∞; тогда nnReal-образ максимумa равен максимуму nnReal-образов: (iSup f).toNNReal = ⨆ i, (f i).toNNReal.

LaTeX

$$$ (\mathrm{iSup}\ f).toNNReal = \sup_i (f(i).toNNReal) $$$

Lean4

theorem toNNReal_iSup (hf : ∀ i, f i ≠ ∞) : (iSup f).toNNReal = ⨆ i, (f i).toNNReal :=
  by
  lift f to ι → ℝ≥0 using hf
  simp_rw [toNNReal_coe]
  by_cases h : BddAbove (range f)
  · rw [← coe_iSup h, toNNReal_coe]
  · rw [NNReal.iSup_of_not_bddAbove h, iSup_coe_eq_top.2 h, toNNReal_top]

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