reindexFinsetRange — Mathlib

English

There is a basis reindexed by the finite set Finset.univ.image(b).

Русский

Существует базис, индексируемый конечным множеством Finset.univ.image(b).

LaTeX

$$$\\mathrm{reindexFinsetRange} : \\mathrm{Basis}(\\mathrm{Finset.univ.image}(b))\\ R\\ M.$$$

Lean4

/-- `b.reindexFinsetRange` is a basis indexed by `Finset.univ.image b`,
the finite set of basis vectors themselves. -/
def reindexFinsetRange : Basis (Finset.univ.image b) R M :=
  b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv (by simp))

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