measurableSet_eball

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

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

English

In a pseudo-EMetric space, the ball with radius ε is a measurable set.

Русский

В псевдометрическом пространстве э_ball множество измеримо.

LaTeX

$$$\\operatorname{MeasurableSet}(\\mathrm{EMetric.ball}(x, \\varepsilon)).$$$

Lean4

@[measurability]
theorem measurableSet_eball : MeasurableSet (EMetric.ball x ε) :=
  EMetric.isOpen_ball.measurableSet

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

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

Разделы

Аффилиация

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