single_eq_set_indicator — Mathlib

English

The function single a b is equal to the indicator function of the singleton {a} sending a to b and all other elements to 0.

Русский

Функция single a b равна индикаторной функции множества {a}, возвращающей значение b на a и 0 в остальных случаях.

LaTeX

$$$$\\text{single } a\\, b = \\mathbf{1}_{\\{a\\}}\\cdot b,$$$$

Lean4

theorem single_eq_set_indicator : ⇑(single a b) = Set.indicator { a } fun _ => b := by
  classical
  ext
  simp [single_apply, Set.indicator, @eq_comm _ a]

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