aestronglyMeasurable_id — Mathlib

English

The identity function id: α → α is AEStronglyMeasurable with respect to any measure μ on α.

Русский

Идентичное отображение id: α → α является AEStronglyMeasurable относительно любой меры μ на α.

LaTeX

$$$AEStronglyMeasurable(id, \mu)$$$

Lean4

@[fun_prop, measurability]
theorem _root_.aestronglyMeasurable_id {α : Type*} [TopologicalSpace α] [PseudoMetrizableSpace α]
    {_ : MeasurableSpace α} [OpensMeasurableSpace α] [SecondCountableTopology α] {μ : Measure α} :
    AEStronglyMeasurable (id : α → α) μ :=
  aemeasurable_id.aestronglyMeasurable

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