real_smul_def — Mathlib

English

The real scalar action on a Jordan decomposition is given by the case distinction r ≥ 0 or r < 0 with the NNReal conversion.

Русский

Действие над разложением Джордана вещественным числом описывается знаковым разбиением: r ≥ 0 или r < 0 с преобразованием в NNReal.

LaTeX

$$$ r \cdot j = \begin{cases} r^{\mathrm{NNReal}} \cdot j, & r \ge 0, \\ -((-r)^{\mathrm{NNReal}} \cdot j), & r < 0. \end{cases} $$$

Lean4

theorem real_smul_def (r : ℝ) (j : JordanDecomposition α) :
    r • j = if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j) :=
  rfl

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