indicator_meas_zero — Mathlib

English

If μ s = 0 then indicator s f =ᵐ[μ] 0.

Русский

Если мерa μ измерения множества s равна 0, то sf равняется нулю почти наверху.

LaTeX

$$$ \\mathrm{indicator\_meas\_zero} \\quad (\\mu s = 0) \\Rightarrow \\text{indicator } s\\, f =_{\\mathrm{ae}}^{\\mu} 0 $$$

Lean4

theorem indicator_meas_zero (hs : μ s = 0) : indicator s f =ᵐ[μ] 0 :=
  indicator_empty' f ▸ indicator_ae_eq_of_ae_eq_set (ae_eq_empty.2 hs)

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