perm_toList — Mathlib

English

For Finsets f1, f2, the lists f1.toList and f2.toList are permutations of each other if and only if f1 = f2.

Русский

Для Finset f1, f2 списки f1.toList и f2.toList являются перестановками друг друга тогда и только тогда, когда f1 = f2.

LaTeX

$$$ f_1.toList.Perm f_2.toList \iff f_1 = f_2 $$$

Lean4

@[simp]
protected theorem perm_toList {f₁ f₂ : Finset α} : f₁.toList.Perm f₂.toList ↔ f₁ = f₂
    where
  mp h := Finset.ext fun x => by simp [← Finset.mem_toList, h.mem_iff]
  mpr h := .of_eq <| congrArg Finset.toList h

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