existsUnique_sub_zpow_mem_Ioc — Mathlib

English

There exists a unique m such that b / a^m ∈ Ioc(c, c a).

Русский

Существует единственный m, при котором b / a^m ∈ Ioc(c, c a).

LaTeX

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

Lean4

@[to_additive]
theorem existsUnique_sub_zpow_mem_Ioc {a : G} (ha : 1 < a) (b c : G) : ∃! m : ℤ, b / a ^ m ∈ Set.Ioc c (c * a) :=
  (Equiv.neg ℤ).bijective.existsUnique_iff.2 <| by
    simpa only [Equiv.neg_apply, zpow_neg, div_inv_eq_mul] using existsUnique_add_zpow_mem_Ioc ha b c

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