lt_def

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanOrder.lt_def

English

The lt_def theorem says a < b iff ∀ n, |b|^n < |a|.

Русский

Теорема lt_def: a < b тогда и только если ∀ n, |b|^n < |a|.

LaTeX

$$$ a < b \iff \forall n \in \mathbb{N}, \ |b|^n < |a| $$$

Lean4

@[to_additive]
theorem lt_def {a b : MulArchimedeanOrder M} : a < b ↔ ∀ n, |b.val|ₘ ^ n < |a.val|ₘ :=
  .rfl

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

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

Разделы

Аффилиация

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