sort_mk — Mathlib

English

If s is a nodup multiset, sorting the Finset built from s yields the same as sorting s as a multiset.

Русский

Если s — безповторное множество, то сортировка Finset, построенного из s, равна сортировке s как мультисета.

LaTeX

$$$ \mathrm{sort} (r, \langle s, h \rangle) = s.\mathrm{sort}(r) $$$

Lean4

@[simp]
theorem sort_mk {s : Multiset α} (h : s.Nodup) : sort r ⟨s, h⟩ = s.sort r :=
  rfl

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