monotone_projIcc

Mathlib.Order.Interval.Set.ProjIcc

URI: https://scilib.ai/kg/mathlib#Set.monotone_projIcc

English

The map projIcc a b h is monotone on Icc(a,b).

Русский

Функция projIcc(a,b,h) монотонна на Icc(a,b).

LaTeX

$$$\text{Monotone}(\operatorname{projIcc}(a,b,h))$$$

Lean4

theorem monotone_projIcc : Monotone (projIcc a b h) := fun _ _ hxy => max_le_max le_rfl <| min_le_min le_rfl hxy

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

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

Разделы

Аффилиация

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