English
Let α be an ordered additive group with an Archimedean property and let p > 0. For every a, b ∈ α and m ∈ Z, the value of the right-interval map toIocMod hp a applied to m·p + b depends only on b, not on m.
Русский
Пусть α — упорядоченная аддитивная группа с архимедовым свойством, пусть p > 0. Для любых a, b ∈ α и m ∈ Z значение правой границы модуля интервала toIocMod hp a, применяемое к m·p + b, зависит только от b и не зависит от m.
LaTeX
$$$\forall a,b \in \alpha\,\forall m \in \mathbb{Z},\; toIocMod\ hp\ a\ (m\cdot p + b) = toIocMod\ hp\ a\ b$$$
Lean4
@[simp]
theorem toIocMod_zsmul_add (a b : α) (m : ℤ) : toIocMod hp a (m • p + b) = toIocMod hp a b := by
rw [add_comm, toIocMod_add_zsmul]
