IicExtend

Mathlib.Order.Interval.Set.ProjIcc

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

English

If f is monotone on Iic b, then IicExtend f is monotone on α.

Русский

Если f монотонна на Iic b, то IicExtend f монотонна на всей области.

LaTeX

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

Lean4

protected theorem IicExtend {f : Iic b → β} (hf : Monotone f) : Monotone (IicExtend f) :=
  hf.comp monotone_projIic

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

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

Разделы

Аффилиация

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