toReal_iSup

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.toReal_iSup

English

If every f(i) ≠ ∞, then toReal commutes with iSup: (iSup f).toReal = ⨆ i, (f i).toReal.

Русский

Пусть все f(i) ≠ ∞; тогда toReal commuting with iSup: (iSup f).toReal = ⨆ i, (f i).toReal.

LaTeX

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

Lean4

theorem toReal_iSup (hf : ∀ i, f i ≠ ∞) : (iSup f).toReal = ⨆ i, (f i).toReal := by
  simp only [ENNReal.toReal, toNNReal_iSup hf, NNReal.coe_iSup]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru