toIocMod_add_toIcoMod_zero — Mathlib

English

The same complementarity holds in the opposite order: the sum of IocMod from a to b and IcoMod from b to a equals p.

Русский

Та же комплементарность сохраняется при обращении порядка: сумма IocMod и IcoMod равна p.

LaTeX

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

Lean4

theorem toIocMod_add_toIcoMod_zero (a b : α) : toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p := by
  rw [_root_.add_comm, toIcoMod_add_toIocMod_zero]

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