posPart_smul — Mathlib

English

The posPart behaves well with scalar multiplication: (r a)⁺ = r a⁺ for nonnegative reals r ≥ 0 (in the appropriate scalar context).

Русский

Положительная часть сохраняет скаляры: (r a)⁺ = r a⁺ при r ≥ 0.

LaTeX

$$$ (r \cdot a)^+ = r \cdot a^+ $$$

Lean4

@[simp]
theorem posPart_smul {r : ℝ≥0} {a : A} : (r • a)⁺ = r • a⁺ :=
  by
  by_cases ha : IsSelfAdjoint a
  · simp only [CFC.posPart_def, NNReal.smul_def]
    rw [← cfcₙ_comp_smul .., ← cfcₙ_smul ..]
    refine cfcₙ_congr fun x hx ↦ ?_
    simp [_root_.posPart_def, mul_max_of_nonneg]
  · obtain (rfl | hr) := eq_or_ne r 0
    · simp
    · have := (not_iff_not.mpr <| (IsSelfAdjoint.all r).smul_iff hr.isUnit (x := a)) |>.mpr ha
      simp [CFC.posPart_def, cfcₙ_apply_of_not_predicate a ha, cfcₙ_apply_of_not_predicate _ this]

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