integrable_neg_iff

Mathlib.MeasureTheory.Function.L1Space.Integrable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.integrable_neg_iff

English

Integrability is preserved under negation: Integrable(-f) ⇔ Integrable(f).

Русский

Интегрируемость сохраняется под отрицанием: Integrable(-f) ⇔ Integrable(f).

LaTeX

$$$\\mathrm{Integrable}(-f, μ) \\iff \\mathrm{Integrable}(f, μ)$$$

Lean4

@[simp]
theorem integrable_neg_iff {f : α → β} : Integrable (-f) μ ↔ Integrable f μ :=
  ⟨fun h => neg_neg f ▸ h.neg, Integrable.neg⟩

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

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

Разделы

Аффилиация

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