instNegPart

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

URI: https://scilib.ai/kg/mathlib#CStarAlgebra.instNegPart

English

There is a PosPart structure on A given by posPart := cfcₙ (·⁺ : ℝ → ℝ).

Русский

Существует структура PosPart на A, заданная posPart = cfcₙ (t⁺).

LaTeX

$$$\text{PosPart} \; A \text{ defined by } \text{posPart} := cfcₙ (\cdot^+ : \mathbb{R} \to \mathbb{R})$$$

Lean4

noncomputable instance : NegPart A where negPart := cfcₙ (·⁻ : ℝ → ℝ)

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

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

Разделы

Аффилиация

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