English
Two CompositionSeries are equal iff they have the same elements.
Русский
Две композиционные серии равны тогда и только тогда, когда у них совпадают элементы.
LaTeX
$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ {s_1,s_2 : \\mathrm{CompositionSeries}\\ X},\\ (\\forall x, x \\in s_1 \\iff x \\in s_2) \\to s_1 = s_2.$$$
Lean4
/-- Two `CompositionSeries` are equal if they have the same elements. See also `ext_fun`. -/
@[ext]
theorem ext {s₁ s₂ : CompositionSeries X} (h : ∀ x, x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂ :=
toList_injective <|
List.eq_of_perm_of_sorted
(by
classical
exact
List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup
(Finset.ext <| by simpa only [List.mem_toFinset, RelSeries.mem_toList]))
s₁.toList_sorted s₂.toList_sorted
