toFinset_eq_of_perm

Mathlib.Data.Finset.Dedup

URI: https://scilib.ai/kg/mathlib#List.toFinset_eq_of_perm

English

If l is permuted to l', then their toFinsets are equal.

Русский

Если список л может быть приведен к l' перестановкой, то их toFinsets равны.

LaTeX

$$$\\forall {l l' : \\mathsf{List}\\,\\alpha},\\; l \\sim l' \\rightarrow l.toFinset = l'.toFinset$$$

Lean4

theorem toFinset_eq_of_perm (l l' : List α) (h : l ~ l') : l.toFinset = l'.toFinset :=
  toFinset_eq_iff_perm_dedup.mpr h.dedup

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru