pow_le_pow_left

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.pow_le_pow_left

English

For any a ≤ b in ENNReal and any n ∈ ℕ, a^n ≤ b^n.

Русский

Для любых a ≤ b в ENNReal и любого n ∈ ℕ верно a^n ≤ b^n.

LaTeX

$$$\forall a,b \in ENNReal, \; a \le b \Rightarrow \; a^n \le b^n$$$

Lean4

@[mono, gcongr]
protected theorem pow_le_pow_left {n : ℕ} (h : a ≤ b) : a ^ n ≤ b ^ n :=
  pow_le_pow_left' h n

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

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

Разделы

Аффилиация

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