inv_iSup

Mathlib.Data.ENNReal.Inv

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

English

The inverse of a supremum equals the infimum of inverses: (sup_i f_i)⁻¹ = inf_i (f_i)⁻¹.

Русский

Обратное верхнего предела равно нижнему пределу обратных: (sup_i f_i)⁻¹ = inf_i (f_i)⁻¹.

LaTeX

$$$(\\sup_i f_i)^{-1} = \\inf_i (f_i)^{-1}$$$

Lean4

theorem inv_iSup (f : ι → ℝ≥0∞) : (⨆ i, f i)⁻¹ = ⨅ i, (f i)⁻¹ :=
  OrderIso.invENNReal.map_iSup _

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

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

Разделы

Аффилиация

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