of_discrete — Mathlib

English

In a finite discrete measurable space, every function f is in Lp for any p.

Русский

В конечном дискретном измеримом пространстве любая функция принадлежит Lp для любого p.

LaTeX

$$MemLp f p μ$$

Lean4

@[simp]
theorem of_discrete [DiscreteMeasurableSpace α] [Finite α] [IsFiniteMeasure μ] : MemLp f p μ :=
  let ⟨C, hC⟩ := Finite.exists_le (‖f ·‖₊);
  .of_bound .of_discrete C <| .of_forall hC

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