real_smul_neg

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

English

If r < 0, then r • j equals the negated NNReal multiple of j.

Русский

Если r < 0, то r • j равно отрицанию NNReal умножения на j.

LaTeX

$$$ r < 0 \implies r \cdot j = -((-r)^{\mathrm{NNReal}} \cdot j) $$$

Lean4

theorem real_smul_neg (r : ℝ) (hr : r < 0) : r • j = -((-r).toNNReal • j) :=
  dif_neg (not_le.2 hr)

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

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

Разделы

Аффилиация

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