toIocMod_zero_sub_comm — Mathlib

English

Let α be as above with p > 0. For any a, b in α, the IocMod value from a to a − b relates to the IcoMod value from b to b − a by the formula: IocMod hp 0 (a−b) = p − IcoMod hp 0 (b−a).

Русский

Пусть α удовлетворяет тем же условиям; для любых a, b справедливо IocMod hp 0 (a−b) = p − IcoMod hp 0 (b−a).

LaTeX

$$$$ \operatorname{toIocMod}(hp, 0, a-b) = p - \operatorname{toIcoMod}(hp, 0, b-a) $$$$

Lean4

theorem toIocMod_zero_sub_comm (a b : α) : toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a) := by
  rw [← neg_sub, toIocMod_neg, neg_zero]

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