negPart_smul_of_nonneg

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

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

← MathLib Explorer

English

The positive part is nonnegative: a⁺ ≥ 0.

Русский

Положительная часть неотрицательна: a⁺ ≥ 0.

LaTeX

$$$0 \le a^+$$$

Lean4

theorem negPart_smul_of_nonneg {r : ℝ} (hr : 0 ≤ r) {a : A} : (r • a)⁻ = r • a⁻ := by
  conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonpos (by simpa), neg_neg]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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