indicator_of_mem

Mathlib.Data.Finsupp.Indicator

URI: https://scilib.ai/kg/mathlib#Finsupp.indicator_of_mem

English

If i ∈ s, then indicator s f i = f i hi, i.e., the value agrees with f on the membership.

Русский

Если i ∈ s, то indicator s f i = f i hi, то есть значение совпадает с f на принадлежности.

LaTeX

$$$indicator(s,f)(i) = f(i) \\quad \\text{for } i\\in s$$$

Lean4

theorem indicator_of_mem (hi : i ∈ s) (f : ∀ i ∈ s, α) : indicator s f i = f i hi :=
  @dif_pos _ (id _) hi _ _ _

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

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

Разделы

Аффилиация

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