exists_mem_Ioc_zpow — Mathlib

English

Let x,y ∈ ℝ≥0 with x ≠ 0 and 1 < y. Then there exists n ∈ ℤ such that x ∈ (y^n, y^{n+1}].

Русский

Пусть x,y ∈ ℝ≥0, x ≠ 0 и 1 < y. Тогда существует n ∈ ℤ такое, что x ∈ (y^n, y^{n+1}].

LaTeX

$$$\forall x,y \in \mathbb{R}_{\ge 0},\ x \neq 0,\ 1 < y\Rightarrow\ exists\ n \in \mathbb{Z},\ x \in (y^n, y^{n+1}]$$$

Lean4

nonrec theorem exists_mem_Ioc_zpow {x : ℝ≥0} {y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) :
    ∃ n : ℤ, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1)) :=
  exists_mem_Ioc_zpow hx.bot_lt hy

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