English
If x ≠ 0, x ≠ ∞, 1 < y, and y ≠ ∞, then there exists an integer n with x inside the half-open interval [y^n, y^{n+1}).
Русский
Пусть x ≠ 0, x ≠ ∞, y > 1 и y ≠ ∞. Тогда существует целое n такое, что x ∈ [y^n, y^{n+1}).
LaTeX
$$$\\forall x,y \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; x \\neq 0 \\land x \\neq \\infty \\land 1 < y \\land y \\neq \\infty \\Rightarrow \\exists n \\in \\mathbb{Z},\\; x \\in Ico (y^n) (y^{n+1})$$$
Lean4
theorem exists_mem_Ico_zpow {x y : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (hy : 1 < y) (h'y : y ≠ ⊤) :
∃ n : ℤ, x ∈ Ico (y ^ n) (y ^ (n + 1)) := by
lift x to ℝ≥0 using h'x
lift y to ℝ≥0 using h'y
have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
by
refine NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)
simpa only [Ne, coe_eq_zero] using hx
refine ⟨n, ?_, ?_⟩
· rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
· rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
