negPart_smul

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

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

English

The negPart also respects scalar multiplication: (r a)⁻ = r a⁻ for nonnegative r when considering the NegPart structure.

Русский

Отрицательная часть также сохраняет масштабирование: (r a)⁻ = r a⁻ для r ≥ 0.

LaTeX

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

Lean4

@[simp]
theorem negPart_smul {r : ℝ≥0} {a : A} : (r • a)⁻ = r • a⁻ := by simpa using posPart_smul (r := r) (a := -a)

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

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

Разделы

Аффилиация

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