Ici_iSup

Mathlib.Order.UpperLower.Principal

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

← MathLib Explorer

English

Ici commutes with arbitrary suprema: Ici(sup_i f(i)) = sup_i Ici(f(i)).

Русский

Ici коммутирует с произвольными верхними пределами: Ici( sup_i f(i) ) = sup_i Ici(f(i)).

LaTeX

$$$Ici\left(\bigvee_i f(i)\right) = \bigvee_i Ici(f(i))$$$

Lean4

@[simp]
theorem Ici_iSup (f : ι → α) : Ici (⨆ i, f i) = ⨆ i, Ici (f i) :=
  SetLike.ext fun c => by simp only [mem_Ici_iff, mem_iSup_iff, iSup_le_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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