le_iSup₂_of_le

Mathlib.Order.CompleteLattice.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem le_iSup₂_of_le {f : ∀ i, κ i → α} (i : ι) (j : κ i) (h : a ≤ f i j) : a ≤ ⨆ (i) (j), f i j :=
  h.trans <| le_iSup₂ i j

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

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

Разделы

Аффилиация

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