strictMonoOn_IciExtend

Mathlib.Order.Interval.Set.ProjIcc

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

← MathLib Explorer

English

If f is strictly monotone on Ici a, then the extension ICIExtend f is strictly monotone on Ici a.

Русский

Если f строго монотонна на Ici a, то расширение ICIExtend f строго монотонно на Ici a.

LaTeX

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

Lean4

theorem strictMonoOn_IciExtend {f : Ici a → β} (hf : StrictMono f) : StrictMonoOn (IciExtend f) (Ici a) :=
  hf.comp_strictMonoOn strictMonoOn_projIci

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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