pow_right_anti₀ — Mathlib

English

For a ≥ 0 and a ≤ 1, the map n ↦ a^n is antitone on natural numbers.

Русский

Для a ≥ 0 и a ≤ 1 отображение n ↦ a^n антотонно по n.

LaTeX

$$$Antitone(n \\mapsto a^n).$$$

Lean4

theorem pow_right_anti₀ [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : Antitone (fun n : ℕ ↦ a ^ n) :=
  antitone_nat_of_succ_le fun n ↦ by
    have : ZeroLEOneClass M₀ := ⟨ha₀.trans ha₁⟩
    rw [← mul_one (a ^ n), pow_succ]
    exact mul_le_mul_of_nonneg_left ha₁ (pow_nonneg ha₀ n)

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