mabs_le

Mathlib.Algebra.Order.Group.Abs

URI: https://scilib.ai/kg/mathlib#mabs_le

English

For a, b in G, we have |a|_m ≤ b if and only if b^{-1} ≤ a and a ≤ b.

Русский

Для a, b в G верно: |a|_м ≤ b тогда и только тогда, что b^{-1} ≤ a и a ≤ b.

LaTeX

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

Lean4

@[to_additive]
theorem mabs_le : |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b := by rw [mabs_le', and_comm, inv_le']

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru