iInf_prod

Mathlib.Order.CompleteLattice.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem iInf_prod {f : β × γ → α} : ⨅ x, f x = ⨅ (i) (j), f (i, j) :=
  @iSup_prod αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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