eq_snoc_eraseLast — Mathlib

English

For a Composition Series s of positive length, s is equal to the snoc (eraseLast s) s.last with the appropriate maximality witness.

Русский

Для композиционной последовательности s положительной длины равенство выполняется: s = snoc (eraseLast s) s.last с подходящим доказательством максимальности.

LaTeX

$$$s = \\text{snoc}(\\text{eraseLast}(s), s.last, \\text{isMaximal\_eraseLast\_last}(h)).$$$

Lean4

theorem eq_snoc_eraseLast {s : CompositionSeries X} (h : 0 < s.length) :
    s = snoc (eraseLast s) s.last (isMaximal_eraseLast_last h) :=
  by
  ext x
  simp only [mem_snoc, mem_eraseLast h, ne_eq]
  by_cases h : x = s.last <;> simp [*, s.last_mem]

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