aemeasurable_id'' — Mathlib

English

The identity map id: α → α is AEMeasurable with respect to μ whenever the sigma-algebra is included appropriately (m ≤ m0).

Русский

Идентичный отображение id: α → α является АЕ-измеримым относительно μ при надлежащем включении сигма-алгебм.

LaTeX

$$$\\\\text{AEMeasurable(id,\\\\mu)}$$$

Lean4

theorem aemeasurable_id'' (μ : Measure α) {m : MeasurableSpace α} (hm : m ≤ m0) : @AEMeasurable α α m m0 id μ :=
  @Measurable.aemeasurable α α m0 m id μ (measurable_id'' hm)

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