Combinations

Combinations in a type are finite subsets of given cardinality.

• Set.powersetCard α n is the set of all Finset α with cardinality n. The name is chosen in relation with Finset.powersetCard which corresponds to the analogous structure for subsets of given cardinality of a given Finset, as a Finset.

• Set.powersetCard.card proves that the Nat.card-cardinality of this set is equal to (Nat.card α).choose n.

def Set.powersetCard (α : Type u_1) (n : ℕ) : Set (Finset α)

The type of combinations of n elements of a type α.

See also Finset.powersetCard.

Equations

• Set.powersetCard α n = {s : Finset α | s.card = n}

@[simp]

theorem Set.powersetCard.mem_iff {α : Type u_1} {n : ℕ} {s : Finset α} : s ∈ powersetCard α n ↔ s.card = n

@[implicit_reducible]

instance Set.powersetCard.instSetLikeElemFinset {α : Type u_1} {n : ℕ} : SetLike (↑(powersetCard α n)) α

Equations

• Set.powersetCard.instSetLikeElemFinset = SetLike.instSubtype

@[implicit_reducible]

instance Set.powersetCard.instPartialOrderElemFinset {α : Type u_1} {n : ℕ} : PartialOrder ↑(powersetCard α n)

Equations

• Set.powersetCard.instPartialOrderElemFinset = PartialOrder.ofSetLike (↑(Set.powersetCard α n)) α

@[simp]

theorem Set.powersetCard.coe_coe {α : Type u_1} {n : ℕ} {s : ↑(powersetCard α n)} : ↑↑s = ↑s

theorem Set.powersetCard.mem_coe_iff {α : Type u_1} {n : ℕ} {s : ↑(powersetCard α n)} {a : α} : a ∈ ↑s ↔ a ∈ s

@[simp]

theorem Set.powersetCard.card_eq {α : Type u_1} {n : ℕ} (s : ↑(powersetCard α n)) : (↑s).card = n

@[simp]

theorem Set.powersetCard.ncard_eq {α : Type u_1} {n : ℕ} (s : ↑(powersetCard α n)) : (↑s).ncard = n

theorem Set.powersetCard.coe_nonempty_iff {α : Type u_1} {n : ℕ} {s : ↑(powersetCard α n)} : (↑s).Nonempty ↔ 1 ≤ n

theorem Set.powersetCard.coe_nontrivial_iff {α : Type u_1} {n : ℕ} {s : ↑(powersetCard α n)} : (↑s).Nontrivial ↔ 1 < n

theorem Set.powersetCard.eq_iff_subset {α : Type u_1} {n : ℕ} {s t : ↑(powersetCard α n)} : s = t ↔ ↑s ⊆ ↑t

theorem Set.powersetCard.exists_mem_notMem {α : Type u_1} {n : ℕ} (hn : 1 ≤ n) (hα : ↑n < ENat.card α) {a b : α} (hab : a ≠ b) : ∃ (s : ↑(powersetCard α n)), a ∈ s ∧ b ∉ s

theorem Set.powersetCard.exists_mem_notMem_iff_ne {α : Type u_1} {n : ℕ} (s t : ↑(powersetCard α n)) : s ≠ t ↔ ∃ a ∈ s, a ∉ t

def Set.powersetCard.map {α : Type u_1} (n : ℕ) {β : Type u_2} (f : α ↪ β) (s : ↑(powersetCard α n)) : ↑(powersetCard β n)

The map powersetCard α n → powersetCard β n induced by embedding f : α ↪ β.

Equations

• Set.powersetCard.map n f s = ⟨Finset.map f ↑s, ⋯⟩

theorem Set.powersetCard.mem_map_iff_mem_range {α : Type u_1} (n : ℕ) {β : Type u_2} (f : α ↪ β) (s : ↑(powersetCard α n)) (b : β) : b ∈ map n f s ↔ b ∈ ⇑f '' ↑s

@[simp]

