partialSups_eq

Mathlib.Order.PartialSups

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

← MathLib Explorer

English

If f is monotone, then partialSups f = f.

Русский

Если f монотонна, то partialSups f = f.

LaTeX

$$$\\text{Monotone}(f) \\Rightarrow \\mathrm{partialSups}\\, f = f$$$

Lean4

theorem partialSups_eq {f : ι → α} (hf : Monotone f) : partialSups f = f :=
  funext fun i ↦ le_antisymm (partialSups_le _ _ _ (@hf · i)) (le_partialSups _ _)

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

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

Разделы

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

Аффилиация

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