negPart

Mathlib.MeasureTheory.Integral.Bochner.L1

URI: https://scilib.ai/kg/mathlib#MeasureTheory.L1.SimpleFunc.negPart

English

PosPart is defined as the positive part of a real-valued object within L1-simple-function context.

Русский

PosPart — положительная часть вещественного значения в контексте простой функции L1.

LaTeX

$$$$ \\text{posPart}(f) = \\text{positive part of } f. $$$$

Lean4

/-- Negative part of a simple function in L1 space. -/
def negPart (f : α →₁ₛ[μ] ℝ) : α →₁ₛ[μ] ℝ :=
  posPart (-f)

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

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

Разделы

Аффилиация

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