Documentation

Mathlib.Data.Fintype.List

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} [inst : ] :
Finset (List α)

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Multiset.lists_coe {α : Type u_1} [inst : ] (l : List α) :
@[simp]
theorem Multiset.mem_lists_iff {α : Type u_1} [inst : ] (s : ) (l : List α) :
s =
instance fintypeNodupList {α : Type u_1} [inst : ] [inst : ] :
Fintype { l // }
Equations
• One or more equations did not get rendered due to their size.