UnionClosed.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

11 declarations, 5 contain sorry, 0 declared as axioms

Union-closed sets conjecture

Reference: Wikipedia

In this file, we:

state the conjecture
state three solved variants of the conjecture, without proof
prove two solved variants of the conjecture
prove the conjecture is sharp

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

abbrev UnionClosed.IsUnionClosed line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset
Proof uses: Membership.mem, Union.union
3 instances, coercions and auxiliary constants left out.
lemma UnionClosed.isUnionClosed_univ line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, UnionClosed.IsUnionClosed, Finset.univ, Finset
Proof uses: of_eq_true, Membership.mem, Union.union, Eq.trans, True, forall_congr, implies_congr, implies_true
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma UnionClosed.isUnionClosed_powerset line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, UnionClosed.IsUnionClosed, Finset.powerset
Proof uses: Membership.mem, Eq.mpr, Union.union, LE.le, id, Eq, congrArg, propext, Finset.mem_powerset, Finset.union_subset, Eq.mp
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem UnionClosed.union_closed For every finite union-closed family of sets, other than the family containing only the empty set, there exists an element that belongs to at least half of the sets in the family sorry line 59 source
Source documentation
For every finite union-closed family of sets, other than the family containing only the empty set, there exists an element that belongs to at least half of the sets in the family.

depends on sorry what this means
Statement uses: DecidableEq, Finset, Nonempty, Ne, Singleton.singleton, EmptyCollection.emptyCollection, UnionClosed.IsUnionClosed, Exists, LE.le, Rat, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Finset.card, Finset.filter, Membership.mem
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem union_closed
    [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A) :
    ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := by
…
```
Mentions: UnionClosed.IsUnionClosed
theorem UnionClosed.union_closed.variants.yu Yu [Yu23] showed that the union-closed sets conjecture holds with a constant of approximately 0.38234 instead of 1/2 sorry line 72 source
Source documentation
Yu [Yu23] showed that the union-closed sets conjecture holds with a constant of approximately 0.38234 instead of 1/2. [Yu23] Yu, Lei (2023). "Dimension-free bounds for the union-closed sets conjecture". Entropy. 25 (5): 767.

depends on sorry what this means
Statement uses: DecidableEq, Finset, Nonempty, Ne, Singleton.singleton, EmptyCollection.emptyCollection, UnionClosed.IsUnionClosed, Exists, LE.le, Rat, HMul.hMul, OfScientific.ofScientific, Bool.true, Finset.card, Finset.filter, Membership.mem
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem union_closed.variants.yu
    [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A) :
    ∃ i : n, (0.38234 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := by
…
```
Mentions: UnionClosed.IsUnionClosed
theorem UnionClosed.union_closed.variants.univ_card Vuckovic and Zivkovic [Vu17] showed that the union-closed sets conjecture holds for set families whose universal set has cardinality at most 12 sorry line 85 source
Source documentation
Vuckovic and Zivkovic [Vu17] showed that the union-closed sets conjecture holds for set families whose universal set has cardinality at most 12. [Vu17] Vuckovic, Bojan; Zivkovic, Miodrag (2017). "The 12-Element Case of Frankl's Conjecture" (PDF). IPSI BGD Transactions on Internet Research. 13 (1): 65.

depends on sorry what this means
Statement uses: DecidableEq, Finset, Fintype, Nonempty, Ne, Singleton.singleton, EmptyCollection.emptyCollection, UnionClosed.IsUnionClosed, LE.le, Nat, Fintype.card, OfNat.ofNat, Exists, Rat, HMul.hMul, HDiv.hDiv, Finset.card, Finset.filter, Membership.mem
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem union_closed.variants.univ_card
    [Fintype n] [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A)
    (h_card : Fintype.card n ≤ 12) :
    ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := by
…
```
Mentions: UnionClosed.IsUnionClosed
theorem UnionClosed.union_closed.variants.family_card Roberts and Simpson [Ro10] showed that the union-closed sets conjecture holds for set families of size at most 46 sorry line 102 source
Source documentation
Roberts and Simpson [Ro10] showed that the union-closed sets conjecture holds for set families of size at most 46. Their method, however, combined with the result of [Vu17], further shows that it holds for #A ≤ 50 as well. [Ro10] Roberts, Ian; Simpson, Jamie (2010). "A note on the union-closed sets conjecture" (PDF). Australas. J. Combin. 47: 265–267. [Vu17] Vuckovic, Bojan; Zivkovic, Miodrag (2017). "The 12-Element Case of Frankl's Conjecture" (PDF). IPSI BGD Transactions on Internet Research. 13 (1): 65.

depends on sorry what this means
Statement uses: DecidableEq, Finset, Nonempty, Ne, Singleton.singleton, EmptyCollection.emptyCollection, UnionClosed.IsUnionClosed, LE.le, Nat, Finset.card, OfNat.ofNat, Exists, Rat, HMul.hMul, HDiv.hDiv, Finset.filter, Membership.mem
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem union_closed.variants.family_card
    [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A)
    (hA : #A ≤ 50) :
    ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := by
…
```
Mentions: UnionClosed.IsUnionClosed
theorem UnionClosed.union_closed.variants.univ_card_two We can show the union-closed sets conjecture is true for the case where the universal set has cardinality 2, by brute force line 115 source
Source documentation
We can show the union-closed sets conjecture is true for the case where the universal set has cardinality 2, by brute force.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat, Ne, Singleton.singleton, EmptyCollection.emptyCollection, UnionClosed.IsUnionClosed, Exists, LE.le, Rat, HMul.hMul, HDiv.hDiv, Finset.card, Finset.filter, Membership.mem
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem union_closed.variants.univ_card_two (A : Finset (Finset (Fin 2)))
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A) :
    ∃ i, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := by
