Union-closed families

DefinitionBinary code of a subset#✓fully proved

For a natural number \(n\) and a subset \(A\) of \(\{0, 1, \dots, n-1\}\), the binary code of \(A\) is the natural number \(b(A) = \sum_{i \in A} 2^i\).

public def binRep (n : ℕ) (A : Finset (Fin n)) : ℕ :=
  ∑ i ∈ A, 2 ^ (i : ℕ)

Used by 4

Used byPrefixes of a sorted canonical family are canonical · Sort key of a subset · Set order · The sort key encodes the set order

DefinitionSet order#✓fully proved

For subsets \(A\) and \(B\) of \(\{0, \dots, n-1\}\), \(A\) precedes \(B\) in the set order, written \(A < B\), if \(|A| > |B|\), or \(|A| = |B|\) and \(b(A) < b(B)\), where \(b(A) = \sum_{i \in A} 2^i\) is the binary code of \(A\).

public def setLT (n : ℕ) (A B : Finset (Fin n)) : Prop :=
  B.card < A.card ∨ (A.card = B.card ∧ binRep n A < binRep n B)

Uses 1 · Used by 3

Statement usesBinary code of a subset

Used byOrderly generation of union-closed families · Prefixes of a sorted canonical family are canonical · The sort key encodes the set order

DefinitionSort key of a subset#✓fully proved

For a subset \(A\) of \(\{0, \dots, n-1\}\), the sort key of \(A\) is the natural number \((n - |A|) \cdot 2^n + b(A)\), where \(b(A) = \sum_{i \in A} 2^i\) is the binary code of \(A\).

Since \(b(A) < 2^n\), comparing sort keys as numbers agrees with the set order: larger sets come first, and sets of the same size are ordered by binary code.

public def setKey (n : ℕ) (A : Finset (Fin n)) : ℕ :=
  (n - A.card) * 2 ^ n + binRep n A

Uses 1 · Used by 3

Statement usesBinary code of a subset

Used byString of a family · Prefixes of a sorted canonical family are canonical · The sort key encodes the set order

DefinitionString of a family#✓fully proved

For a family \(U\) of subsets of \(\{0, \dots, n-1\}\), the string \(s(U)\) is the list of the sort keys of the nonempty members of \(U\), in increasing order.

public def famString (n : ℕ) (U : Finset (Finset (Fin n))) : List ℕ :=
  Multiset.sort ((U.filter (· ≠ ∅)).val.map (setKey n)) (· ≤ ·)

Uses 1 · Used by 2

Statement usesSort key of a subset

Used byCanonical family · Prefixes of a sorted canonical family are canonical

DefinitionPermuted image of a family#✓fully proved

For a permutation \(\sigma\) of \(\{0, \dots, n-1\}\) and a family \(U\) of subsets of \(\{0, \dots, n-1\}\), the permuted image \(\sigma(U)\) is the family \(\{\sigma(A) : A \in U\}\), where \(\sigma(A) = \{\sigma(a) : a \in A\}\).

public def permImage (n : ℕ) (σ : Equiv.Perm (Fin n))
    (U : Finset (Finset (Fin n))) : Finset (Finset (Fin n)) :=
  U.image fun A => A.image ⇑σ

Used by 2

Used byCanonical family · Prefixes of a sorted canonical family are canonical

DefinitionUnion-closed family#✓fully proved

A family \(U\) of subsets of \(\{0, \dots, n-1\}\) is union-closed if \(A \cup B \in U\) for all \(A, B \in U\).

public def IsUnionClosed (n : ℕ) (U : Finset (Finset (Fin n))) : Prop :=
  ∀ A ∈ U, ∀ B ∈ U, A ∪ B ∈ U

Used by 1

Used byOrderly generation of union-closed families

DefinitionCanonical family#✓fully proved

A family \(U\) of subsets of \(\{0, \dots, n-1\}\) is canonical, the canonical representative of its isomorphism class, if for every permutation \(\sigma\) of \(\{0, \dots, n-1\}\) the string \(s(U)\) is lexicographically at most the string \(s(\sigma(U))\) of the permuted family \(\sigma(U)\).

public def IsCanonical (n : ℕ) (U : Finset (Finset (Fin n))) : Prop :=
  ∀ σ : Equiv.Perm (Fin n), famString n U ≤ famString n (permImage n σ U)

Uses 2 · Used by 2

