up_iSup

Mathlib.Order.CompleteLattice.Lemmas

URI: https://scilib.ai/kg/mathlib#ULift.up_iSup

English

For a family f(i) ∈ α, lifting commutes with iSup: up(⨆ i, f i) = ⨆ i, up(f i).

Русский

Для семейства f(i) ∈ α поднятие через ULift commute с iSup: up(⨆ i, f(i)) = ⨆ i, up(f(i)).

LaTeX

$$$\\mathrm{up}\\left(\\bigvee_{i} f(i)\\right) = \\bigvee_{i} \\mathrm{up}(f(i))$$$

Lean4

theorem up_iSup [SupSet α] (f : ι → α) : up (⨆ i, f i) = ⨆ i, up (f i) :=
  congr_arg ULift.up <| (down_iSup _).symm

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

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

Разделы

Аффилиация

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