monotone_projIci

Mathlib.Order.Interval.Set.ProjIcc

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

English

The map projIci a is monotone with respect to the order on the half-line [a, ∞).

Русский

Функция projIci a монотонна на луче [a, ∞).

LaTeX

$$$\text{Monotone}(\operatorname{projIci}(a))$$$

Lean4

theorem monotone_projIci : Monotone (projIci a) := fun _ _ => max_le_max le_rfl

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

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

Разделы

Аффилиация

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