theorem Set.powersetCard.coe_map {α : Type u_1} (n : ℕ) {β : Type u_2} (f : α ↪ β) (s : ↑(powersetCard α n)) : ↑(map n f s) = ⇑f '' ↑s

@[simp]

theorem Set.powersetCard.val_map {α : Type u_1} (n : ℕ) {β : Type u_2} (f : α ↪ β) (s : ↑(powersetCard α n)) : ↑(map n f s) = Finset.map f ↑s

def Set.powersetCard.ofCard {α : Type u_1} {n : ℕ} {s : Finset α} (s_card : s.card = n) : ↑(powersetCard α n)

The coercion of a finite set to its corresponding element of Set.powersetCard.

Equations

• Set.powersetCard.ofCard s_card = ⟨s, ⋯⟩

@[simp]

theorem Set.powersetCard.val_ofCard {α : Type u_1} {n : ℕ} {s : Finset α} (s_card : s.card = n) : ↑(ofCard s_card) = s

@[simp]

theorem Set.powersetCard.ofCard_coe {α : Type u_1} {n : ℕ} {s : ↑(powersetCard α n)} (h : (↑s).card = n) : ofCard h = s

noncomputable def Set.powersetCard.ofSingleton {α : Type u_1} : α ≃ ↑(powersetCard α 1)

The equivalence sending a : α to the singleton {a}.

Equations

• Set.powersetCard.ofSingleton = { toFun := fun (a : α) => ⟨{a}, ⋯⟩, invFun := fun (s : ↑(Set.powersetCard α 1)) => ⋯.choose, left_inv := ⋯, right_inv := ⋯ }

def Set.powersetCard.ofFinEmb (n : ℕ) (β : Type u_2) (f : Fin n ↪ β) : ↑(powersetCard β n)

The image of an embedding f : Fin n ↪ β as an element of powersetCard β n.

Equations

• Set.powersetCard.ofFinEmb n β f = Set.powersetCard.map n f ⟨Finset.univ, ⋯⟩

@[simp]

theorem Set.powersetCard.mem_ofFinEmb_iff_mem_range (n : ℕ) (β : Type u_2) (f : Fin n ↪ β) (b : β) : b ∈ ofFinEmb n β f ↔ b ∈ range ⇑f

@[simp]

theorem Set.powersetCard.coe_ofFinEmb (n : ℕ) (β : Type u_2) (f : Fin n ↪ β) : ↑(ofFinEmb n β f) = range ⇑f

@[simp]

theorem Set.powersetCard.val_ofFinEmb (n : ℕ) (β : Type u_2) (f : Fin n ↪ β) : ↑(ofFinEmb n β f) = Finset.map f Finset.univ

theorem Set.powersetCard.ofFinEmb_surjective (n : ℕ) (β : Type u_2) : Function.Surjective (ofFinEmb n β)

def Set.powersetCard.compl {α : Type u_1} {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} (hm : m + n = Fintype.card α) : ↑(powersetCard α n) ≃ ↑(powersetCard α m)

Complement of Finsets as an equivalence on Set.powersetCard.

Equations

