inv_iInf

Mathlib.Data.ENNReal.Inv

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

English

The inverse of an infimum equals the infimum of inverses: (⨅ i, f_i)⁻¹ = ⨆ i, (f_i)⁻¹.

Русский

Обратное инфимума равно инфимума обратных: (⨅ i, f_i)⁻¹ = ⨆ i, (f_i)⁻¹.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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