head_le — Mathlib

English

For any i, head ≤ s i.

Русский

Для любого индекса голова ≤ элемент серии на этом индексе.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ {s : \\mathrm{CompositionSeries}\\ X},\\ {i : \\mathrm{Fin}(s.length + 1)},\\mathrm{head}\\le s(i).$$$

Lean4

@[simp]
theorem head_le {s : CompositionSeries X} (i : Fin (s.length + 1)) : s.head ≤ s i :=
  s.strictMono.monotone (Fin.zero_le _)

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