measurable_dist — Mathlib

English

If f, g: β → α are measurable, then the function b ↦ dist(f(b), g(b)) is measurable.

Русский

Если f, g: β → α измеримы, то функция b ↦ dist(f(b), g(b)) измерима.

LaTeX

$$$\\text{Measurable}(f) \\rightarrow \\text{Measurable}(g) \\rightarrow \\text{Measurable}(b \\mapsto \\operatorname{dist}(f(b), g(b))).$$$

Lean4

@[measurability]
theorem measurable_dist : Measurable fun p : α × α => dist p.1 p.2 :=
  continuous_dist.measurable

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