sub_iInf

Mathlib.Data.ENNReal.Operations

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

← MathLib Explorer

English

Subtraction distributes over iInf in ENNReal: a − ⨅ i f(i) = ⨆ i (a − f(i)).

Русский

В ENNReal вычитание распределяется над iInf: a − ⨅ i f(i) = ⨆ i (a − f(i)).

LaTeX

$$$ a - \bigl(\inf_i f(i)\bigr) = \sup_i\, (a - f(i)) $$$

Lean4

theorem sub_iInf : (a - ⨅ i, f i) = ⨆ i, a - f i :=
  by
  refine eq_of_forall_ge_iff fun c => ?_
  rw [tsub_le_iff_right, add_comm, iInf_add]
  simp [tsub_le_iff_right, add_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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