le_partialSups

Mathlib.Order.PartialSups

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

English

For any f: ι → α, we have f ≤ partialSups f.

Русский

Для любой функции f: ι → α выполняется f ≤ partialSups f.

LaTeX

$$$f \\le \\mathrm{partialSups} f$$$

Lean4

theorem le_partialSups (f : ι → α) : f ≤ partialSups f := fun _ => le_partialSups_of_le f le_rfl

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

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

Разделы

Аффилиация

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