aemeasurable — Mathlib

English

For κ a kernel and μ a measure on α, κ is almost everywhere μ-measurable; i.e., the map a ↦ κ a is measurably well-behaved μ-almost everywhere.

Русский

Пусть κ — ядро, μ — мера на α. Тогда отображение a ↦ κ a измеримо почти всюду по μ.

LaTeX

$$$\mathrm{AEMeasurable}(\kappa, \mu)$$$

Lean4

theorem aemeasurable (κ : Kernel α β) {μ : Measure α} : AEMeasurable κ μ :=
  κ.measurable.aemeasurable

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