measurableSet_mulSupport — Mathlib

English

The set where a strongly measurable function is nonzero is measurable.

Русский

Множество точек, на которых функция не равна нулю, измеримо.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \text{MeasurableSet}(\mathrm{mulSupport}(f))$$$

Lean4

@[to_additive]
nonrec theorem measurableSet_mulSupport {m : MeasurableSpace α} [One β] [TopologicalSpace β] [MetrizableSpace β]
    (hf : StronglyMeasurable f) : MeasurableSet (mulSupport f) :=
  by
  borelize β
  exact measurableSet_mulSupport hf.measurable

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