exists_pow_lt_of_lt_one — Mathlib

English

For a,b ∈ ℝ≥0 with a > 0 and b < 1, there exists n ∈ ℕ such that b^n < a.

Русский

Пусть a,b ∈ ℝ≥0 и a > 0, b < 1. Существует n ∈ ℕ такое, что b^n < a.

LaTeX

$$$\forall a,b \in \mathbb{R}_{\ge 0},\ a > 0,\ b < 1\ \Rightarrow\ \exists n \in \mathbb{N},\ b^n < a$$$

Lean4

nonrec theorem exists_pow_lt_of_lt_one {a b : ℝ≥0} (ha : 0 < a) (hb : b < 1) : ∃ n : ℕ, b ^ n < a := by
  simpa only [← coe_pow, NNReal.coe_lt_coe] using exists_pow_lt_of_lt_one (NNReal.coe_pos.2 ha) (NNReal.coe_lt_coe.2 hb)

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