English
Reindexing preserves monotonicity: IsMono C on the reindexed line is equivalent to IsMono of C composed with the isomorphisms, i.e., IsMono C (l.reindex eη eα eι) ⇔ IsMono (λ x, C (eα ∘ x ∘ eι⁻¹)) l.
Русский
Переиндексация сохраняет монотонность: IsMono C на переиндексированной линии эквивалентно IsMono на исходной линии с композициями эквиваленций.
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
@[simp]
theorem reindex_isMono {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι' → α') → κ} :
(l.reindex eη eα eι).IsMono C ↔ l.IsMono fun x ↦ C <| eα ∘ x ∘ eι.symm :=
by
simp only [IsMono, funext (reindex_apply _ _ _ _ _), coe_apply]
exact exists_congr fun c ↦ (eη.arrowCongr eα).symm.forall_congr <| by aesop
