English
The indicator of a constant nonzero value on a set s is measurable iff s is measurable.
Русский
Индикатор константы b ≠ 0 на множество s измерим тогда и только тогда, когда s измеримо.
LaTeX
$$$[\\text{Zero } \\beta] [\\text{MeasurableSingletonClass } \\beta] (b) [\\text{NeZero } b] :\\ Measurable (s.indicator (fun x \\mapsto b)) \\iff \\ MeasurableSet s$$$
Lean4
/-- The measurability of a set `A` is equivalent to the measurability of the indicator function
which takes a constant value `b ≠ 0` on a set `A` and `0` elsewhere. -/
theorem measurable_indicator_const_iff [Zero β] [MeasurableSingletonClass β] (b : β) [NeZero b] :
Measurable (s.indicator (fun (_ : α) ↦ b)) ↔ MeasurableSet s :=
by
constructor <;> intro h
· convert h (MeasurableSet.singleton (0 : β)).compl
ext a
simp [NeZero.ne b]
· exact measurable_const.indicator h
