indicator_apply — Mathlib

English

Indicator s f i equals f i hi if i ∈ s, else 0; i.e., a closed form for the evaluation.

Русский

Indicator s f i равняется f i hi если i ∈ s, иначе 0; то есть явное выражение для значения.

LaTeX

$$$indicator(s,f)(i)=\\begin{cases} f(i) & i\\in s \\\\ 0 & i\\notin s\\end{cases}$$$

Lean4

@[simp]
theorem indicator_apply [DecidableEq ι] : indicator s f i = if hi : i ∈ s then f i hi else 0 :=
  by
  simp only [indicator, ne_eq, coe_mk]
  congr

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