le_sup'_of_le

Mathlib.Data.Finset.Lattice.Fold

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

English

If a ≤ f(b) then a ≤ s.sup' ⟨b⟩ f.

Русский

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

LaTeX

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

Lean4

theorem le_sup'_of_le {a : α} {b : β} (hb : b ∈ s) (h : a ≤ f b) : a ≤ s.sup' ⟨b, hb⟩ f :=
  h.trans <| le_sup' _ hb

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

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

Разделы

Аффилиация

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