Ici_iSup₂

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.Ici_iSup₂

English

In a complete lattice, Ici of the supremum equals the intersection over all indices of Ici of the corresponding elements.

Русский

В полной решётке Ici(⨆ f) равно ⋂ Ici(f).

LaTeX

$$$$ \\mathrm{Ici}\\Big(\\big(\\sup_i f(i)\\big)\\Big) = \\bigcap_i \\mathrm{Ici}(f(i)). $$$$

Lean4

theorem Ici_iSup₂ (f : ∀ i, κ i → α) : Ici (⨆ (i) (j), f i j) = ⋂ (i) (j), Ici (f i j) := by simp_rw [Ici_iSup]

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

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

Разделы

Аффилиация

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