MeasurableSet — Mathlib

English

MeasurableSet s is the predicate that s is measurable with respect to the ambient measure space on α.

Русский

MeasurableSet s — это предикат, означающий, что множество s измеримо относительно окружающего пространственного пространства меры на α.

LaTeX

$$$\text{MeasurableSet}(s) \;\text{is defined as} \; s \in \mathcal{M}$, где $\mathcal{M}$ — базовая сигма-алгебра на $\alpha$.$$

Lean4

/-- `MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`) -/
def MeasurableSet [MeasurableSpace α] (s : Set α) : Prop :=
  ‹MeasurableSpace α›.MeasurableSet' s

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