strictMonoOn_IicExtend — Mathlib

English

If f is strictly monotone on Ici a, then the restriction of its extension to Ici a is strictly monotone.

Русский

Если f строго монотонна на Ici a, то расширение ограничено до Ici a остаётся строго монотонным.

LaTeX

$$$\\text{StrictMonoOn}(\\mathrm{IciExtend} f) \\; (\\mathrm{Ici} a)$$$

Lean4

theorem strictMonoOn_IicExtend {f : Iic b → β} (hf : StrictMono f) : StrictMonoOn (IicExtend f) (Iic b) :=
  hf.comp_strictMonoOn strictMonoOn_projIic

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