measurableSet_ball — Mathlib

English

In a metric space with opens-measurable structure, every open ball B(x, ε) is a measurable set.

Русский

В метрическом пространстве с открытым измеримым пространством любая открытая шара B(x, ε) является измеримым множеством.

LaTeX

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

Lean4

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

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