Fixed-cardinality subsets of linear orders #

This file collects two enumerations of fixed-cardinality subsets through Mathlib's Set.powersetCard.ofFinEmbEquiv, together with the sum and product formulas for its increasing enumeration.

In a linear order, a three-element finite set is listed exactly once as an increasing triple a < b < c. Set.powersetCard.ofLtTriple is this enumeration, an equivalence between the increasing triples and Set.powersetCard I 3. It is the case n = 3 of Mathlib's Set.powersetCard.ofFinEmbEquiv, stated for triples so that sums and products over the increasing triples {t : I × I × I // t.1 < t.2.1 ∧ t.2.1 < t.2.2} can be compared with sums over three-element sets. For instance, a finite linear order with n elements has n.choose 3 increasing triples.

For k + p = N, the indices k, …, N - 1 of Fin N form the p-subset TauCeti.topBlock h, built through Set.powersetCard.ofFinEmbEquiv from the order embedding a ↦ k + a. Its increasing enumeration is a ↦ k + a, an index lies in it exactly when it is at least k, and every other p-subset meets the first k indices.

The shuffle of two disjoint fixed-cardinality subsets lists the increasing enumeration of the first followed by that of the second. The shuffle of a singleton {i} with s.erase i lists i first and then s.erase i, and in the presentation Fin (n + 1) it is the inverse cycle moving the position of i in s to the front.

source

@[simp]

theorem Set.powersetCard.prod_comp_ofFinEmbEquiv_symm {I : Type u_1} [LinearOrder I] {n : ℕ} (s : ↑(powersetCard I n)) {M : Type u_2} [CommMonoid M] (f : I → M) :

∏ a : Fin n, f ((ofFinEmbEquiv.symm s) a) = ∏ i ∈ ↑s, f i

A product over the increasing enumeration of a fixed-cardinality subset is the product over that subset.

source

@[simp]

theorem Set.powersetCard.sum_comp_ofFinEmbEquiv_symm {I : Type u_1} [LinearOrder I] {n : ℕ} (s : ↑(powersetCard I n)) {M : Type u_2} [AddCommMonoid M] (f : I → M) :

∑ a : Fin n, f ((ofFinEmbEquiv.symm s) a) = ∑ i ∈ ↑s, f i

Summing over the increasing enumeration of a fixed-cardinality subset is the same as summing over that subset.

source

noncomputable def Set.powersetCard.ofLtTriple {I : Type u_1} [LinearOrder I] :

{ t : I × I × I // t.1 < t.2.1 ∧ t.2.1 < t.2.2 } ≃ ↑(powersetCard I 3)

The increasing triples a < b < c of a linear order enumerate its three-element sets, by (a, b, c) ↦ {a, b, c}.

Instances For

source

@[simp]

theorem Set.powersetCard.val_ofLtTriple {I : Type u_1} [LinearOrder I] (t : { t : I × I × I // t.1 < t.2.1 ∧ t.2.1 < t.2.2 }) :

↑(ofLtTriple t) = {(↑t).1, (↑t).2.1, (↑t).2.2}

The three-element set enumerated by an increasing triple consists of its three entries.

source

theorem Set.powersetCard.exists_lt_lt_val_eq {I : Type u_1} [LinearOrder I] (s : ↑(powersetCard I 3)) :

∃ (a : I) (b : I) (c : I), a < b ∧ b < c ∧ ↑s = {a, b, c}

Every three-element set of a linear order is {a, b, c} for some a < b < c.

source

theorem Set.powersetCard.card_lt_triple {I : Type u_1} [LinearOrder I] [Fintype I] :

Fintype.card { t : I × I × I // t.1 < t.2.1 ∧ t.2.1 < t.2.2 } = (Fintype.card I).choose 3

A finite linear order with n elements has n.choose 3 increasing triples.

source

theorem Set.powersetCard.orderEmbOfFin_permOfDisjoint {I : Type u_1} [LinearOrder I] {m n : ℕ} (u : ↑(powersetCard I m)) (t : ↑(powersetCard I n)) (hdisj : Disjoint ↑u ↑t) (j : Fin (m + n)) :

((↑(disjUnion hdisj)).orderEmbOfFin ⋯) ((permOfDisjoint hdisj) j) = Sum.elim (⇑((↑u).orderEmbOfFin ⋯)) (⇑((↑t).orderEmbOfFin ⋯)) (finSumFinEquiv.symm j)

The shuffle of two disjoint fixed-cardinality subsets u and t lists the increasing enumeration of u, followed by the increasing enumeration of t, inside the increasing enumeration of their union.

source

theorem Set.powersetCard.orderEmbOfFin_permOfDisjoint_singleton_erase {I : Type u_1} [LinearOrder I] (i : I) (s : Finset I) {n : ℕ} (hn : (s.erase i).card = n) (hdisj : Disjoint ↑⟨{i}, ⋯⟩ ↑⟨s.erase i, hn⟩) (j : Fin (n + 1)) :

((↑(disjUnion hdisj)).orderEmbOfFin ⋯) ((permOfDisjoint hdisj) ((finCongr ⋯).symm j)) = Fin.cons i (⇑((s.erase i).orderEmbOfFin hn)) j

The shuffle of the singleton {i} and s.erase i places i first, followed by the increasing enumeration of s.erase i.

source

theorem Set.powersetCard.conj_permOfDisjoint_singleton_erase {I : Type u_1} [LinearOrder I] (i : I) (s : Finset I) (hi : i ∈ s) {n : ℕ} (hn : (s.erase i).card = n) (hsCard : s.card = n + 1) (hdisj : Disjoint ↑⟨{i}, ⋯⟩ ↑⟨s.erase i, hn⟩) :

(finCongr ⋯).symm.trans (Equiv.trans (permOfDisjoint hdisj) (finCongr ⋯)) = Equiv.symm ((s.orderIsoOfFin hsCard).symm ⟨i, hi⟩).cycleRange

The shuffle of the singleton {i} and s.erase i, in the presentation Fin (n + 1), is the inverse cycle moving the position of i in the increasing enumeration of s to the front.

source