measurable_edist

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

URI: https://scilib.ai/kg/mathlib#measurable_edist

English

The map p ↦ edist p.1 p.2 from α × α to ℝ≥0∞ is measurable.

Русский

Отображение p ↦ edist p.1 p.2 из α × α в ℝ≥0∞ измеримо.

LaTeX

$$$\\text{Measurable}(p \\mapsto \\operatorname{edist}(p_1, p_2)).$$$

Lean4

@[measurability]
theorem measurable_edist : Measurable fun p : α × α => edist p.1 p.2 :=
  continuous_edist.measurable

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru