toIocMod_le_right

Mathlib.Algebra.Order.ToIntervalMod

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

English

We have toIocMod hp a b ≤ a + p.

Русский

Для toIocMod hp a b ≤ a + p.

LaTeX

$$$\mathrm{toIocMod}(hp,a,b) \le a + p$$$

Lean4

theorem toIocMod_le_right (a b : α) : toIocMod hp a b ≤ a + p :=
  (Set.mem_Ioc.1 (toIocMod_mem_Ioc hp a b)).2

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

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

Разделы

Аффилиация

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