sup'_singleton

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.sup'_singleton

English

The supremum over a singleton set equals the image value: ( {b} ).sup' f = f(b).

Русский

Супремум над множеством из одного элемента равен значению функции в этом элементе.

LaTeX

$$$\bigl\{b\bigr\}.sup' f = f(b)$$$

Lean4

@[simp]
theorem sup'_singleton {b : β} : ({ b } : Finset β).sup' (singleton_nonempty _) f = f b :=
  rfl

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

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

Разделы

Аффилиация

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