reindex — Mathlib

English

A reindexed line is mono for C if and only if the original line is mono for the conjugated color map: l.IsMono C reindexed ⇔ l.IsMono (λ x, C (eα ∘ x ∘ eι⁻¹)).

Русский

Линия после переиндексации моно-относительно C тогда и только тогда, когда исходная линия моно относительно преобразованной карты цвета.

LaTeX

$$$\\text{IsMono }(l.reindex\\ eη\\ eα\\ eι\\,C) \\iff \\text{IsMono }(l,\\ x \\mapsto C\\big(eα\\circ x\\circ eι^{-1}\\big)).$$$

Lean4

protected theorem reindex {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι → α) → κ} (hl : l.IsMono C) :
    (l.reindex eη eα eι).IsMono fun x ↦ C <| eα.symm ∘ x ∘ eι := by simp [reindex_isMono, Function.comp_assoc];
  simpa [← Function.comp_assoc]

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