aemeasurable_const' — Mathlib

English

If f is almost everywhere constant in the sense ∀ᵐ x ∀ᵐ y, f x = f y, then f is AEMeasurable.

Русский

Если функция почти всюду константна, то она AЕ-измерима.

LaTeX

$$$\forall^\text{ae} x, \forall^\text{ae} y, f(x) = f(y) \Rightarrow \mathrm{AEMeasurable}(f, \mu)$$$

Lean4

theorem aemeasurable_const' (h : ∀ᵐ (x) (y) ∂μ, f x = f y) : AEMeasurable f μ :=
  by
  rcases eq_or_ne μ 0 with (rfl | hμ)
  · exact aemeasurable_zero_measure
  · haveI := ae_neBot.2 hμ
    rcases h.exists with ⟨x, hx⟩
    exact ⟨const α (f x), measurable_const, EventuallyEq.symm hx⟩

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