erase_def — Mathlib

English

The erase operation removes the i-th coordinate, producing a DFinsupp with support reduced by i and coordinates j ↦ f j.

Русский

Операция erase удаляет координату i, получая DFinsupp с опорой, уменьшенной на i, и координатами j ↦ f j.

LaTeX

$$$\\mathrm{erase}\\,i\\;f = \\mathrm{mk}(f.{\\mathrm{support}}.\\mathrm{erase}\\ i)\\; (\\lambda j, f j.1)$$$

Lean4

theorem erase_def (i : ι) (f : Π₀ i, β i) : f.erase i = mk (f.support.erase i) fun j => f j.1 :=
  by
  ext j
  by_cases h1 : j = i <;> by_cases h2 : f j ≠ 0 <;> simp at h2 <;> simp [h1, h2]

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