length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero

English

If two Composition Series have equal heads and equal lasts, then equality of their lengths follows from a zero length in one.

Русский

Если две композиционные последовательности имеют равные головы и концы, то равенство длин следует из нуля одной длины.

LaTeX

$$$\\forall s_1,s_2,\\; s_1.head = s_2.head \\land s_1.last = s_2.last \\land s_1.length = 0 \\Rightarrow s_2.length = 0.$$$

Lean4

theorem length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero {s₁ s₂ : CompositionSeries X}
    (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) (hs₁ : s₁.length = 0) : s₂.length = 0 :=
  by
  have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
    s₂.injective (hb.symm.trans ((congr_arg s₁ (Fin.ext (by simp [hs₁]))).trans ht)).symm
  simpa [Fin.ext_iff]

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