inj — Mathlib

English

Within a composition series, equality of elements at indices implies equality of indices.

Русский

Если два индекса в серии дают одинаковый элемент, то сами индексы равны.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X] (s : \\mathrm{CompositionSeries}\\ X)\\ {i j : \\mathrm{Fin}\\ s.length.succ},\\ (s i = s j) \\iff i = j.$$$

Lean4

@[simp]
protected theorem inj (s : CompositionSeries X) {i j : Fin s.length.succ} : s i = s j ↔ i = j :=
  s.injective.eq_iff

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