existsUnique_div_zpow_mem_Ico — Mathlib

English

There exists a unique m such that b·a^m lies in the half-open interval Ioc(c, c a) (i.e., c < b a^m ≤ c a).

Русский

Существует единственный m, для которого b·a^m принадлежит интервалу Ioc(c, c a) (c < b a^m ≤ c a).

LaTeX

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

Lean4

@[to_additive]
theorem existsUnique_div_zpow_mem_Ico {a : G} (ha : 1 < a) (b c : G) : ∃! m : ℤ, b / a ^ m ∈ Set.Ico c (c * a) := by
  simpa only [mem_Ico, 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)

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