Ici_sSup

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#UpperSet.Ici_sSup

English

For a complete lattice, Ici of a supremum over a set equals the supremum over all Ici(a) for a in the set.

Русский

Для полной решетки верхних множеств Ici(sup S) = sup {Ici(a) : a ∈ S}.

LaTeX

$$$Ici(\mathrm{sSup} \, S) = \bigsup_{a \in S} Ici(a)$$$

Lean4

@[simp]
theorem Ici_sSup (S : Set α) : Ici (sSup S) = ⨆ a ∈ S, Ici a :=
  SetLike.ext fun c => by simp only [mem_Ici_iff, mem_iSup_iff, sSup_le_iff]

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

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

Разделы

Аффилиация

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