posPart_def

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

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

English

The positive part is defined by the functional calculus of t ↦ t⁺: a⁺ = cfcₙ (t^+) a.

Русский

Положительная часть задаётся через функциональный калькулятор: a⁺ = cfcₙ (t^+) a.

LaTeX

$$$a^+ = \mathrm{cfc}_{\mathbb{R}}(t \mapsto t^+)(a)$$$

Lean4

theorem posPart_def (a : A) : a⁺ = cfcₙ (·⁺ : ℝ → ℝ) a :=
  rfl

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

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

Разделы

Аффилиация

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