aestronglyMeasurable_dirac — Mathlib

English

For any a in α, any measurable f: α → β, the map x ↦ f(a) is AEStronglyMeasurable with respect to the dirac measure at a.

Русский

Для любого a в α, любой измеримый f: α → β, отображение x ↦ f(a) является AES-сильно измеримым относительно меры Дирака в точке a.

LaTeX

$$$[MeasurableSingletonClass \ α] \Rightarrow AEStronglyMeasurable(f, \text{dirac}(a))$$$

Lean4

@[fun_prop]
theorem aestronglyMeasurable_dirac [MeasurableSingletonClass α] {a : α} {f : α → β} :
    AEStronglyMeasurable f (Measure.dirac a) :=
  ⟨fun _ ↦ f a, stronglyMeasurable_const, ae_eq_dirac f⟩

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