reindexFinsetRange_repr_self — Mathlib

English

For i ∈ ι, the repr of b.reindexFinsetRange at b i is the singleton vector at b i.

Русский

Для i ∈ ι представление b.reindexFinsetRange на b i есть единичный вектор, соответствующий b i.

LaTeX

$$$b.\\mathrm{reindexFinsetRange.repr}(b i) = \\mathrm{Finsupp.single}⟨b i, \\text{mem\_image\_of\_mem}(b,\\mathrm{mem\_univ}(i))\\rangle\\, 1.$$$

Lean4

theorem reindexFinsetRange_repr_self (i : ι) :
    b.reindexFinsetRange.repr (b i) = Finsupp.single ⟨b i, Finset.mem_image_of_mem b (Finset.mem_univ i)⟩ 1 :=
  by
  ext ⟨bi, hbi⟩
  rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self]
  simp [Finsupp.single_apply]

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