inv_pow_le_inv_pow_of_le

Mathlib.Algebra.Order.Field.Basic

URI: https://scilib.ai/kg/mathlib#inv_pow_le_inv_pow_of_le

← MathLib Explorer

English

For 1 ≤ a, the inverse power a^n has nonincreasing order with respect to n.

Русский

Для 1 ≤ a закон обратной степени a^n не возрастает по n.

LaTeX

$$$1 \le a \Rightarrow m \le n \Rightarrow (a^{n})^{-1} \le (a^{m})^{-1}$$$

Lean4

theorem inv_pow_le_inv_pow_of_le (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) : (a ^ n)⁻¹ ≤ (a ^ m)⁻¹ := by
  convert one_div_pow_le_one_div_pow_of_le a1 mn using 1 <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru