toFinsupp_apply — Mathlib

English

For every i, the value of l.toFinsupp at i equals the i-th element of l, with default 0 if i is beyond the end.

Русский

Для каждого i значение l.toFinsupp на i равно i-й элемент списка, при этом если i выходит за пределы длины, берётся 0.

LaTeX

$$$$ (l\\toFinsupp : \\mathbb{N} \\to M)(i) = l_i,0. $$$$

Lean4

@[simp, norm_cast]
theorem toFinsupp_apply (i : ℕ) : (l.toFinsupp : ℕ → M) i = l.getD i 0 :=
  rfl

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