toIocMod_neg' — Mathlib

English

Let α be an ordered abelian group with Archimedean property and p > 0. Then the Ioc-modulus under negation satisfies a symmetry: toIocMod hp (−a) b = p − toIcoMod hp a (−b).

Русский

Пусть α — упорядоченная абелева группа с архимедовым свойством и p > 0. Тогда выполняется симметрия для модульных интервалов: toIocMod hp (−a) b = p − toIcoMod hp a (−b).

LaTeX

$$$ toIocMod\; hp\; (-a)\; b = p - toIcoMod\; hp\; a\ (-b) $$$

Lean4

theorem toIocMod_neg' (a b : α) : toIocMod hp (-a) b = p - toIcoMod hp a (-b) := by
  simpa only [neg_neg] using toIocMod_neg hp (-a) (-b)

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