English
For a measurable set s and a simple function f, the support of f.piecewise(s, hs, 0) is s intersect the support of f.
Русский
Для измеримого множества s и простой функции f опорная область f.piecewise(s, hs, 0) равна пересечению s и опоры f.
LaTeX
$$$$ \\operatorname{Function.support}\\big(f.\\text{piecewise}(s, hs, \\text{const } \\alpha 0)\\big) = s \\cap \\operatorname{Function.support}(f). $$$$
Lean4
theorem support_indicator [Zero β] {s : Set α} (hs : MeasurableSet s) (f : α →ₛ β) :
Function.support (f.piecewise s hs (SimpleFunc.const α 0)) = s ∩ Function.support f :=
Set.support_indicator