coe_iSup

Mathlib.Order.CompleteSublattice

URI: https://scilib.ai/kg/mathlib#CompleteSublattice.coe_iSup

English

The α-value of the supremum of f(i) over i equals the supremum in α of the α-values f(i).

Русский

Значение в α наибольшей границы по i равно ⊔_i (f(i) : α).

LaTeX

$$$\left(\uparrow(\mathrm{iSup} f) : α\right) = \bigvee_{i} (f(i) : α)$$$

Lean4

@[simp]
theorem coe_iSup {ι} (f : ι → L) : (↑(iSup f) : α) = ⨆ i, (f i : α) := by rw [iSup, coe_sSup', iSup_range]

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

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

Разделы

Аффилиация

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