iSup_prod

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iSup_prod

English

Let f : β × γ → α. Then iSup over x equals iSup over i then j of f i j; i.e. ⨆ x f x = ⨆ i ⨆ j f(i,j).

Русский

Пусть f : β × γ → α. Тогда iSup по x равен iSup по i и по j от f(i,j).

LaTeX

$$$$ \iSup_{x} f x = \iSup_{i} \iSup_{j} f(i,j) $$$$

Lean4

theorem iSup_prod {f : β × γ → α} : ⨆ x, f x = ⨆ (i) (j), f (i, j) :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, Prod.forall]

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

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

Разделы

Аффилиация

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