support_indicator — Mathlib

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

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