existsUnique_zpow_near_of_one_lt'

English

Same principle as above with alternative instantiation; there exists unique m with b/a^m in an interval Ico(c, c a).

Русский

То же самое в другой инстанциации: существует уникальный m с b/a^m в интервале Ico(c, c a).

LaTeX

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

Lean4

@[to_additive]
theorem existsUnique_zpow_near_of_one_lt' {a : G} (ha : 1 < a) (g : G) : ∃! k : ℤ, 1 ≤ g / a ^ k ∧ g / a ^ k < a := by
  simpa only [one_le_div', zpow_add_one, div_lt_iff_lt_mul'] using existsUnique_zpow_near_of_one_lt ha g

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