edist — Mathlib

English

If f,g: β → α are almost everywhere measurable with respect to μ, then the map a ↦ edist(f(a), g(a)) is AEMeasurable with respect to μ.

Русский

Если f,g: β → α — а.е.-измеримы по μ, то a ↦ edist(f(a), g(a)) — а.е.-измеримо по μ.

LaTeX

$$$AEMeasurable f \\mu \\; \\land \\; AEMeasurable g \\mu \\; \\Rightarrow \\; AEMeasurable (\\lambda a. edist (f a) (g a)) \\mu$$$

Lean4

@[measurability, fun_prop]
theorem edist {f g : β → α} {μ : Measure β} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    AEMeasurable (fun a => edist (f a) (g a)) μ :=
  (@continuous_edist α _).aemeasurable2 hf hg

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