coeFn_negPart

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.coeFn_negPart

← MathLib Explorer

English

For f in Lp, almost everywhere negPart f = -min(f,0).

Русский

Для f из Lp почти везде действует negPart f = -min(f,0).

LaTeX

$$$\forall f\; \mu\text{-a.e.}\; \negPart f = -\min(f,0)$$$

Lean4

theorem coeFn_negPart (f : Lp ℝ p μ) : ∀ᵐ a ∂μ, negPart f a = -min (f a) 0 :=
  (coeFn_negPart_eq_max f).mono fun a h => by rw [h, ← max_neg_neg, neg_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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