le_biSup

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#le_biSup

English

If i ∈ s, then f i ≤ ⨆ i ∈ s, f i.

Русский

Если i ∈ s, то f(i) ≤ sup_{i ∈ s} f(i).

LaTeX

$$$ f(i) \\le \\bigvee_{i \\in s} f(i) \\quad \\text{whenever } i \\in s. $$$

Lean4

theorem le_biSup {ι : Type*} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) : f i ≤ ⨆ i ∈ s, f i :=
  biInf_le (α := αᵒᵈ) f hi

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

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

Разделы

Аффилиация

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