zpow_le_one_of_nonpos — Mathlib

English

If n ≤ 0 and x ≥ 1, then x^n ≤ 1.

Русский

Если n ≤ 0 и x ≥ 1, то x^n ≤ 1.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\; n \\le 0 \\Rightarrow \\forall x \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; 1 \\le x \\Rightarrow x^n \\le 1$$$

Lean4

theorem zpow_le_one_of_nonpos {n : ℤ} (hn : n ≤ 0) {x : ℝ≥0∞} (hx : 1 ≤ x) : x ^ n ≤ 1 :=
  by
  obtain ⟨m, rfl⟩ := neg_surjective n
  lift m to ℕ using by simpa using hn
  rw [← ENNReal.inv_zpow', ENNReal.inv_zpow, ENNReal.inv_le_one]
  exact mod_cast one_le_pow₀ hx

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