mathlib documentation


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 decidable_eq 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} [decidable_eq α] :
multiset αfinset (list α)

The finset of l : list α that, given m : multiset α, have the property ⟦l⟧ = m.

theorem multiset.lists_coe {α : Type u_1} [decidable_eq α] (l : list α) :
theorem multiset.mem_lists_iff {α : Type u_1} [decidable_eq α] (s : multiset α) (l : list α) :
def fintype_nodup_list {α : Type u_1} [decidable_eq α] [fintype α] :
fintype {l // l.nodup}