Fintype instance for nodup lists

The subtype of {l : List α // l.Nodup} over a [Fintype α] admits a Fintype instance.

Implementation details

To construct the Fintype instance, a function lifting a Multiset α to the Multiset (List α) is provided. This function is applied to the Finset.powerset of Finset.univ.

def Multiset.lists {α : Type u_1} : Multiset α → Multiset (List α)

Given a m : Multiset α, we form the Multiset of l : List α with the property ⟦l⟧ = m.

@[simp]

theorem Multiset.lists_coe {α : Type u_1} (l : List α) : (↑l).lists = ↑l.permutations

@[simp]

theorem Multiset.lists_nodup_finset {α : Type u_1} (l : Finset α) : l.val.lists.Nodup

@[simp]

theorem Multiset.mem_lists_iff {α : Type u_1} (s : Multiset α) (l : List α) : l ∈ s.lists ↔ s = ⟦l⟧

@[simp]

theorem perm_toList {α : Type u_1} {f₁ f₂ : Finset α} : f₁.toList.Perm f₂.toList ↔ f₁ = f₂

instance fintypeNodupList {α : Type u_1} [Fintype α] : Fintype { l : List α // l.Nodup }