biSup_add'

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.biSup_add'

← MathLib Explorer

English

We have (sup_i ⨆_{p(i)} f_i) + a = ⨆_i ⨆_{p(i)} (f_i + a).

Русский

Имеем (sup_i ⨆_{p(i)} f_i) + a = ⨆_i ⨆_{p(i)} (f_i + a).

LaTeX

$$$\\bigl(\\sup_i \\sup_{p(i)} f_i\\bigr) + a = \\sup_i \\sup_{p(i)} (f_i + a)$$$

Lean4

theorem biSup_add' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℝ≥0∞) : (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, f i + a :=
  by simp only [add_comm, add_biSup' h]

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

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

Разделы

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

Аффилиация

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