reindex — Mathlib

English

Equivalences of the index set induce equivalences of orientations.

Русский

Эквивалентности множеств индексов порождают эквивалентности ориентаций.

LaTeX

$$$\text{reindex}: (e: \iota \simeq \iota') \;:\; Orientation R M \iota \simeq Orientation R M \iota'.$$$

Lean4

/-- An equivalence between indices implies an equivalence between orientations. -/
def reindex (e : ι ≃ ι') : Orientation R M ι ≃ Orientation R M ι' :=
  Module.Ray.map <| AlternatingMap.domDomCongrₗ R e

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