strictMonoOn_projIcc

Mathlib.Order.Interval.Set.ProjIcc

URI: https://scilib.ai/kg/mathlib#Set.strictMonoOn_projIcc

English

projIcc a b h is strictly monotone on Icc a b.

Русский

projIcc a b h строго монотонна на Icc a b.

LaTeX

$$$\text{StrictMonoOn}(\operatorname{projIcc}(a,b,h), \mathrm{Icc}(a,b))$$$

Lean4

theorem strictMonoOn_projIcc : StrictMonoOn (projIcc a b h) (Icc a b) := fun x hx y hy hxy => by
  simpa only [projIcc_of_mem, hx, hy]

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

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

Разделы

Аффилиация

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