le_sup

Mathlib.Data.Finset.Lattice.Fold

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

English

If b ∈ s, then f(b) ≤ s.sup f.

Русский

Если b ∈ s, то f(b) ≤ sup f.

LaTeX

$$$ \\text{hb} : b \\in s \\Rightarrow f b \\le s.sup f $$$

Lean4

theorem le_sup {b : β} (hb : b ∈ s) : f b ≤ s.sup f :=
  Finset.sup_le_iff.1 le_rfl _ hb

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

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

Разделы

Аффилиация

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