English
The indicator function commutes with the Real embedding: taking the Real value after indicator equals the indicator of the Real-valued function.
Русский
Индикаторная функция сохраняет отображение в действительные числа: преобразование в Real после индикатора равно индикатору преобразованной функции.
LaTeX
$$$(((s.indicator f a) \\\\text{ : } \\\\mathbb{R}_{\\\\ge 0}) \\\\text{ : } \\\\mathbb{R}) = s.\\\\text{indicator} (\\\\lambda x. \\\\uparrow f x) a.$$$
Lean4
@[simp, norm_cast]
theorem coe_indicator {α} (s : Set α) (f : α → ℝ≥0) (a : α) :
((s.indicator f a : ℝ≥0) : ℝ) = s.indicator (fun x => ↑(f x)) a :=
(toRealHom : ℝ≥0 →+ ℝ).map_indicator _ _ _
