aemeasurable_const — Mathlib

English

For any β and any μ on α, the constant function a ↦ b is almost everywhere measurable with respect to μ.

Русский

Для любых β и меры μ на α константная функция a ↦ b является AEMеасимируемой по отношению к μ.

LaTeX

$$$AEMeasurable \ (\lambda a:\\alpha. b) \mu$$$

Lean4

@[simp, fun_prop, measurability]
theorem aemeasurable_const {b : β} : AEMeasurable (fun _a : α => b) μ :=
  measurable_const.aemeasurable

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