reindex_appTop_coord — Mathlib

English

For i: m → n and j ∈ m, the i-th coordinate under reindex respects composition: (reindex i S).appTop(coord S j) = coord S (i j).

Русский

Для i: m → n и j ∈ m, координата i-го индекса сохраняет композицию: (reindex i S).appTop(coord S j) = coord S (i j).

LaTeX

$$$(\\mathrm{reindex}\\ i\\ S).{\\rm appTop}(\\mathrm{coord}_S(j)) = \\mathrm{coord}_S(i(j)).$$$

Lean4

@[simp]
theorem reindex_appTop_coord {n m : Type v} (i : m → n) (S : Scheme.{max u v}) (j : m) :
    (reindex i S).appTop (coord S j) = coord S (i j) :=
  homOfVector_appTop_coord _ _ _

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