IciExtend

Mathlib.Order.Interval.Set.ProjIcc

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

English

If f is monotone, then its extension to the whole domain via IciExtend is monotone as well.

Русский

Если f монотонна на области Ici a, то её расширение по IciExtend монотонно на всей области.

LaTeX

$$$\\text{Monotone}(\\mathrm{IciExtend} f)$$$

Lean4

protected theorem IciExtend {f : Ici a → β} (hf : Monotone f) : Monotone (IciExtend f) :=
  hf.comp monotone_projIci

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

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

Разделы

Аффилиация

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