measurable_infEdist

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

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

English

For fixed s ⊆ α, the function x ↦ infEdist(x, s) is measurable.

Русский

Для фиксированного s ⊆ α функция x ↦ infEdist(x, s) измерима.

LaTeX

$$$\\operatorname{Measurable}(x \\mapsto \\operatorname{infEdist}(x, s)).$$$

Lean4

@[measurability]
theorem measurable_infEdist {s : Set α} : Measurable fun x => infEdist x s :=
  continuous_infEdist.measurable

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

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

Разделы

Аффилиация

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