aemeasurable_congr — Mathlib

English

Let f,g: α → β. If f and g are equal μ-almost everywhere, then AEMeasurable f μ is equivalent to AEMeasurable g μ.

Русский

Пусть f,g: α → β. Если f и g равны μ-почти в каждой точке, то AEMeasurable f μ эквивалентна AEMeasurable g μ.

LaTeX

$$$f =_{\mu}^{\mathrm{a.e.}} g \Rightarrow (\mathrm{AEMeasurable} f \mu \iff \mathrm{AEMeasurable} g \mu)$$$

Lean4

theorem aemeasurable_congr (h : f =ᵐ[μ] g) : AEMeasurable f μ ↔ AEMeasurable g μ :=
  ⟨fun hf => AEMeasurable.congr hf h, fun hg => AEMeasurable.congr hg h.symm⟩

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