mul_rpow_of_nonneg

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

If z ≥ 0, then (x y)^z = x^z y^z for all ENNReal x,y.

Русский

Если z ≥ 0, то (x y)^z = x^z y^z для всех x,y ∈ ENNReal.

LaTeX

$$$$(x y)^{z} = x^{z} y^{z} \quad \text{при } z \ge 0$$$$

Lean4

theorem mul_rpow_of_nonneg (x y : ℝ≥0∞) {z : ℝ} (hz : 0 ≤ z) : (x * y) ^ z = x ^ z * y ^ z := by
  simp [hz.not_gt, mul_rpow_eq_ite]

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

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

Разделы

Аффилиация

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