toNNReal_mul

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#Real.toNNReal_mul

← MathLib Explorer

English

If p ≥ 0, then toNNReal(p*q) = toNNReal(p) * toNNReal(q) for all q.

Русский

Если p ≥ 0, то toNNReal(p*q) = toNNReal(p) * toNNReal(q).

LaTeX

$$$$ p \ge 0 \implies \operatorname{toNNReal}(p q) = \operatorname{toNNReal}(p) \cdot \operatorname{toNNReal}(q). $$$$

Lean4

theorem toNNReal_mul {p q : ℝ} (hp : 0 ≤ p) : Real.toNNReal (p * q) = Real.toNNReal p * Real.toNNReal q :=
  NNReal.eq <| by simp [mul_max_of_nonneg, hp]

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

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

Разделы

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

Аффилиация

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