closure_iSup₂_closure

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#LowerAdjoint.closure_iSup₂_closure

← MathLib Explorer

English

For f: i ↦ κ i → α, u(l(⨆ i, κ i → α)) = u(l(⨆ i, α)).

Русский

Для f: i ↦ κ i → α выполняется u(l(⨆ i, f i)) = u(l(⨆ i, α)).

LaTeX

$$$u(l(\\bigvee i, f i)) = u(l(\\bigvee i, i))$$$

Lean4

theorem closure_iSup₂_closure (f : ∀ i, κ i → α) : u (l <| ⨆ (i) (j), u (l <| f i j)) = u (l <| ⨆ (i) (j), f i j) :=
  l.closureOperator.closure_iSup₂_closure _

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

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

Разделы

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

Аффилиация

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