coe_iInf₂

Mathlib.Order.UpperLower.CompleteLattice

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

English

The underlying set of iInf over a two-argument family f i j equals ⋂ i, ⋂ j, f i j.

Русский

Основание iInf f равно ⋂ i, ⋂ j, f i j.

LaTeX

$$$ (↑(iInf (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j $$$

Lean4

@[norm_cast]
theorem coe_iInf₂ (f : ∀ i, κ i → LowerSet α) : (↑(⨅ (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j := by simp

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

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

Разделы

Аффилиация

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