strictMonoOn_IccExtend

Mathlib.Order.Interval.Set.ProjIcc

URI: https://scilib.ai/kg/mathlib#StrictMono.strictMonoOn_IccExtend

English

If f is strictly monotone on Icc a b, then IccExtend h f is strictly monotone on Icc a b.

Русский

Если f строго монотонна на Icc a b, то IccExtend h f строго монотонна на Icc a b.

LaTeX

$$$\\text{StrictMonoOn}(\\mathrm{IccExtend} h f) \\; (\\mathrm{Icc} a b)$$$

Lean4

theorem strictMonoOn_IccExtend (hf : StrictMono f) : StrictMonoOn (IccExtend h f) (Icc a b) :=
  hf.comp_strictMonoOn (strictMonoOn_projIcc h)

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

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

Разделы

Аффилиация

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