coe_negPart

Mathlib.MeasureTheory.Integral.Bochner.L1

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

English

The negative part aligns with the Lp negative part under the same coercion.

Русский

Отрицательная часть согласуется с отрицательной частью Lp при той же коэрцировке.

LaTeX

$$$$ (\\text{coe}_{\\text{negPart}})(f) = \\text{Lp.negPart}(f) $$$$

Lean4

@[norm_cast]
theorem coe_negPart (f : α →₁ₛ[μ] ℝ) : (negPart f : α →₁[μ] ℝ) = Lp.negPart (f : α →₁[μ] ℝ) :=
  rfl

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

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

Разделы

Аффилиация

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