real_smul_posPart_neg — Mathlib

English

If r > 0, the positive part under a positive scaling corresponds to the negative part of the original.

Русский

Если r > 0, при положительном масштабе положительная часть относится к отрицательной части исходного.

LaTeX

$$$ r > 0 \implies (r \cdot j).\mathrm{posPart} = (-r).toNNReal \cdot j.\mathrm{negPart} $$$

Lean4

theorem real_smul_posPart_neg (r : ℝ) (hr : r < 0) : (r • j).posPart = (-r).toNNReal • j.negPart := by
  rw [real_smul_def, ← smul_negPart, if_neg (not_le.2 hr), neg_posPart]

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