iSup_singleton

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iSup_singleton

English

The supremum over a singleton {b} of f equals f(b).

Русский

Супремум по одиночному множеству {b} равен f(b).

LaTeX

$$$$ \\sup_{x \\in \\{b\\}} f(x) = f(b) $$$$

Lean4

theorem iSup_singleton {f : β → α} {b : β} : ⨆ x ∈ (singleton b : Set β), f x = f b := by simp

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

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

Разделы

Аффилиация

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