coe_iSup₂

Mathlib.Order.UpperLower.CompleteLattice

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

English

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

Русский

Основание iSup₂ f равняется ⋃ i, ⋃ j, f i j.

LaTeX

$$$ (↑(iSup (i) (j), f i j)) = ⋃ (i) (j), f i j $$$

Lean4

@[norm_cast]
theorem coe_iSup₂ (f : ∀ i, κ i → LowerSet α) : (↑(⨆ (i) (j), f i j) : Set α) = ⋃ (i) (j), f i j := by simp

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

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

Разделы

Аффилиация

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