real_smul_nonneg

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

URI: https://scilib.ai/kg/mathlib#MeasureTheory.JordanDecomposition.real_smul_nonneg

English

If r ≥ 0, then r • j equals r’s NNReal version times j.

Русский

Если r ≥ 0, то r • j равно r приведённому к NNReal умножению на j.

LaTeX

$$$ r \ge 0 \implies r \cdot j = r^{\mathrm{NNReal}} \cdot j $$$

Lean4

theorem real_smul_nonneg (r : ℝ) (hr : 0 ≤ r) : r • j = r.toNNReal • j :=
  dif_pos hr

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

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

Разделы

Аффилиация

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