lt_mabs

Mathlib.Algebra.Order.Group.Unbundled.Abs

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

English

For all a,b in α, a < |b|_m iff a < b or a < b^{-1}.

Русский

Для всех a,b в α: a < |b|_м тогда и только тогда, когда a < b или a < b^{-1}.

LaTeX

$$$a < |b|_m \iff a < b \lor a < b^{-1}$$$

Lean4

@[to_additive]
theorem lt_mabs : a < |b|ₘ ↔ a < b ∨ a < b⁻¹ :=
  lt_max_iff

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

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

Разделы

Аффилиация

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