single_apply — Mathlib

English

The i'-th coordinate of the singleton at i is b when i' = i and 0 otherwise.

Русский

i'-я координата сингла на i равна b, если i' = i, и ноль иначе.

LaTeX

$$$(\mathrm{single}\ i\ b)_{i'} = \begin{cases} b, & i' = i \\ 0, & i' \neq i \end{cases}$$$

Lean4

@[simp]
theorem single_apply {i i' b} : (single i b : Π₀ i, β i) i' = if h : i = i' then Eq.recOn h b else 0 :=
  by
  rw [single_eq_pi_single, Pi.single, Function.update]
  simp [@eq_comm _ i i']

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