measurableSet_support — Mathlib

English

The support of a simple function is a measurable set when the ambient space is measurable.

Русский

Опорa простой функции является измеримым множеством, когда пространство измеримо.

LaTeX

$$$\\text{MeasurableSet}(\\operatorname{support} f)$$$

Lean4

theorem measurableSet_support [MeasurableSpace α] (f : α →ₛ β) : MeasurableSet (support f) :=
  by
  rw [f.support_eq]
  exact Finset.measurableSet_biUnion _ fun y _ => measurableSet_fiber _ _

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