toIocDiv_eq_sub

Mathlib.Algebra.Order.ToIntervalMod

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

English

In the same setting, the IocDiv of a and b equals the IocDiv of 0 and (b − a).

Русский

В той же обстановке IocDiv hp a b = IocDiv hp 0 (b − a).

LaTeX

$$$$ \operatorname{toIocDiv}(hp, a, b) = \operatorname{toIocDiv}(hp, 0, b-a) $$$$

Lean4

theorem toIocDiv_eq_sub (a b : α) : toIocDiv hp a b = toIocDiv hp 0 (b - a) := by
  rw [toIocDiv_sub_eq_toIocDiv_add, zero_add]

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

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

Разделы

Аффилиация

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