sup_singleton

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.sup_singleton

English

The supremum over a singleton equals the value of the function at that element: ({b} ).sup f = f(b).

Русский

Наибольшая грань над одиночным множеством равна значению функции в этом элементе: ({b}).sup f = f(b).

LaTeX

$$$ (\\{ b \\} : Finset \\beta).sup f = f b $$$

Lean4

@[simp]
theorem sup_singleton {b : β} : ({ b } : Finset β).sup f = f b :=
  Multiset.sup_singleton

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

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

Разделы

Аффилиация

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