Iic_iInf₂

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#LowerSet.Iic_iInf₂

English

Distributes over a double infimum: Iic(⨅ i, j, f i j) = ⨅ i, j, Iic(f i j).

Русский

Дистрибутивно по двойному inf: Iic(⨅ i, j, f(i,j)) = ⨅ i, j, Iic(f(i,j)).

LaTeX

$$Iic (⨅ (i) (j), f i j) = ⨅ (i) (j), Iic (f i j)$$

Lean4

theorem Iic_iInf₂ (f : ∀ i, κ i → α) : Iic (⨅ (i) (j), f i j) = ⨅ (i) (j), Iic (f i j) := by simp

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

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

Разделы

Аффилиация

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