finStronglyMeasurable_zero — Mathlib

English

The zero function is finitely strongly measurable for any measure μ.

Русский

Нулевая функция finitely strongly measurable для любой меры μ.

LaTeX

$$$\text{FinStronglyMeasurable}(0 : \alpha \to \beta)\, \mu$$$

Lean4

theorem finStronglyMeasurable_zero {α β} {m : MeasurableSpace α} {μ : Measure α} [Zero β] [TopologicalSpace β] :
    FinStronglyMeasurable (0 : α → β) μ :=
  ⟨0, by simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero, measure_empty, zero_lt_top, forall_const],
    fun _ => tendsto_const_nhds⟩

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