exists_mem_Ico_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_Ico_zpow {x : ℝ≥0} {y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) :
    ∃ n : ℤ, x ∈ Set.Ico (y ^ n) (y ^ (n + 1)) :=
  exists_mem_Ico_zpow hx.bot_lt hy

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