measure_preimage_lt_top_of_integrable

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

← MathLib Explorer

English

If f is integrable and x ≠ 0, then μ(f^{-1}({x})) < ∞.

Русский

Если f интегрируема и x ≠ 0, то μ(f^{-1}({x})) < ∞.

LaTeX

$$$\\mathrm{Integrable}(f,\\mu) \\Rightarrow \\forall x\\,(x\\neq 0\\Rightarrow \\mu(f^{-1}(\\{x\\}))<\\infty)$$$

Lean4

theorem measure_preimage_lt_top_of_integrable (f : α →ₛ E) (hf : Integrable f μ) {x : E} (hx : x ≠ 0) :
    μ (f ⁻¹' { x }) < ∞ :=
  integrable_iff.mp hf x hx

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

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

Разделы

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

Аффилиация

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