…
```
Mentions: UnionClosed.IsUnionClosed
theorem UnionClosed.union_closed.variants.singleton_mem We can show the union-closed sets conjecture is true for the case where the set family contains some singleton line 126 source
Source documentation
We can show the union-closed sets conjecture is true for the case where the set family contains some singleton.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, UnionClosed.IsUnionClosed, Membership.mem, Singleton.singleton, Exists, LE.le, Rat, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Finset.card, Finset.filter
Proof uses: Exists.intro, Not, Eq.mpr, id, Eq, congrArg, rfl, Set.InjOn, Insert.insert, forall_congr, Set, Eq.trans, Set.ofPred, And, implies_congr, congrFun', Finset.coe_filter, Eq.refl, Finset.erase, Eq.mp and 39 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem union_closed.variants.singleton_mem
    (h_union_closed : IsUnionClosed A)
    (i : n) (hi : {i} ∈ A) :
    ∃ i, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := by
…
```
Mentions: UnionClosed.IsUnionClosed
theorem UnionClosed.union_closed.variants.sharpness The union-closed sets conjecture is sharp in the sense that if we replace the constant 1/2 with any larger constant, then the conjecture fails line 155 source
Source documentation
The union-closed sets conjecture is sharp in the sense that if we replace the constant 1/2 with any larger constant, then the conjecture fails.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, Real, LT.lt, HDiv.hDiv, OfNat.ofNat, Nat, Not, Finset, Ne, Singleton.singleton, EmptyCollection.emptyCollection, UnionClosed.IsUnionClosed, Exists, LE.le, HMul.hMul, Finset.card, Finset.filter, Membership.mem
Proof uses: IsEmpty, Nonempty, Or, False, isEmpty_or_nonempty, of_eq_true, Eq.trans, Eq, True, congrFun', congrArg, Eq.mp, implies_congr, Eq.refl, funext, congr, CharP.cast_eq_zero, MulZeroClass.mul_zero, Finset.filter_empty, Union.union and 138 more
220 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
theorem union_closed.variants.sharpness [Fintype n] (c : ℝ) (hc : 1 / 2 < c) :
    ¬ (∀ A : Finset (Finset n), A ≠ {∅} → IsUnionClosed A →
        ∃ i : n, c * #A ≤ #{x ∈ A | i ∈ x}) := by
…
```
Mentions: c, UnionClosed.IsUnionClosed
theorem UnionClosed.union_closed.variants.cardinality_even_of_union_closed_tight Documented declaration: cardinality_even_of_union_closed_tight sorry line 216 source
Source documentation
The union-closed sets conjecture is tight for a union-closed family A if the largest number of sets in A containing a common element is exactly half of the sets in A, that is, $\max_i |\{X \in A : i \in X\}| = |A| / 2$.
If the union-closed sets conjecture is tight for some family A then $|A| = 2^k$ for some $k$. This is the first part of Conjecture 3 in the reference below; its second part (that the family then contains the power set of a $k$-element set as a "submatrix") is not formalized here.
Reference: Conjecture 3 in https://www.nieuwarchief.nl/serie5/pdf/naw5-2023-24-4-225.pdf.

depends on sorry what this means
Statement uses: DecidableEq, Finset, Nonempty, Ne, Singleton.singleton, EmptyCollection.emptyCollection, UnionClosed.IsUnionClosed, IsGreatest, Rat, Set.range, Finset.card, Finset.filter, Membership.mem, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Exists, Nat, Eq, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem union_closed.variants.cardinality_even_of_union_closed_tight
    [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_ne_empty : A ≠ ∅)
    (h_union_closed : IsUnionClosed A)
    (h_tight : IsGreatest (Set.range fun i : n => (#{x ∈ A | i ∈ x} : ℚ)) ((1 / 2 : ℚ) * #A)) :
    ∃ k, #A = 2 ^ k := by
…
```
Mentions: UnionClosed.IsUnionClosed