eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero

English

If two Composition Series share the same head and last, and one has length zero, then the two series are equal.

Русский

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

LaTeX

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

Lean4

theorem eq_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₁0 : s₁.length = 0) : s₁ = s₂ :=
  by
  have : ∀ x, x ∈ s₁ ↔ x = s₁.last := fun x =>
    ⟨fun hx => subsingleton_of_length_eq_zero hs₁0 hx s₁.last_mem, fun hx => hx.symm ▸ s₁.last_mem⟩
  have : ∀ x, x ∈ s₂ ↔ x = s₂.last := fun x =>
    ⟨fun hx =>
      subsingleton_of_length_eq_zero (length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht hs₁0) hx
        s₂.last_mem,
      fun hx => hx.symm ▸ s₂.last_mem⟩
  ext
  simp [*]

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