cast_le_pow_div_sub — Mathlib

English

For any a > 1 in a ordered ring α 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 \in α) \le (a^{n} / (a-1))$$$

Lean4

/-- For any `a > 1` and a natural `n` we have `n ≤ a ^ n / (a - 1)`. See also
`Nat.cast_le_pow_sub_div_sub` for a stronger inequality with `a ^ n - 1` in the numerator. -/
theorem cast_le_pow_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ a ^ n / (a - 1) :=
  (n.cast_le_pow_sub_div_sub H).trans <| div_le_div_of_nonneg_right (sub_le_self _ zero_le_one) (sub_nonneg.2 H.le)

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