existsUnique_add_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},\\ b\\cdot a^{m} \\in Ioc(c, c a).$$$

Lean4

@[to_additive]
theorem existsUnique_add_zpow_mem_Ioc {a : G} (ha : 1 < a) (b c : G) : ∃! m : ℤ, b * a ^ m ∈ Set.Ioc c (c * a) :=
  (Equiv.addRight (1 : ℤ)).bijective.existsUnique_iff.2 <| by
    simpa only [zpow_add_one, div_lt_iff_lt_mul', le_div_iff_mul_le', ← mul_assoc, and_comm, mem_Ioc,
      Equiv.coe_addRight, mul_le_mul_iff_right] using existsUnique_zpow_near_of_one_lt ha (c / b)

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