partialSups_monotone

Mathlib.Order.PartialSups

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

← MathLib Explorer

English

Repeated assertion: partialSups is monotone in its input function.

Русский

Повторное утверждение: partialSups монотонна в своей входной функции.

LaTeX

$$$\\mathrm{Monotone}(\\mathrm{partialSups})$$$

Lean4

theorem partialSups_monotone (f : ι → α) : Monotone (partialSups f) := fun i _ hnm ↦
  partialSups_le f i _ (fun _ hm'n ↦ le_partialSups_of_le _ (hm'n.trans hnm))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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