strictMonoOn_projIic

Mathlib.Order.Interval.Set.ProjIcc

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

English

projIic b is strictly monotone on Iic b.

Русский

projIic b строго монотонна на Iic b.

LaTeX

$$$\text{StrictMonoOn}(\operatorname{projIic}(b), \mathrm{Iic}(b))$$$

Lean4

theorem strictMonoOn_projIic : StrictMonoOn (projIic b) (Iic b) := fun x hx y hy hxy => by
  simpa only [projIic_of_mem, hx, hy]

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

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

Разделы

Аффилиация

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