strictMonoOn_projIci

Mathlib.Order.Interval.Set.ProjIcc

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

English

projIci a is strictly monotone on Ici a.

Русский

projIci a ограничено строго монотонно на Ici a.

LaTeX

$$$\text{StrictMonoOn}(\operatorname{projIci}(a), \mathrm{Ici}(a))$$$

Lean4

theorem strictMonoOn_projIci : StrictMonoOn (projIci a) (Ici a) := fun x hx y hy hxy => by
  simpa only [projIci_of_mem, hx, hy]

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

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

Разделы

Аффилиация

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