edist — Mathlib

English

Let f,g: β → α be measurable. Then the map b ↦ edist(f(b), g(b)) is measurable.

Русский

Пусть f,g: β → α измеримы. Тогда отображение b ↦ edist(f(b), g(b)) измеримо.

LaTeX

$$$\\text{Measurable}(f) \\to \\text{Measurable}(g) \\to \\text{Measurable}(\\lambda b. edist (f\\,b) (g\\,b))$$$

Lean4

@[measurability, fun_prop]
theorem edist {f g : β → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun b => edist (f b) (g b) :=
  (@continuous_edist α _).measurable2 hf hg

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