length_pos_of_head_eq_head_of_last_eq_last_of_length_pos

English

If two Composition Series have equal heads and equal lasts and the first has positive length, then the second also has positive length.

Русский

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

LaTeX

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

Lean4

theorem length_pos_of_head_eq_head_of_last_eq_last_of_length_pos {s₁ s₂ : CompositionSeries X} (hb : s₁.head = s₂.head)
    (ht : s₁.last = s₂.last) : 0 < s₁.length → 0 < s₂.length :=
  not_imp_not.1
    (by
      simpa only [pos_iff_ne_zero, ne_eq, Decidable.not_not] using
        length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb.symm ht.symm)

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