toIcoMod_mem_Ico

Mathlib.Algebra.Order.ToIntervalMod

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

English

The value of toIcoMod hp a b lies in the interval [a, a+p).

Русский

Значение toIcoMod hp a b лежит в интервале [a, a+p).

LaTeX

$$$toIcoMod\, hp\, a\, b \in [a, a+p)$$$

Lean4

theorem toIcoMod_mem_Ico (a b : α) : toIcoMod hp a b ∈ Set.Ico a (a + p) :=
  sub_toIcoDiv_zsmul_mem_Ico hp a b

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

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

Разделы

Аффилиация

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