toIcoMod_lt_right

Mathlib.Algebra.Order.ToIntervalMod

URI: https://scilib.ai/kg/mathlib#toIcoMod_lt_right

English

We have toIcoMod hp a b < a + p.

Русский

Для toIcoMod обозначение выполняется: toIcoMod hp a b < a + p.

LaTeX

$$$\mathrm{toIcoMod}(hp,a,b) < a + p$$$

Lean4

theorem toIcoMod_lt_right (a b : α) : toIcoMod hp a b < a + p :=
  (Set.mem_Ico.1 (toIcoMod_mem_Ico hp a b)).2

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

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

Разделы

Аффилиация

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