single_eq_update — Mathlib

English

The function single a b is equal to the update of the constant zero function at a by b.

Русский

Функция single a b равна обновлению нулевой функции на координате a значением b.

LaTeX

$$$$\\text{single } a\\, b = \\operatorname{update}(0)\\, a\\, b.$$$$

Lean4

theorem single_eq_update [DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Function.update (0 : _) a b := by
  classical rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]

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