iSup₂_le_iSup

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iSup₂_le_iSup

English

If κ: ι → Sort* and f: ι → α, then ⨆ (i) (_ : κ i), f i ≤ ⨆ i, f i.

Русский

Если κ: ι → Sort и f: ι → α, то ⨆ (i) (_ : κ i), f i ≤ ⨆ i, f i.

LaTeX

$$$$\\big\\lvert\\!\\!\\!\\!\\!\\!\\!\\!\\; \\text{(двойная индексация)} \\le \\iSup_i f(i).$$$$

Lean4

theorem iSup₂_le_iSup (κ : ι → Sort*) (f : ι → α) : ⨆ (i) (_ : κ i), f i ≤ ⨆ i, f i :=
  iSup₂_le fun i _ => le_iSup f i

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

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

Разделы

Аффилиация

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