repr_reindex — Mathlib

English

The set of vectors obtained from the reindexed basis has the same range as the original basis.

Русский

Множество векторов, полученных из перебиндованного базиса, совпадает по диапазону с исходным базисом.

LaTeX

$$Set.range (b.reindex e) = Set.range b$$

Lean4

@[simp]
theorem repr_reindex : (b.reindex e).repr x = (b.repr x).mapDomain e :=
  DFunLike.ext _ _ <| by simp [repr_reindex_apply]

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