erase_single — Mathlib

English

For any i, j and x ∈ β i, erase j (single i x) equals 0 if i = j, otherwise single i x.

Русский

Для любых i, j и x ∈ β i, erase j (single i x) равно 0, если i = j, иначе равен single i x.

LaTeX

$$$ \\mathrm{erase}_j (\\\\mathrm{single}_i x) = \\begin{cases} 0, & i = j \\\\ \\\\mathrm{single}_i x, & i \neq j. \\end{cases} $$$

Lean4

theorem erase_single (j : ι) (i : ι) (x : β i) : (single i x).erase j = if i = j then 0 else single i x := by
  rw [← filter_ne_eq_erase, filter_single, ite_not]

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