mulIndicator_apply_eq_if

Mathlib.Topology.LocallyConstant.Basic

URI: https://scilib.ai/kg/mathlib#LocallyConstant.mulIndicator_apply_eq_if

English

The value of the mulIndicator function at a point a is f(a) if a ∈ U and is 1 otherwise.

Русский

Значение mulIndicator в точке a есть f(a) при a ∈ U и 1 вне U.

LaTeX

$$$ (f.mulIndicator hU)(a) = \\begin{cases} f(a), & a \\in U; \\\\ 1, & a \\notin U. \\end{cases} $$$

Lean4

@[to_additive]
theorem mulIndicator_apply_eq_if (hU : IsClopen U) : mulIndicator f hU a = if a ∈ U then f a else 1 :=
  Set.mulIndicator_apply U f a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru