Noncrossing partitions and the refinement order

AbbreviationSet partition#✓fully proved

A set partition of \(\{0, \dots, n-1\}\) is a finite collection of nonempty, pairwise disjoint subsets of \(\{0, \dots, n-1\}\), called blocks, whose union is \(\{0, \dots, n-1\}\).

abbrev SetPartition (n : ℕ) :=
  Finpartition (Finset.univ : Finset (Fin n))

Used by 48

Used byDescending strictly \(k\)-Naples parking functions and noncrossing partitions · Even noncrossing partitions and Dyck paths with even descents · Recursive lower bound for marriageable singles partitions · Noncrossing partitions split into lonely and marriageable singles partitions · Marriageable singles partition · Number of lonely singles partitions · Small values of the lonely singles count · Number of marriageable singles partitions · Small values of the marriageable singles count · Crossing after merging two blocks · Same block after merging two blocks · Noncrossing partitions by number of blocks and of singleton blocks · Base value of the noncrossing block and singleton count · The block of a point in the discrete noncrossing partition · The block of a point in the indiscrete noncrossing partition · Discrete noncrossing partition · The discrete noncrossing partition consists of the singletons · The discrete partition of the empty set has no blocks · Characterization of the discrete noncrossing partition · Characterization of the indiscrete noncrossing partition · A partition whose blocks are all the whole set is indiscrete · The empty set has a unique noncrossing partition · The indiscrete noncrossing partition · The indiscrete partition of a nonempty set has a single block · The indiscrete partition of the empty set has no blocks · The discrete partition is noncrossing · The indiscrete partition is noncrossing · Block of a noncrossing partition · Crossing in a set partition · Noncrossing set partition · Partitions of at most three points are noncrossing · Noncrossing partition · Noncrossing partitions of a one-element set · Noncrossing partitions of a three-element set · Noncrossing partitions of a two-element set · Noncrossing partitions of the empty set · The discrete and indiscrete partitions of a three-element set differ · The discrete and indiscrete partitions of a two-element set differ · A noncrossing partition of three points with three blocks is discrete · Classification of noncrossing partitions of a three-element set · Classification of noncrossing partitions of a two-element set · A noncrossing partition of three points with one block is indiscrete · Noncrossing partitions of one point are indiscrete · Enumerating the proper noncrossing partitions of three points · Noncrossing partitions of three points have one, two or three blocks · Enumerating the two-block noncrossing partitions of three points · Two-block partition of three points · The two-block partitions of three points are not indiscrete

DefinitionCrossing in a set partition#✓fully proved

A set partition \(P\) of \(\{0, \dots, n-1\}\) has a crossing if there are \(a < b < c < d\) in \(\{0, \dots, n-1\}\) such that \(a\) and \(c\) lie in the same block of \(P\), \(b\) and \(d\) lie in the same block of \(P\), and these two blocks are different.

def HasCrossing {n : ℕ} (P : SetPartition n) : Prop :=
  ∃ a b c d : Fin n,
    a < b ∧ b < c ∧ c < d ∧
      P.part a = P.part c ∧ P.part b = P.part d ∧ P.part a ≠ P.part b

Uses 1 · Used by 17

Statement usesSet partition

Used byDescending strictly \(k\)-Naples parking functions and noncrossing partitions · Recursive lower bound for marriageable singles partitions · Noncrossing partitions split into lonely and marriageable singles partitions · Number of lonely singles partitions · Small values of the lonely singles count · Number of marriageable singles partitions · Small values of the marriageable singles count · Noncrossing partitions by number of blocks and of singleton blocks · Base value of the noncrossing block and singleton count · The discrete partition is noncrossing · The indiscrete partition is noncrossing · Noncrossing set partition · Partitions of at most three points are noncrossing · Noncrossing partitions of a one-element set · Noncrossing partitions of a three-element set · Noncrossing partitions of a two-element set · Noncrossing partitions of the empty set

DefinitionNoncrossing set partition#✓fully proved

A set partition of \(\{0, \dots, n-1\}\) is noncrossing if it has no crossing.

def IsNoncrossing {n : ℕ} (P : SetPartition n) : Prop :=
  ¬ HasCrossing P

Uses 2 · Used by 41

Statement usesCrossing in a set partition · Set partition

Used byDescending strictly \(k\)-Naples parking functions and noncrossing partitions · Even noncrossing partitions and Dyck paths with even descents · Recursive lower bound for marriageable singles partitions · Noncrossing partitions split into lonely and marriageable singles partitions · Number of lonely singles partitions · Small values of the lonely singles count · Number of marriageable singles partitions · Small values of the marriageable singles count · Noncrossing partitions by number of blocks and of singleton blocks · Base value of the noncrossing block and singleton count · Discrete noncrossing partition · The discrete noncrossing partition consists of the singletons · The discrete partition of the empty set has no blocks · Characterization of the discrete noncrossing partition · Characterization of the indiscrete noncrossing partition · A partition whose blocks are all the whole set is indiscrete · The empty set has a unique noncrossing partition · The indiscrete noncrossing partition · The indiscrete partition of a nonempty set has a single block · The indiscrete partition of the empty set has no blocks · The discrete partition is noncrossing · The indiscrete partition is noncrossing · Block of a noncrossing partition · Partitions of at most three points are noncrossing · Noncrossing partition · Noncrossing partitions of a one-element set · Noncrossing partitions of a three-element set · Noncrossing partitions of a two-element set · Noncrossing partitions of the empty set · The discrete and indiscrete partitions of a three-element set differ · The discrete and indiscrete partitions of a two-element set differ · A noncrossing partition of three points with three blocks is discrete · Classification of noncrossing partitions of a three-element set · Classification of noncrossing partitions of a two-element set · A noncrossing partition of three points with one block is indiscrete · Noncrossing partitions of one point are indiscrete · Enumerating the proper noncrossing partitions of three points · Noncrossing partitions of three points have one, two or three blocks · Enumerating the two-block noncrossing partitions of three points · Two-block partition of three points · The two-block partitions of three points are not indiscrete

DefinitionNoncrossing partition#✓fully proved

A noncrossing partition of \(\{0, \dots, n-1\}\) is a set partition of \(\{0, \dots, n-1\}\) that is noncrossing.

def NoncrossingPartition (n : ℕ) :=
  { P : NoncrossingPartition.SetPartition n // NoncrossingPartition.IsNoncrossing P }

Uses 2 · Used by 37

Statement usesNoncrossing set partition · Set partition

Used byDescending strictly \(k\)-Naples parking functions and noncrossing partitions · Even noncrossing partitions and Dyck paths with even descents · Recursive lower bound for marriageable singles partitions · Noncrossing partitions split into lonely and marriageable singles partitions · Number of lonely singles partitions · Small values of the lonely singles count · Number of marriageable singles partitions · Small values of the marriageable singles count · Maximal sets of lanes and noncrossing partitions · Noncrossing partitions by number of blocks and of singleton blocks · Base value of the noncrossing block and singleton count · Discrete noncrossing partition · Discrete and indiscrete partitions agree on the empty set · Characterization of the discrete noncrossing partition · The only noncrossing partition of the empty set is the discrete one · Characterization of the indiscrete noncrossing partition · A partition whose blocks are all the whole set is indiscrete · The empty set has a unique noncrossing partition · The indiscrete noncrossing partition · Block of a noncrossing partition · Noncrossing partitions of a one-element set · Noncrossing partitions of a three-element set · Noncrossing partitions of a two-element set · Noncrossing partitions of the empty set · The discrete and indiscrete partitions of a three-element set differ · The discrete and indiscrete partitions of a two-element set differ · A noncrossing partition of three points with three blocks is discrete · Classification of noncrossing partitions of a three-element set · Classification of noncrossing partitions of a two-element set · A noncrossing partition of three points with one block is indiscrete · Noncrossing partitions of one point are indiscrete · Enumerating the proper noncrossing partitions of three points · The proper noncrossing partition of two points · Noncrossing partitions of three points have one, two or three blocks · Enumerating the two-block noncrossing partitions of three points · Two-block partition of three points · The two-block partitions of three points are not indiscrete

DefinitionBlock of a noncrossing partition#✓fully proved

For a noncrossing partition \(P\) of \(\{0, \dots, n-1\}\) and a point \(a \in \{0, \dots, n-1\}\), the block of \(P\) at \(a\) is the block of the underlying set partition that contains \(a\).

def block {n : ℕ} (P : _root_.NoncrossingPartition n) (a : Fin n) : Finset (Fin n) :=
  P.val.part a

Uses 3 · Used by 4

Statement usesNoncrossing partition · Noncrossing set partition · Set partition

Used byDescending strictly \(k\)-Naples parking functions and noncrossing partitions · The block of a point in the discrete noncrossing partition · The block of a point in the indiscrete noncrossing partition · A partition whose blocks are all the whole set is indiscrete

TheoremPartitions of at most three points are noncrossing#✓fully proved

For every \(n \le 3\), every set partition of \(\{0, \dots, n-1\}\) is noncrossing.

theorem isNoncrossing_of_le_three {n : ℕ} (hn : n ≤ 3) (P : SetPartition n) :
    IsNoncrossing P

Uses 3 · Used by 1

Statement usesNoncrossing set partition · Set partition

Proof usesCrossing in a set partition

Used byTwo-block partition of three points

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.