measurableSet_mulSupport — Mathlib

English

If f is measurable and β has a unit, then the multiplicative support set of f is measurable.

Русский

Если f измерима и β обладает единицей, то множество mulSupport(f) измеримо.

LaTeX

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

Lean4

@[to_additive (attr := measurability)]
theorem measurableSet_mulSupport [One β] [MeasurableSingletonClass β] (hf : Measurable f) :
    MeasurableSet (Function.mulSupport f) :=
  hf (measurableSet_singleton 1).compl

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