coe_iSup

Mathlib.Order.CompleteLatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Iic.coe_iSup

English

For a family f:ι → Iic a, the coe of the iSup equals the iSup of the coerced elements.

Русский

Для семейства f:ι → Iic a коэффициент коe с iSup равен iSup из приведённых к α элементов.

LaTeX

$$$$ \uparrow(\operatorname{iSup} f) = \operatorname{iSup}(f(i) : α). $$$$

Lean4

@[simp]
theorem coe_iSup : (↑(⨆ i, f i) : α) = ⨆ i, (f i : α) := by rw [iSup, coe_sSup]; congr; ext; simp

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

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

Разделы

Аффилиация

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