Extremal noncrossing partitions: discrete and indiscrete

TheoremThe discrete partition is noncrossing#✓fully proved

For every natural number \(n\), the discrete partition of \(\{0, \dots, n-1\}\), whose blocks are the singletons, is noncrossing.

theorem isNoncrossing_bot (n : ℕ) : IsNoncrossing (⊥ : SetPartition n)

Uses 3 · Used by 1

Statement usesNoncrossing set partition · Set partition

Proof usesCrossing in a set partition

Used byDiscrete noncrossing partition

TheoremThe indiscrete partition is noncrossing#✓fully proved

For every natural number \(n\), the indiscrete partition of \(\{0, \dots, n-1\}\), the coarsest partition of this set, is noncrossing.

theorem isNoncrossing_top (n : ℕ) : IsNoncrossing (⊤ : SetPartition n)

Uses 3 · Used by 1

Statement usesNoncrossing set partition · Set partition

Proof usesCrossing in a set partition

Used byThe indiscrete noncrossing partition

DefinitionDiscrete noncrossing partition#✓fully proved

For a natural number \(n\), the discrete noncrossing partition of \(\{0, \dots, n-1\}\) is the finest partition of this set, whose blocks are the singletons \(\{a\}\) for \(a \in \{0, \dots, n-1\}\); it is noncrossing.

def discrete (n : ℕ) : NoncrossingPartition n :=
  ⟨⊥, isNoncrossing_bot n⟩

Uses 4 · Used by 14

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · The discrete partition is noncrossing

Used byThe block of a point in the discrete noncrossing partition · The discrete noncrossing partition consists of the singletons · The discrete partition of the empty set has no blocks · 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 · Noncrossing partitions of a two-element 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 · Enumerating the proper noncrossing partitions of three points · The proper noncrossing partition of two points

DefinitionThe indiscrete noncrossing partition#✓fully proved

For a natural number \(n\), the indiscrete noncrossing partition of \(\{0, \dots, n-1\}\) is the coarsest partition of this set: its only block is the whole set when \(n > 0\), and it has no blocks when \(n = 0\). It is noncrossing.

def indiscrete (n : ℕ) : NoncrossingPartition n :=
  ⟨⊤, isNoncrossing_top n⟩

Uses 4 · Used by 21

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · The indiscrete partition is noncrossing

Used byThe block of a point in the indiscrete noncrossing partition · Discrete and indiscrete partitions agree on the empty set · 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 partition of a nonempty set has a single block · The indiscrete partition of the empty set has no blocks · 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 · 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 · The two-block partitions of three points are not indiscrete

TheoremThe block of a point in the discrete noncrossing partition#✓fully proved

For every natural number \(n\) and every \(a \in \{0, \dots, n-1\}\), the block containing \(a\) in the discrete noncrossing partition of \(\{0, \dots, n-1\}\) is the singleton \(\{a\}\).

@[simp]
theorem block_discrete (n : ℕ) (a : Fin n) : block (discrete n) a = {a}

Uses 3

Statement usesBlock of a noncrossing partition · Discrete noncrossing partition

Proof usesSet partition

TheoremThe block of a point in the indiscrete noncrossing partition#✓fully proved

For every natural number \(n\) and every \(a \in \{0, \dots, n-1\}\), the block containing \(a\) in the indiscrete noncrossing partition of \(\{0, \dots, n-1\}\) is the whole set \(\{0, \dots, n-1\}\).

For \(n = 0\) there is no such \(a\), so the statement is vacuous.

@[simp]
theorem block_indiscrete (n : ℕ) (a : Fin n) : block (indiscrete n) a = Finset.univ

Uses 3

Statement usesBlock of a noncrossing partition · The indiscrete noncrossing partition

Proof usesSet partition

TheoremThe discrete noncrossing partition consists of the singletons#✓fully proved

For every natural number \(n\), the set of blocks of the discrete noncrossing partition of \(\{0, \dots, n-1\}\) is exactly the set of singletons \(\{a\}\) with \(a \in \{0, \dots, n-1\}\).

@[simp]
theorem discrete_parts (n : ℕ) :
    (discrete n).val.parts =
      (Finset.univ : Finset (Fin n)).map ⟨singleton, singleton_injective⟩

Uses 3 · Used by 3

Statement usesNoncrossing set partition · Set partition · Discrete noncrossing partition

Used byThe discrete and indiscrete partitions of a three-element set differ · The discrete and indiscrete partitions of a two-element set differ · Enumerating the proper noncrossing partitions of three points

TheoremThe indiscrete partition of the empty set has no blocks#✓fully proved

For \(n = 0\), the set of blocks of the indiscrete noncrossing partition of \(\{0, \dots, n-1\}\), the empty set, is empty.

@[simp]
theorem indiscrete_parts_zero : (indiscrete 0).val.parts = ∅

Uses 3 · Used by 2

Statement usesNoncrossing set partition · Set partition · The indiscrete noncrossing partition

Used byThe empty set has a unique noncrossing partition · Noncrossing partitions of the empty set

TheoremThe discrete partition of the empty set has no blocks#✓fully proved