Statement usesString of a family · Permuted image of a family

Used byOrderly generation of union-closed families · Prefixes of a sorted canonical family are canonical

TheoremThe sort key encodes the set order#✓fully proved

For all subsets \(A\) and \(B\) of \(\{0, \dots, n-1\}\), \(A < B\) in the set order if and only if the sort key of \(A\) is less than the sort key of \(B\).

public theorem setLT_iff_setKey_lt (n : ℕ) (A B : Finset (Fin n)) :
    setLT n A B ↔ setKey n A < setKey n B

Uses 3

Statement usesSort key of a subset · Set order

Proof usesBinary code of a subset

TheoremPrefixes of a sorted canonical family are canonical#✓fully proved

Let \(A_1, \dots, A_k\) be nonempty subsets of \(\{0, \dots, n-1\}\) with \(A_i < A_j\) in the set order whenever \(i < j\), and suppose the family \(U = \{\emptyset, A_1, \dots, A_k\}\) is canonical. Then for every \(m \le k\), including \(m = 0\), the family \(\{\emptyset, A_1, \dots, A_m\}\) is canonical.

Neither union closure nor coverage of the universe is needed.

public theorem orderly_canonical_prefix_of_sorted
    (n k m : ℕ) (U : Finset (Finset (Fin n)))
    (A : Fin k → Finset (Fin n))
    (hmk : m ≤ k)
    (hU : U = insert ∅ (Finset.image A Finset.univ))
    (hne : ∀ i, A i ≠ ∅)
    (hlt : ∀ i j : Fin k, i < j → setLT n (A i) (A j))
    (hcan : IsCanonical n U) :
    IsCanonical n
      (insert ∅ (Finset.image (fun i : Fin m => A (Fin.castLE hmk i)) Finset.univ))

Uses 6 · Used by 1

Statement usesCanonical family · Set order

Proof usesBinary code of a subset · String of a family · Permuted image of a family · Sort key of a subset

Used byOrderly generation of union-closed families

TheoremOrderly generation of union-closed families#✓fully proved

Let \(n\), \(k\) and \(m\) be natural numbers with \(1 \le m \le k\), and let \(A_1, \dots, A_k\) be nonempty subsets of \(\Omega_n = \{0, \dots, n-1\}\) with \(A_i < A_j\) in the set order whenever \(i < j\). Suppose the family \(U = \{\emptyset, A_1, \dots, A_k\}\) is union-closed, every element of \(\Omega_n\) lies in some member of \(U\), \(U \ne \{\Omega_n, \emptyset\}\), and \(U\) is canonical. Then the prefix family \(\{\emptyset, A_1, \dots, A_m\}\) is canonical.

The hypotheses that \(U\) is union-closed, covers \(\Omega_n\) and differs from \(\{\Omega_n, \emptyset\}\) are not used in the proof. The string of \(U\) lists the sort keys of \(A_1, \dots, A_k\) in order, so the string of the prefix family is a prefix of it, and a permutation that made the prefix family's string smaller would make the string of \(U\) smaller.

public theorem orderly_canonical_prefix
    (n k m : ℕ) (U : Finset (Finset (Fin n)))
    (A : Fin k → Finset (Fin n))
    (_hm : 1 ≤ m) (hmk : m ≤ k)
    (hU : U = insert ∅ (Finset.image A Finset.univ))
    (hne : ∀ i, A i ≠ ∅)
    (hlt : ∀ i j : Fin k, i < j → setLT n (A i) (A j))
    (_hbase : U ≠ {Finset.univ, ∅})
    (_hcov : ∀ i : Fin n, ∃ A₀ ∈ U, i ∈ A₀)
    (_huc : IsUnionClosed n U)
    (hcan : IsCanonical n U) :
    IsCanonical n
      (insert ∅ (Finset.image (fun i : Fin m => A (Fin.castLE hmk i)) Finset.univ))

Sources

• Gunnar Brinkmann and Robin Deklerck, "Generation of Union-Closed Sets and Moore Families", Journal of Integer Sequences 21 (2018), Article 18.1.7, Theorem thm:orderly, source lines 275–281, https://cs.uwaterloo.ca/journals/JIS/VOL21/Brinkmann/brink6.tex.

Uses 4

Statement usesCanonical family · Union-closed family · Set order

Proof usesPrefixes of a sorted canonical family are canonical

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.