of — Mathlib · SciLib

English

The i-th component of the j-th left-embedded element equals b if j=i, otherwise it is 0.

Русский

i-я компонента элемента lof_j(b) равна b, если j=i, иначе 0.

LaTeX

$$$\\mathrm{component}_i(\\mathrm{lof}_j(b)) = \\begin{cases} b, & i=j, \\\\ 0, & i\\neq j. \\end{cases}$$$

Lean4

theorem of [DecidableEq ι] (i j : ι) (b : M j) :
    component R ι M i ((lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0 :=
  DFinsupp.single_apply

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