§3, p. 979 — a stable partition is stable with respect to any union of its blocks

Proved

PaigeTarjan.Coarsest.stableWrt_of_isUnionOfBlocks

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

coarsest-partitionp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1partition-refinement

Let $E$ be a relation on a finite set $U$ and let $Q$ be a stable partition of $U$ . For every subfamily $T \subseteq Q$ of blocks,

Q \text{ is stable with respect to } \textstyle\bigcup_{C \in T} C.

This observation is used in the proof of Lemma 2: a set that is a union of blocks of the current partition is also a union of blocks of any stable partition refining it, and so cannot split that partition.

Formalization Note The empty subfamily is allowed; its union is $\emptyset$ , whose preimage is empty, so the statement holds for it as well.

Preamble

import Mathlib
import Definitions.Def_PaigeTarjan_Coarsest_Basic

Formal statement

namespace PaigeTarjan.Coarsest

/-- §3, p. 979, end of the first paragraph: a stable partition is stable with respect to the
union of any subset of its blocks. -/
theorem stableWrt_of_isUnionOfBlocks {U : Type*} [Fintype U] [DecidableEq U]
    (E : U → U → Prop) [DecidableRel E] (Q : Finset (Finset U))
    (hQ : IsPartition Q) (hstab : Stable E Q) (T : Finset (Finset U)) (hT : T ⊆ Q) :
    StableWrt E Q (T.biUnion id) := by sorry

end PaigeTarjan.Coarsest

Source

Paige, Tarjan, Three Partition Refinement Algorithms, SIAM J. Comput. 16 (1987), p. 979, §3, first paragraph, last sentence

Read-back

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

Take a finite set $U$ with decidable equality, a decidable binary relation $E$ on $U$ , and a family $Q$ of subsets of $U$ . Assume:

$Q$ is a partition of $U$ ;
$Q$ is stable, meaning that for every pair of blocks $B, S \in Q$ , either $B \subseteq E^{-1}(S)$ or $B \cap E^{-1}(S) = \varnothing$ , where $E^{-1}(S) = \{x : \exists y \in S,\ x \mathrel{E} y\}$ .

Then for every subfamily $T \subseteq Q$ , $Q$ is stable with respect to $\bigcup_{C \in T} C$ . That is, every block $B \in Q$ satisfies

B \subseteq E^{-1}\Bigl(\bigcup_{C \in T} C\Bigr) \quad\text{or}\quad B \cap E^{-1}\Bigl(\bigcup_{C \in T} C\Bigr) = \varnothing.

Degenerate cases.

$T = \varnothing$ gives the union $\varnothing$ , whose preimage is empty, so the claim holds trivially.
$T = Q$ gives the union $U$ (when $U$ is nonempty). The claim is then that each block either lies entirely inside the set of elements with at least one $E$ -successor, or contains no such element.
If $U = \varnothing$ , then $Q$ and $T$ are empty and the claim is vacuous.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph