mathlib3 documentation

data.fintype.list

Fintype instance for nodup lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
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.

Equations
source
@[simp]
theorem multiset.lists_coe {α : Type u_1} [decidable_eq α] (l : list α) :
↑l.lists = l.permutations.to_finset
source
@[simp]
theorem multiset.mem_lists_iff {α : Type u_1} [decidable_eq α] (s : multiset α) (l : list α) :
l ∈ s.lists ↔ s = ⟦l⟧
source
@[protected, instance]
def fintype_nodup_list {α : Type u_1} [decidable_eq α] [fintype α] :
fintype {l // l.nodup}
Equations