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' ⟨b,h⟩ f.

Русский

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

LaTeX

$$$f(b) \le s.sup' \langle b, h \rangle f$$$

Lean4

theorem le_sup' {b : β} (h : b ∈ s) : f b ≤ s.sup' ⟨b, h⟩ f :=
  (sup'_le_iff ⟨b, h⟩ f).1 le_rfl b h

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

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

Разделы

Аффилиация

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