congr_ae — Mathlib

English

If f is measurable and f equals g almost everywhere, then g is measurable.

Русский

Если f измерима и равна g почти всюду, то g измерима.

LaTeX

$$$\mathrm{Measurable}(f) \land f =^{\mu}_{ae} g \Rightarrow \mathrm{Measurable}(g).$$$

Lean4

theorem _root_.Measurable.congr_ae {α β} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} [_hμ : μ.IsComplete]
    {f g : α → β} (hf : Measurable f) (hfg : f =ᵐ[μ] g) : Measurable g :=
  NullMeasurable.measurable_of_complete (NullMeasurable.congr hf.nullMeasurable hfg)

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