negPart_neg

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

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

English

For any a, the relation between negPart and posPart is given by the identity negPart a = - posPart (-a).

Русский

Для любого a выполняется равенство negPart(a) = - posPart(-a).

LaTeX

$$$\text{negPart}(a) = -\text{posPart}(-a)$$$

Lean4

@[simp]
theorem negPart_neg (a : A) : (-a)⁻ = a⁺ := by rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]

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

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

Разделы

Аффилиация

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