injective — Mathlib

English

A composition series defines an injective map from its index set into X.

Русский

Серия компоновки задает инъективное отображение индексов в X.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ (s : \\mathrm{CompositionSeries}\\ X)\\ \\mathrm{Injective}\\ s.toFun.$$$

Lean4

protected theorem injective (s : CompositionSeries X) : Function.Injective s :=
  s.strictMono.injective

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