Maps, coercions and enumerations of fixed-cardinality subsets

Set.powersetCard.map_injective shows that vertex embeddings induce injective maps on fixed-cardinality subsets.

Set.powersetCard.coe_ofSingleton identifies the finite set underlying the singleton equivalence. It lets computations with fixed-cardinality subsets use the usual singleton API.

Set.powersetCard.finChooseEquiv m j enumerates the j-element subsets of Fin m by Fin (m.choose j).

theorem Set.powersetCard.map_injective {α : Type u_1} {β : Type u_2} (n : ℕ) (f : α ↪ β) : Function.Injective (map n f)

An embedding induces an injective map on fixed-cardinality subsets.

@[simp]

theorem Set.powersetCard.coe_ofSingleton {α : Type u_1} (a : α) : ↑(ofSingleton a) = {a}

The finite set underlying the singleton equivalence is the singleton itself.

noncomputable def Set.powersetCard.finChooseEquiv (m j : ℕ) : ↑(powersetCard (Fin m) j) ≃ Fin (m.choose j)

An enumeration of the j-element subsets of Fin m by Fin (m.choose j).