mabs — Mathlib

English

In a lattice-ordered group, the absolute value |a|_m is defined as a ⊔ a^{-1}; it is the join of a and its inverse. Consequently |a|_m equals max{a, a^{-1}} in the lattice order.

Русский

В упорядоченной по решётке группе абсолютное значение |a|_м определяется как a ⊔ a^{-1}; это наименьшее верхнее значение пары a и её обратного. Следовательно, |a|_м равно максимуму {a, a^{-1}} в порядке по решётке.

LaTeX

$$$|a|_m = a \sqcup a^{-1}$$$

Lean4

/-- `mabs a`, denoted `|a|ₘ`, is the absolute value of `a`. -/
@[to_additive /-- `abs a`, denoted `|a|`, is the absolute value of `a` -/
    ]
def mabs (a : α) : α :=
  a ⊔ a⁻¹

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