cast_le_pow_sub_div_sub — Mathlib

English

For any a > 1 in a ordered field α and any natural n, we have n ≤ a^n / (a − 1).

Русский

Для любого a > 1 в упорядоченном поле α и любого натурального n выполняется неравенство n ≤ a^n / (a − 1).

LaTeX

$$$\forall a \in \alpha,\ a > 1,\forall n \in \mathbb{N},\ (n \le a^{n} / (a-1))$$$

Lean4

/-- Bernoulli's inequality reformulated to estimate `(n : α)`. -/
theorem cast_le_pow_sub_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ (a ^ n - 1) / (a - 1) :=
  (le_div_iff₀ (sub_pos.2 H)).2 <|
    le_sub_left_of_add_le <| one_add_mul_sub_le_pow ((neg_le_self zero_le_one).trans H.le) _

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