exists_lt_pow — Mathlib

English

For any a>1 in a Archimedean ordered group, and any g, there exists a unique integer k such that a^k ≤ g < a^{k+1}.

Русский

Для любого a>1 в упорядоченной группе с Архимедовым свойством и любого g существует единственный целочисленный k такой, что a^k ≤ g < a^{k+1}.

LaTeX

$$$\\forall a>1\\ (g:\\, G),\\ExistsUnique k\\in \\mathbb{Z},\\ a^{k} \\le g \\land g < a^{k+1}. $$$

Lean4

@[to_additive]
theorem exists_lt_pow [CommMonoid M] [PartialOrder M] [MulArchimedean M] [MulLeftStrictMono M] {a : M} (ha : 1 < a)
    (b : M) : ∃ n : ℕ, b < a ^ n :=
  let ⟨k, hk⟩ := MulArchimedean.arch b ha
  ⟨k + 1, hk.trans_lt <| pow_lt_pow_right' ha k.lt_succ_self⟩

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