single_eq_indicator

Mathlib.Data.Finsupp.Indicator

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

← MathLib Explorer

English

For any i, b, we have single i b = indicator({i})(λ x ∈ {i}, b).

Русский

Для любого i, b верно: single i b = indicator({i})(λ x ∈ {i}, b).

LaTeX

$$$\\operatorname{single}_i(b) = \\operatorname{indicator}(\{i\\}, \\lambda x\\in\\{i\\}, b)$$$

Lean4

theorem single_eq_indicator (b : α) : single i b = indicator { i } (fun _ _ => b) := by
  classical
  ext j
  simp [single_apply, indicator_apply, @eq_comm _ j]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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