sup_one

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

For any f, the supremum over {1} equals f(1).

Русский

Наименьшее верхнее значение над {1} равно f(1).

LaTeX

$$sup 1 f = f 1$$

Lean4

@[to_additive (attr := simp)]
theorem sup_one [SemilatticeSup β] [OrderBot β] (f : α → β) : sup 1 f = f 1 :=
  sup_singleton

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

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

Разделы

Аффилиация

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