English
If 0 < x ≤ 1 and 0 < y < 1 in a suitable Archimedean setting, there exists n ∈ ℕ with y^{n+1} < x ≤ y^n.
Русский
Если 0 < x ≤ 1 и 0 < y < 1 в архимедовом окружении, то существует n ∈ ℕ такое, что y^{n+1} < x ≤ y^n.
LaTeX
$$$\\exists n ∈ \\mathbb{N}, \\ y^{n+1} < x \\land x ≤ y^n$$$
Lean4
/-- Given `x` and `y` between `0` and `1`, `x` is between two successive powers of `y`.
This is the same as `exists_nat_pow_near`, but for elements between `0` and `1` -/
theorem exists_nat_pow_near_of_lt_one (xpos : 0 < x) (hx : x ≤ 1) (ypos : 0 < y) (hy : y < 1) :
∃ n : ℕ, y ^ (n + 1) < x ∧ x ≤ y ^ n :=
by
rcases exists_nat_pow_near (one_le_inv_iff₀.2 ⟨xpos, hx⟩) (one_lt_inv_iff₀.2 ⟨ypos, hy⟩) with ⟨n, hn, h'n⟩
refine ⟨n, ?_, ?_⟩
· rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n
· rwa [inv_pow, inv_le_inv₀ (pow_pos ypos _) xpos] at hn
