closure_iSup_closure

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#LowerAdjoint.closure_iSup_closure

English

For a family f: i ↦ α, u(l(⨆ i, u(l(f i)))) = u(l(⨆ i, f i)).

Русский

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

LaTeX

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

Lean4

theorem closure_iSup_closure (f : ι → α) : u (l (⨆ i, u (l (f i)))) = u (l (⨆ i, f i)) :=
  l.closureOperator.closure_iSup_closure _

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

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

Разделы

Аффилиация

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