For \(n = 0\), the discrete noncrossing partition of the empty set \(\{0, \dots, n-1\}\) has no blocks: its set of blocks is empty.

@[simp]
theorem discrete_parts_zero : (discrete 0).val.parts = ∅

Uses 3

Statement usesNoncrossing set partition · Set partition · Discrete noncrossing partition

TheoremThe indiscrete partition of a nonempty set has a single block#✓fully proved

For a natural number \(n\) with \(0 < n\), the set of blocks of the indiscrete noncrossing partition of \(\{0, \dots, n-1\}\) is \(\{\{0, \dots, n-1\}\}\): its only block is the whole set.

theorem indiscrete_parts_pos {n : ℕ} (hn : 0 < n) :
    (indiscrete n).val.parts = {Finset.univ}

Uses 3 · Used by 4

Statement usesNoncrossing set partition · Set partition · The indiscrete noncrossing partition

Used byThe discrete and indiscrete partitions of a three-element set differ · The discrete and indiscrete partitions of a two-element set differ · Enumerating the proper noncrossing partitions of three points · The two-block partitions of three points are not indiscrete

TheoremCharacterization of the discrete noncrossing partition#✓fully proved

Let \(n\) be a natural number. A noncrossing partition \(P\) of \(\{0, \dots, n-1\}\) equals the discrete noncrossing partition if and only if \(P\), viewed as a set partition, is the finest partition of \(\{0, \dots, n-1\}\).

theorem eq_discrete_iff_val_eq_bot {n : ℕ} {P : NoncrossingPartition n} :
    P = discrete n ↔ P.val = ⊥

Uses 4 · Used by 2

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · Discrete noncrossing partition

Used byA noncrossing partition of three points with three blocks is discrete · Classification of noncrossing partitions of a two-element set

TheoremCharacterization of the indiscrete noncrossing partition#✓fully proved

Let \(n\) be a natural number. A noncrossing partition \(P\) of \(\{0, \dots, n-1\}\) equals the indiscrete noncrossing partition if and only if \(P\), viewed as a set partition, is the coarsest partition of \(\{0, \dots, n-1\}\).

theorem eq_indiscrete_iff_val_eq_top {n : ℕ} {P : NoncrossingPartition n} :
    P = indiscrete n ↔ P.val = ⊤

Uses 4 · Used by 4

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · The indiscrete noncrossing partition

Used byA partition whose blocks are all the whole set is indiscrete · 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

TheoremA partition whose blocks are all the whole set is indiscrete#✓fully proved

Let \(n\) be a natural number and let \(P\) be a noncrossing partition of \(\{0, \dots, n-1\}\). If for every \(a \in \{0, \dots, n-1\}\) the block of \(P\) containing \(a\) is the whole set \(\{0, \dots, n-1\}\), then \(P\) is the indiscrete noncrossing partition.

theorem eq_indiscrete_of_forall_block_eq_univ {n : ℕ} (P : NoncrossingPartition n)
    (h : ∀ a : Fin n, block P a = Finset.univ) : P = indiscrete n

Uses 7

Statement usesNoncrossing partition · Block of a noncrossing partition · The indiscrete noncrossing partition

Proof usesBlocks of a partition other than the coarsest are smaller than the ground set · Noncrossing set partition · Set partition · Characterization of the indiscrete noncrossing partition

TheoremThe empty set has a unique noncrossing partition#✓fully proved

For \(n = 0\), every noncrossing partition of \(\{0, \dots, n-1\}\), the empty set, equals the indiscrete noncrossing partition of this set.

theorem eq_indiscrete_zero (P : NoncrossingPartition 0) : P = indiscrete 0

Uses 5 · Used by 2

Statement usesNoncrossing partition · The indiscrete noncrossing partition

Proof usesNoncrossing set partition · Set partition · The indiscrete partition of the empty set has no blocks

Used byDiscrete and indiscrete partitions agree on the empty set · The only noncrossing partition of the empty set is the discrete one

TheoremDiscrete and indiscrete partitions agree on the empty set#✓fully proved

For \(n = 0\), the discrete and the indiscrete noncrossing partitions of the empty set \(\{0, \dots, n-1\}\) are equal.

@[simp]
theorem discrete_zero_eq_indiscrete_zero : discrete 0 = indiscrete 0

Uses 4 · Used by 1

Statement usesNoncrossing partition · Discrete noncrossing partition · The indiscrete noncrossing partition

Proof usesThe empty set has a unique noncrossing partition

Used byThe only noncrossing partition of the empty set is the discrete one

TheoremThe only noncrossing partition of the empty set is the discrete one#✓fully proved

For \(n = 0\), every noncrossing partition of the empty set \(\{0, \dots, n-1\}\) equals the discrete noncrossing partition.

theorem eq_discrete_zero (P : NoncrossingPartition 0) : P = discrete 0

Uses 5

Statement usesNoncrossing partition · Discrete noncrossing partition

Proof usesDiscrete and indiscrete partitions agree on the empty set · The empty set has a unique noncrossing partition · The indiscrete noncrossing partition

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.