iSup_mono

Mathlib.Order.CompleteLattice.Basic

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

English

If f ≤ g pointwise, then iSup f ≤ iSup g.

Русский

Если для всех i f(i) ≤ g(i), тогда iSup f ≤ iSup g.

LaTeX

$$$$\\forall i, f(i) \\le g(i) \\Rightarrow \\iSup_i f(i) \\le \\iSup_i g(i).$$$$

Lean4

@[gcongr]
theorem iSup_mono (h : ∀ i, f i ≤ g i) : iSup f ≤ iSup g :=
  iSup_le fun i => le_iSup_of_le i <| h i

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

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

Разделы

Аффилиация

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