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 Finset (List α) that can construct it is provided. This function is applied to the Finset.powerset of Finset.univ.

In general, a DecidableEq instance is not necessary to define this function, but a proof of (List.permutations l).nodup is required to avoid it, which is a TODO.

def Multiset.lists {α : Type u_1} [DecidableEq α] : Multiset α → Finset (List α)

The Finset of l : List α that, given m : Multiset α, have the property ⟦l⟧ = m.

Equations

• s.lists = Quotient.liftOn s (fun (l : List α) => l.permutations.toFinset) ⋯

@[simp]

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

@[simp]

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

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

Equations

• fintypeNodupList = Fintype.subtype (Finset.univ.powerset.biUnion fun (s : Finset α) => s.val.lists) ⋯