ciSup_eq

Mathlib.Order.ConditionallyCompleteLattice.Indexed

URI: https://scilib.ai/kg/mathlib#IsLUB.ciSup_eq

English

The coercion of the supremum equals the supremum taken in WithBot α.

Русский

Приведение к WithBot сохраняет супремум: ↑(⨆ i, f i) = (⨆ i, f i) в WithBot α.

LaTeX

$$$\uparrow\left(\sup_i f(i)\right) = \sup_i f(i)\quad\text{in } WithBot(\alpha)$$$

Lean4

theorem ciSup_eq [Nonempty ι] {f : ι → α} (H : IsLUB (range f) a) : ⨆ i, f i = a :=
  H.csSup_eq (range_nonempty f)

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

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

Разделы

Аффилиация

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