existsUnique_mul_zpow_mem_Ico — Mathlib

English

For a>1, for any b,c there exists unique m with b·a^m ∈ [c, c a).

Русский

Для a>1 существует уникальный m такое, что b·a^m ∈ [c, c a).

LaTeX

$$$\\exists! m\\in \\mathbb{Z},\\ b\\cdot a^{m} \\in Ico(c, c a).$$$

Lean4

@[to_additive]
theorem existsUnique_mul_zpow_mem_Ico {a : G} (ha : 1 < a) (b c : G) : ∃! m : ℤ, b * a ^ m ∈ Set.Ico c (c * a) :=
  (Equiv.neg ℤ).bijective.existsUnique_iff.2 <| by
    simpa only [Equiv.neg_apply, mem_Ico, zpow_neg, ← div_eq_mul_inv, le_div_iff_mul_le, one_mul, mul_comm c,
      div_lt_iff_lt_mul, mul_assoc] using existsUnique_zpow_near_of_one_lt' ha (b / c)

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