• Set.powersetCard.compl hm = { toFun := fun (s : ↑(Set.powersetCard α n)) => ⟨(↑s)ᶜ, ⋯⟩, invFun := fun (t : ↑(Set.powersetCard α m)) => ⟨(↑t)ᶜ, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Set.powersetCard.coe_compl {α : Type u_1} {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} {hm : m + n = Fintype.card α} {s : ↑(powersetCard α n)} : ↑((compl hm) s) = (↑s)ᶜ

@[simp]

theorem Set.powersetCard.mem_compl {α : Type u_1} {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} {hm : m + n = Fintype.card α} {s : ↑(powersetCard α n)} {a : α} : a ∈ (compl hm) s ↔ a ∉ s

theorem Set.powersetCard.compl_symm {α : Type u_1} {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} {hm : m + n = Fintype.card α} : (compl hm).symm = compl ⋯

def Set.powersetCard.disjUnion {α : Type u_1} {n m : ℕ} {s : ↑(powersetCard α m)} {t : ↑(powersetCard α n)} (hst : Disjoint ↑s ↑t) : ↑(powersetCard α (m + n))

The disjoint union of two powersetCards.

Equations

• Set.powersetCard.disjUnion hst = ⟨(↑s).disjUnion (↑t) hst, ⋯⟩

@[simp]

theorem Set.powersetCard.coe_disjUnion {α : Type u_1} {n m : ℕ} {s : ↑(powersetCard α m)} {t : ↑(powersetCard α n)} {hst : Disjoint ↑s ↑t} : ↑(disjUnion hst) = (↑s).disjUnion (↑t) hst

@[simp]

theorem Set.powersetCard.mem_disjUnion {α : Type u_1} {n m : ℕ} {s : ↑(powersetCard α m)} {t : ↑(powersetCard α n)} {hst : Disjoint ↑s ↑t} {a : α} : a ∈ disjUnion hst ↔ a ∈ s ∨ a ∈ t

theorem Set.powersetCard.coe_finset (α : Type u_1) (n : ℕ) [Fintype α] : powersetCard α n = ↑(Finset.powersetCard n Finset.univ)

@[implicit_reducible]

instance Set.powersetCard.instFintypeElemFinset (α : Type u_1) (n : ℕ) [Fintype α] : Fintype ↑(powersetCard α n)

Equations

• Set.powersetCard.instFintypeElemFinset α n = ⋯.mpr inferInstance

instance Set.powersetCard.instFiniteElemFinset (α : Type u_1) (n : ℕ) [Finite α] : Finite ↑(powersetCard α n)

theorem Set.powersetCard.exist_mem_powersetCard_of_inf (α : Type u_1) (n : ℕ) (h : 0 < n) [Infinite α] (a : α) : ∃ s ∈ powersetCard α n, a ∈ s

instance Set.powersetCard.instInfinite (α : Type u_1) (n : ℕ) [NeZero n] [Infinite α] : Infinite ↑(powersetCard α n)

theorem Set.powersetCard.card (α : Type u_1) (n : ℕ) : Nat.card ↑(powersetCard α n) = (Nat.card α).choose n

theorem Set.powersetCard.nontrivial {α : Type u_1} {n : ℕ} (h1 : 0 < n) (h2 : ↑n < ENat.card α) : Nontrivial ↑(powersetCard α n)

If 0 < n < ENat.card α, then powersetCard α n is nontrivial.

theorem Set.powersetCard.nontrivial' {α : Type u_1} {n : ℕ} (h1 : 0 < n) (h2 : n < Nat.card α) : Nontrivial ↑(powersetCard α n)

A variant of Set.powersetCard.nontrivial that uses Nat.card.

@[simp]

theorem Set.powersetCard.eq_empty_iff {α : Type u_1} {n : ℕ} [Finite α] : powersetCard α n = ∅ ↔ Nat.card α < n

theorem Set.powersetCard.nontrivial_iff {α : Type u_1} {n : ℕ} [Finite α] : Nontrivial ↑(powersetCard α n) ↔ 0 < n ∧ n < Nat.card α

def Set.powersetCard.prodEquiv {α : Type u_1} : (n : ℕ) × ↑(powersetCard α n) ≃ Finset α

The bijection between the product of (n : ℕ) and the finsets of α of cardinality n and Finset α.

Equations

• Set.powersetCard.prodEquiv = { toFun := fun (x : (n : ℕ) × ↑(Set.powersetCard α n)) => ↑x.snd, invFun := fun (x : Finset α) => ⟨x.card, ⟨x, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Set.powersetCard.prodEquiv_apply {α : Type u_1} (x : (n : ℕ) × ↑(powersetCard α n)) : prodEquiv x = ↑x.snd

@[simp]

theorem Set.powersetCard.prodEquiv_symm_apply {α : Type u_1} (s : Finset α) : prodEquiv.symm s = ⟨s.card, ofCard ⋯⟩