exists_pow_lt — Mathlib

English

Same principle as above with alternative formulation; unique m s.t. b / a^m ∈ (c, c a].

Русский

Тот же принцип в другой формулировке; существует уникальный m, такое что b / a^m ∈ (c, c a].

LaTeX

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

Lean4

@[to_additive]
theorem exists_pow_lt {a : G} (ha : a < 1) (b : G) : ∃ n : ℕ, a ^ n < b :=
  (exists_lt_pow (one_lt_inv'.mpr ha) b⁻¹).imp <| by simp

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