le_iSup₂

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#le_iSup₂

English

If a ≤ f(i)(j) for all i and j, then a ≤ ⨆ (i) (j), f(i)(j).

Русский

Если $a \\le f(i)(j)$ при всех $i,j$, то $a \\le \\bigsup_{i,j} f(i)(j)$.

LaTeX

$$$$a \\le f(i,j) \\quad\\Rightarrow\\quad a \\le \\bigsup_{i,j} f(i,j).$$$$

Lean4

theorem le_iSup₂ {f : ∀ i, κ i → α} (i : ι) (j : κ i) : f i j ≤ ⨆ (i) (j), f i j :=
  le_iSup_of_le i <| le_iSup (f i) j

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

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

Разделы

Аффилиация

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