single_apply — Mathlib

English

For any a, a' ∈ α and b ∈ M, the value of the finitely supported function single a b at a' is b if a = a', and 0 otherwise; i.e., single a b a' = if a = a' then b else 0.

Русский

Для любых a, a' ∈ α и b ∈ M значение функции finite поддержки single a b в точке a' равно b, если a = a', иначе 0;

LaTeX

$$$$\\forall a,a'\\in \\alpha,\\; \\forall b\\in M:\\quad (\\text{single } a\\, b)(a') = \\begin{cases} b, & \\text{если } a=a', \\\\ 0, & \\text{иначе}.\\end{cases}$$$$

Lean4

theorem single_apply [Decidable (a = a')] : single a b a' = if a = a' then b else 0 := by
  classical simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]

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