Density of an event under relabelling

Relabelling a finite type by an equivalence does not change the density of an event: for e : α ≃ β, the density of {a | p (e a)} in α equals the density of {b | p b} in β (Fintype.dens_filter_comp_equiv). This is the form needed to reindex uniform seeds or sample spaces; Mathlib's Finset.dens_map_equiv states the same invariance for the image of a finset.

Main results

• Fintype.dens_filter_comp_equiv: relabelling the sample space by an equivalence preserves the density of an event.

theorem Fintype.dens_filter_comp_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α ≃ β) (p : β → Prop) [DecidablePred p] : {a : α | p (e a)}.dens = {b : β | p b}.dens

Relabelling the sample space by an equivalence does not change the density of an event.