mabs_le' — Mathlib

English

In a lattice-ordered group, the modulus of an element is bounded by b exactly when both the element and its inverse are bounded by b.

Русский

В решеточно-упорядоченной группе модуль элемента не превосходит b тогда и только тогда, когда сам элемент и его обратное также не превосходят b.

LaTeX

$$$|a|_m \le b \iff a \le b \land a^{-1} \le b$$$

Lean4

@[to_additive]
theorem mabs_le' : |a|ₘ ≤ b ↔ a ≤ b ∧ a⁻¹ ≤ b :=
  sup_le_iff

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