posPart_smul_of_nonneg

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

URI: https://scilib.ai/kg/mathlib#CFC.posPart_smul_of_nonneg

English

PosPart respects nonnegative scalar action: for r ∈ NNReal, posPart((r) a) = r posPart(a).

Русский

Для r ∈ NNReal выполняется posPart(r a) = r posPart(a).

LaTeX

$$$posPart((r) a) = r \; posPart(a) \text{ for } r \in \mathbb{NNReal}$$$

Lean4

theorem posPart_smul_of_nonneg {r : ℝ} (hr : 0 ≤ r) {a : A} : (r • a)⁺ = r • a⁺ :=
  posPart_smul (r := ⟨r, hr⟩)

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

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

Разделы

Аффилиация

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