aefinStronglyMeasurable_zero — Mathlib

English

For any α, β with a topological space structure, the zero function is AEFinStronglyMeasurable.

Русский

Для любых α, β с топологическим пространством нулевая функция является AEFinStronglyMeasurable.

LaTeX

$$$ \\text{AEFinStronglyMeasurable}\\ (0: α \\to β) \\ μ $$$

Lean4

theorem aefinStronglyMeasurable_zero {α β} {_ : MeasurableSpace α} (μ : Measure α) [Zero β] [TopologicalSpace β] :
    AEFinStronglyMeasurable (0 : α → β) μ :=
  ⟨0, finStronglyMeasurable_zero, EventuallyEq.rfl⟩

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