Union-closed families, occurrences, density, nondegeneracy

Definition

TenChallenges_UnionClosed

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

extremal-set-theoryfranklunion-closed

The definitions behind Challenge 9 of the Ten Challenges benchmark, for a finite family $\mathcal F$ of finite subsets of a type $U$ .

Union-closed. $A\cup B\in\mathcal F$ whenever $A,B\in\mathcal F$ .
Occurrences. $\mathrm{occ}_{\mathcal F}(x)$ is the number of members of $\mathcal F$ containing $x$ .
Density. $\delta_{\mathcal F}(x)=\mathrm{occ}_{\mathcal F}(x)/\max(1,|\mathcal F|)$ , a rational number; for nonempty $\mathcal F$ this is the fraction of members containing $x$ .
Nondegenerate. $\mathcal F\ne\emptyset$ and $\mathcal F\ne\{\emptyset\}$ , the two union-closed families excluded from the conjecture.

Formalization Note. Families are Finset (Finset U) with [DecidableEq U]; the density is a quotient in ℚ, with the denominator $\max(1,|\mathcal F|)$ avoiding division by zero.

Definition code

import Mathlib.Data.Finset.Card
import Mathlib.Algebra.Order.Ring.Unbundled.Rat

variable {U : Type*} [DecidableEq U] (F : Finset (Finset U))

/-- A finite family of finite sets is union-closed. -/
def IsUnionClosed : Prop :=
  ∀ ⦃A B : Finset U⦄, A ∈ F → B ∈ F → A ∪ B ∈ F

/-- The number of members of the family containing `x`. -/
def occurrences (x : U) : ℕ :=
  (F.filter fun A => x ∈ A).card

/-- The density of an element with respect to a finite family. -/
def density (x : U) : ℚ :=
  (occurrences F x : ℚ) / max 1 F.card

/-- The two degenerate families excluded from the union-closed sets conjecture. -/
def Nondegenerate : Prop :=
  F ≠ ∅ ∧ F ≠ {∅}

Source

Ten Challenges repository, file Defs_and_Lems/UnionClosed.lean (commit ff14a56), https://github.com/TenChallenges/ten-challenges/blob/main/Defs_and_Lems/UnionClosed.lean; conjecture as in H. Bruhn, O. Schaudt, The journey of the union-closed sets conjecture, Graphs Combin. 31 (2015), Section 1.

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Setting shared by all four definitions. Throughout, $U$ is an arbitrary type (any collection of "elements": finite or infinite, possibly empty; it lives in an arbitrary but fixed universe), and $F$ is a finite set whose members are finite subsets of $U$ , i.e. a finite family of finite sets with no repeated members. The first three definitions additionally assume that $U$ carries a decidable equality (a procedure deciding whether two given elements of $U$ are equal); this is an extra parameter of those definitions. Write $|F|$ for the number of members of $F$ .

Definition IsUnionClosed (" $F$ is union-closed") is the proposition

\forall\, A, B \text{ finite subsets of } U:\qquad A \in F \;\wedge\; B \in F \;\Longrightarrow\; A \cup B \in F .

Here $A$ and $B$ range over all finite subsets of $U$ (the hypotheses $A \in F$ , $B \in F$ then restrict them), and $A = B$ is allowed. Nothing requires $F$ to be nonempty, to contain $\emptyset$ , to contain the whole union of its members, or to be closed under intersection. Edge cases: the empty family $F = \emptyset$ satisfies this vacuously; the family $\{\emptyset\}$ satisfies it; every one-member family $\{A\}$ satisfies it.

Definition occurrences assigns to $x \in U$ the natural number

\operatorname{occ}_F(x) \;=\; \bigl|\{\, A \in F \;:\; x \in A \,\}\bigr| ,

the number of members of $F$ that contain $x$ . It is $0$ when no member of $F$ contains $x$ (in particular for every $x$ when $F = \emptyset$ ), and it is at most $|F|$ .

Definition density assigns to $x \in U$ the rational number

\operatorname{dens}_F(x) \;=\; \frac{\operatorname{occ}_F(x)}{\max(1,\,|F|)} \;\in\; \mathbb{Q},

where the numerator $\operatorname{occ}_F(x)$ and the denominator $\max(1,|F|)$ are natural numbers (the maximum is taken among natural numbers) viewed as rationals. The denominator is always $\ge 1$ , so this is an ordinary quotient and the "division by zero gives zero" convention of the rationals is never invoked. If $F \neq \emptyset$ this equals $\operatorname{occ}_F(x) / |F|$ , a rational in $[0,1]$ (the fraction of members of $F$ containing $x$ ); if $F = \emptyset$ it equals $0/1 = 0$ for every $x$ .

Definition Nondegenerate (" $F$ is nondegenerate") is the proposition

F \neq \emptyset \quad\wedge\quad F \neq \{\emptyset\},

i.e. $F$ is neither the empty family nor the family whose only member is the empty set. (This definition takes no decidable-equality assumption.) It does not say that $\emptyset \notin F$ , and it does not require $F$ to have two or more members: for example $\{A\}$ with $A \neq \emptyset$ , and $\{\emptyset, A\}$ with $A \neq \emptyset$ , are both nondegenerate. Literally, the condition is equivalent to " $F$ has at least one member that is a nonempty set"; in particular a nondegenerate $F$ can only exist when $U$ has at least one element (if $U$ is empty, every $F$ is $\emptyset$ or $\{\emptyset\}$ ).

Human review

Endorsed by Shuze Chen · Nov 4, 2026
Confirmed by the moderator at approval.
Endorsed by utkuokur · Nov 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph