le_def — Mathlib

English

The le_def theorem states that for any a,b ∈ MulArchimedeanOrder M, a ≤ b if and only if ∃ n with |b| ≤ |a|^n.

Русский

Теорема le_def говорит, что для любых a,b ∈ MulArchimedeanOrder M выполняется: a ≤ b тогда и только если существует n такое, что |b| ≤ |a|^n.

LaTeX

$$$ a \le b \iff \exists n \in \mathbb{N}, \ |b| \le |a|^n $$$

Lean4

@[to_additive]
theorem le_def {a b : MulArchimedeanOrder M} : a ≤ b ↔ ∃ n, |b.val|ₘ ≤ |a.val|ₘ ^ n :=
  .rfl

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