sup_def

Mathlib.Data.Finset.Lattice.Fold

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

English

The supremum over a finite set s of f equals the supremum of the multiset of f-values over s: sup_s f = (map f s).sup.

Русский

Наибольшая грань функции f на конечном множестве s равна верхней грани отображения значений f по s: sup_s f = (map f s).sup.

LaTeX

$$$ s.sup f = (s.1.map f).sup $$$

Lean4

theorem sup_def : s.sup f = (s.1.map f).sup :=
  rfl

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

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

Разделы

Аффилиация

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