snoc_eraseLast_last — Mathlib

English

If s.eraseLast.last is maximal below s.last, then s.eraseLast.snoc s.last h = s.

Русский

Если s.eraseLast.last максимален ниже s.last, то s.eraseLast.snoc s.last h = s.

LaTeX

$$$\\text{If } IsMaximal(s.eraseLast.last, s.last) \\text{ then } s.eraseLast.snoc s.last h = s.$$$

Lean4

@[simp]
theorem snoc_eraseLast_last {s : CompositionSeries X} (h : IsMaximal s.eraseLast.last s.last) :
    s.eraseLast.snoc s.last h = s :=
  have h : 0 < s.length :=
    Nat.pos_of_ne_zero (fun hs => ne_of_gt (lt_of_isMaximal h) <| by simp [last, Fin.ext_iff, hs])
  (eq_snoc_eraseLast h).symm

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