monovary_self

Mathlib.Order.Monotone.Monovary

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

English

For any f: ι → α, Monovary(f, f) holds.

Русский

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

LaTeX

$$$\\operatorname{Monovary}(f, f)$$$

Lean4

theorem monovary_self (f : ι → α) : Monovary f f := fun _ _ => le_of_lt

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

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

Разделы

Аффилиация

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