le_map_iSup

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#Monotone.le_map_iSup

English

If f is monotone, then for any s: i → α, ⨆ i f(s i) ≤ f(iSup s).

Русский

Если f монотонна, то для любого s: i → α выполняется sup_i f(s i) ≤ f(iSup s).

LaTeX

$$[Monotone] f → ⨆ i, f(s i) ≤ f(iSup s)$$

Lean4

theorem le_map_iSup [CompleteLattice β] {f : α → β} (hf : Monotone f) : ⨆ i, f (s i) ≤ f (iSup s) :=
  iSup_le fun _ => hf <| le_iSup _ _

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

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

Разделы

Аффилиация

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