exists_pow_lt_of_lt_one — Mathlib

English

Under similar Archimedean conditions, there exists a natural power near x, i.e., between consecutive powers of y around x.

Русский

При аналогичных архимедовых условиях существует ближайшая степень y к x, между двумя соседними степенями.

LaTeX

$$$\\exists n ∈ \\mathbb{N}, y^n ≤ x < y^{n+1}$$$

Lean4

/-- For any `y < 1` and any positive `x`, there exists `n : ℕ` with `y ^ n < x`. -/
theorem exists_pow_lt_of_lt_one (hx : 0 < x) (hy : y < 1) : ∃ n : ℕ, y ^ n < x :=
  by
  by_cases y_pos : y ≤ 0
  · use 1
    simp only [pow_one]
    exact y_pos.trans_lt hx
  rw [not_le] at y_pos
  rcases pow_unbounded_of_one_lt x⁻¹ ((one_lt_inv₀ y_pos).2 hy) with ⟨q, hq⟩
  exact ⟨q, by rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq⟩

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