Documentation

Mathlib.Data.Set.PowersetCard

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

Instances For

@[simp]

theorem Set.powersetCard.mem_iff {α : Type u_1} {n : ℕ} {s : Finset α} :

s ∈ powersetCard α n ↔ s.card = n

instance Set.powersetCard.instSetLikeElemFinset {α : Type u_1} {n : ℕ} :

SetLike (↑(powersetCard α n)) α

Equations

instance Set.powersetCard.instPartialOrderElemFinset {α : Type u_1} {n : ℕ} :

PartialOrder ↑(powersetCard α n)

Equations

@[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

Instances For

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

noncomputable def Set.powersetCard.ofSingleton {α : Type u_1} :

α ≃ ↑(powersetCard α 1)

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

Equations

Instances For

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

Instances For

@[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

Instances For

@[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 ⋯

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

powersetCard α n = ↑(Finset.powersetCard n Finset.univ)

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

Fintype ↑(powersetCard α n)

Equations

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 α