instPosPart — Mathlib

English

There exists a PosPart operation on A defined by applying the continuous functional calculus to t ↦ t⁺: a⁺ = cfcₙ (t⁺) a.

Русский

Существуют положительная часть элемента и её определение через непрерывный функциональный калькулятор: a⁺ = cfcₙ (t⁺) a.

LaTeX

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

Lean4

noncomputable instance : PosPart A where posPart := cfcₙ (·⁺ : ℝ → ℝ)

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