Finite.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

33 declarations, 0 contain sorry, 0 declared as axioms

Finite hypergraphs and block designs

Finite hypergraphs are finite families of finite vertex sets. This file supplies uniformity, weak vertex coloring, independent sets, transversals, designs, and finite extremal counts. Finset.toHypergraph connects this presentation to Mathlib's Hypergraph.

The ground type includes isolated vertices. The support is H.biUnion id when only incident vertices should be counted. Colorings require two differently colored vertices in every edge; empty and singleton edges therefore admit no proper coloring.

Imports (6)

Imported by 3 files

def Set.HasFiniteTransversal A family of finite sets has a transversal with at most k vertices line 42 source
Source documentation
A family of finite sets has a transversal with at most k vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Finset, Nat
Proof uses: Exists, And, LE.le, Finset.card, Membership.mem
4 instances, coercions and auxiliary constants left out.
```
def HasFiniteTransversal {V : Type*} (F : Set (Finset V)) (k : ℕ) : Prop :=
…
```
def Finset.IsUniform Every edge has exactly r vertices line 52 source
Source documentation
Every edge has exactly r vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Membership.mem, Eq, Finset.card
2 instances, coercions and auxiliary constants left out.
```
def IsUniform (H : Finset (Finset V)) (r : ℕ) : Prop := ∀ e ∈ H, e.card = r
```
def Finset.toHypergraph The hypergraph with edge family H and ground vertex set S line 55 source
Source documentation
The hypergraph with edge family H and ground vertex set S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Membership.mem, LE.le, Hypergraph
Proof uses: Hypergraph.ofEdgeFamily
11 instances, coercions and auxiliary constants left out.
```
def toHypergraph (H : Finset (Finset V)) (S : Finset V) (h : ∀ e ∈ H, e ⊆ S) :
    Hypergraph V :=
…
```
theorem Finset.isUniform_toHypergraph_iff Conversion preserves uniformity line 62 source
Source documentation
Conversion preserves uniformity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Membership.mem, LE.le, Nat, Iff, Hypergraph.IsUniform, Finset.toHypergraph, Finset.IsUniform
Proof uses: Hypergraph.isUniform_ofEdgeFamily_iff
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isUniform_toHypergraph_iff (H : Finset (Finset V)) (S : Finset V)
    (h : ∀ e ∈ H, e ⊆ S) (r : ℕ) :
    (H.toHypergraph S h).IsUniform r ↔ H.IsUniform r := by
…
```
Mentions: Finset.IsUniform
def Finset.IsProperHypergraphColoring A weak proper coloring has no monochromatic edge line 68 source
Source documentation
A weak proper coloring has no monochromatic edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset
Proof uses: Membership.mem, Exists, And, Ne
2 instances, coercions and auxiliary constants left out.
```
def IsProperHypergraphColoring (H : Finset (Finset V)) {C : Type*} (c : V → C) : Prop :=
…
```
Mentions: c
theorem Finset.isProperColoring_toHypergraph_iff Conversion preserves weak proper colorings line 74 source
Source documentation
Conversion preserves weak proper colorings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Membership.mem, LE.le, Iff, Hypergraph.IsProperColoring, Finset.toHypergraph, Finset.IsProperHypergraphColoring
Proof uses: Hypergraph.isProperColoring_ofEdgeFamily_iff
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isProperColoring_toHypergraph_iff {C : Type*} (H : Finset (Finset V))
    (S : Finset V) (h : ∀ e ∈ H, e ⊆ S) (f : V → C) :
    (H.toHypergraph S h).IsProperColoring f ↔ H.IsProperHypergraphColoring f := by
…
```
def Finset.HypergraphColorable The edge family admits a weak proper coloring with k colors line 80 source
Source documentation
The edge family admits a weak proper coloring with k colors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Exists, Fin, Finset.IsProperHypergraphColoring
```
def HypergraphColorable (H : Finset (Finset V)) (k : ℕ) : Prop :=
…
```
theorem Finset.hypergraphColorable_two_iff Two-colorability agrees with the existing Property B predicate line 85 source
Source documentation
Two-colorability agrees with the existing Property B predicate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Iff, Finset.HypergraphColorable, OfNat.ofNat, Nat, Finset.HasPropertyB
Proof uses: Iff.rfl
2 instances, coercions and auxiliary constants left out.
```
theorem hypergraphColorable_two_iff (H : Finset (Finset V)) :
    H.HypergraphColorable 2 ↔ H.HasPropertyB := Iff.rfl
```
def Finset.HasHypergraphChromaticNumber The weak chromatic number is exactly k line 89 source
Source documentation
The weak chromatic number is exactly k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: And, Finset.HypergraphColorable, LT.lt, Not
1 instances, coercions and auxiliary constants left out.
```
def HasHypergraphChromaticNumber (H : Finset (Finset V)) (k : ℕ) : Prop :=
…
```
def Finset.IsHypergraphIndependent No edge is contained in this set of vertices line 93 source
Source documentation
No edge is contained in this set of vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset
Proof uses: Membership.mem, Not, LE.le
5 instances, coercions and auxiliary constants left out.
```
def IsHypergraphIndependent (H : Finset (Finset V)) (S : Finset V) : Prop :=
…
```
def Finset.hypergraphDegree The number of hyperedges containing a vertex line 97 source
Source documentation
The number of hyperedges containing a vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Nat
Proof uses: Finset.card, Finset.filter, Membership.mem
3 instances, coercions and auxiliary constants left out.
```
def hypergraphDegree (H : Finset (Finset V)) (v : V) : ℕ := #{e ∈ H | v ∈ e}
```
def Finset.IsLinearHypergraph Distinct edges intersect in at most one vertex line 100 source
Source documentation
Distinct edges intersect in at most one vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset
Proof uses: Set.Pairwise, LE.le, Nat, Finset.card, Inter.inter, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def IsLinearHypergraph (H : Finset (Finset V)) : Prop :=
…
```
def Finset.ContainsSubgraph Some m vertices span at least k edges line 104 source
Source documentation
Some m vertices span at least k edges.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Nat
Proof uses: Exists, And, Eq, Finset.card, LE.le, Finset.filter
5 instances, coercions and auxiliary constants left out.
```
def ContainsSubgraph (H : Finset (Finset V)) (m k : ℕ) : Prop :=
…
```
def Finset.hypergraphInduce The edges induced on a vertex set line 108 source
Source documentation
The edges induced on a vertex set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset
Proof uses: Finset.filter, LE.le
4 instances, coercions and auxiliary constants left out.
```
def hypergraphInduce (H : Finset (Finset V)) (S : Finset V) : Finset (Finset V) :=
…
```
def Finset.ContainsCompleteHypergraph A copy of the complete r-uniform hypergraph on k vertices line 112 source
Source documentation
A copy of the complete r-uniform hypergraph on k vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Exists, And, Eq, Finset.card, LE.le, Finset.powersetCard
3 instances, coercions and auxiliary constants left out.
```
def ContainsCompleteHypergraph (H : Finset (Finset V)) (r k : ℕ) : Prop :=
…
```
def Finset.HasHypergraphMatching A collection of k pairwise vertex-disjoint edges line 116 source
Source documentation
A collection of k pairwise vertex-disjoint edges.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Exists, And, LE.le, Eq, Finset.card, Set.Pairwise, Disjoint
6 instances, coercions and auxiliary constants left out.
```
def HasHypergraphMatching (H : Finset (Finset V)) (k : ℕ) : Prop :=
…
```
def Finset.IsBlockDesign Every t-set of ground vertices lies in exactly one block line 120 source
Source documentation
Every t-set of ground vertices lies in exactly one block.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: And, Finset.IsUniform, Eq, Finset.card, ExistsUnique, Membership.mem, LE.le
5 instances, coercions and auxiliary constants left out.
```
def IsBlockDesign (H : Finset (Finset V)) (t k : ℕ) : Prop :=
…
```
def Finset.IsPairwiseBalancedDesign A pairwise balanced design, permitting a block equal to the ground set line 124 source
Source documentation
A pairwise balanced design, permitting a block equal to the ground set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset
Proof uses: And, Membership.mem, LE.le, Nat, OfNat.ofNat, Finset.card, Eq, ExistsUnique
7 instances, coercions and auxiliary constants left out.
```
def IsPairwiseBalancedDesign (H : Finset (Finset V)) : Prop :=
…
```
def Finset.blockSizeProfile The nondecreasing block-size sequence, retaining repeated sizes line 129 source
Source documentation
The nondecreasing block-size sequence, retaining repeated sizes.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, List, Nat
Proof uses: Multiset.sort, Multiset.map, Finset.card, Finset.val, LE.le
7 instances, coercions and auxiliary constants left out.
```
def blockSizeProfile (H : Finset (Finset V)) : List ℕ :=
…
```
def Finset.IsCompleteHypergraphDecomposition Partition into complete r-graphs with either r or r+1 vertices line 133 source
Source documentation
Partition into complete r-graphs with either r or r+1 vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Nat
Proof uses: And, Membership.mem, Or, Eq, Finset.card, HAdd.hAdd, OfNat.ofNat, Finset.biUnion, Finset.powersetCard, Set.Pairwise, Disjoint
9 instances, coercions and auxiliary constants left out.
```
def IsCompleteHypergraphDecomposition (H : Finset (Finset V)) (r : ℕ)
    (D : Finset (Finset V)) : Prop :=
…
```
def Finset.ContainsCompletePartiteHypergraph A complete t-partite t-uniform hypergraph with r vertices in each part line 140 source
Source documentation
A complete t-partite t-uniform hypergraph with r vertices in each part.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Nat
Proof uses: Exists, Function.Embedding, Prod, Fin, Membership.mem, Finset.image, Prod.mk, Finset.univ
5 instances, coercions and auxiliary constants left out.
```
def ContainsCompletePartiteHypergraph (H : Finset (Finset V)) (t r : ℕ) : Prop :=
…
```
def Finset.HasRepeatedDisjointUnion Two distinct disjoint pairs of edges with the same union line 145 source
Source documentation
Two distinct disjoint pairs of edges with the same union.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset
Proof uses: Exists, And, Membership.mem, Disjoint, Eq, Union.union, Ne
5 instances, coercions and auxiliary constants left out.
```
def HasRepeatedDisjointUnion (H : Finset (Finset V)) : Prop :=
…
```
theorem Finset.isUniform_empty line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset.IsUniform, EmptyCollection.emptyCollection, Finset
Proof uses: of_eq_true, Membership.mem, Eq, Finset.card, Eq.trans, True, forall_congr, False, implies_congr, Eq.refl, implies_true
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Finset.containsSubgraph_iff The cardinal bound in ContainsSubgraph counts edges, not copies with labels line 155 source
Source documentation
The cardinal bound in ContainsSubgraph counts edges, not copies with labels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Nat, Iff, Finset.ContainsSubgraph, Exists, And, Eq, Finset.card, LE.le, Finset.hypergraphInduce
Proof uses: Iff.rfl
1 instances, coercions and auxiliary constants left out.
```
theorem containsSubgraph_iff (H : Finset (Finset V)) (m k : ℕ) :
    H.ContainsSubgraph m k ↔ ∃ S : Finset V,
      S.card = m ∧ k ≤ (H.hypergraphInduce S).card := Iff.rfl
…
```
theorem Finset.not_colorable_singleton A singleton edge prevents any weak proper coloring line 161 source
Source documentation
A singleton edge prevents any weak proper coloring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Finset.HypergraphColorable, Singleton.singleton, Finset
Proof uses: Fin, Finset.IsProperHypergraphColoring, False, False.elim, Eq.mp, Eq.trans, Membership.mem, Exists, And, Eq, forall_congr, implies_congr, Eq.refl, congrArg, funext, congr, congrFun', True, eq_self, not_true_eq_false
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem not_colorable_singleton (v : V) (k : ℕ) :
    ¬ ({ {v} } : Finset (Finset V)).HypergraphColorable k := by
…
```
Mentions: Finset.HypergraphColorable
def Finset.hypergraphIndependenceNumber The largest cardinality of an independent vertex set in a finite ground type line 168 source
Source documentation
The largest cardinality of an independent vertex set in a finite ground type.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Finset, Nat
Proof uses: Finset.sup, Finset.filter, Finset.IsHypergraphIndependent, Classical.propDecidable, Finset.powerset, Finset.univ, Finset.card
3 instances, coercions and auxiliary constants left out.
```
noncomputable def hypergraphIndependenceNumber [Fintype V] (H : Finset (Finset V)) : ℕ :=
…
```
def Finset.propertyBWitnesses Subsets of the incident vertices witnessing Property B line 173 source
Source documentation
Subsets of the incident vertices witnessing Property B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset
Proof uses: Finset.filter, And, Membership.mem, Finset.Nonempty, Inter.inter, Finset.IsHypergraphIndependent, Classical.propDecidable, Finset.powerset, Finset.biUnion, id
6 instances, coercions and auxiliary constants left out.
```
noncomputable def propertyBWitnesses (H : Finset (Finset V)) : Finset (Finset V) :=
…
```
def Hypergraph.extremalNumber Maximum number of edges among r-uniform families satisfying P on n labeled vertices line 184 source
Source documentation
Maximum number of edges among r-uniform families satisfying P on n labeled vertices. The value is zero if no family is admissible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin
Proof uses: Finset.sup, Finset.filter, Classical.propDecidable, Finset.powerset, Finset.powersetCard, Finset.univ, Finset.card
4 instances, coercions and auxiliary constants left out.
```
noncomputable def extremalNumber (n r : ℕ) (P : Finset (Finset (Fin n)) → Prop) : ℕ :=
…
```
def Hypergraph.cliqueExtremalNumber The extremal number forbidding a complete uniform hypergraph line 188 source
Source documentation
The extremal number forbidding a complete uniform hypergraph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Hypergraph.extremalNumber, Finset, Fin, Not, Finset.ContainsCompleteHypergraph
```
noncomputable def cliqueExtremalNumber (n r k : ℕ) : ℕ :=
…
```
def Hypergraph.configurationExtremalNumber The extremal number forbidding e edges on v vertices (not necessarily induced) line 192 source
Source documentation
The extremal number forbidding e edges on v vertices (not necessarily induced).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Hypergraph.extremalNumber, Finset, Fin, Not, Finset.ContainsSubgraph
1 instances, coercions and auxiliary constants left out.
```
noncomputable def configurationExtremalNumber (n r v e : ℕ) : ℕ :=
…
```
def Hypergraph.partiteExtremalNumber The extremal number forbidding a complete balanced multipartite uniform hypergraph line 196 source
Source documentation
The extremal number forbidding a complete balanced multipartite uniform hypergraph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Hypergraph.extremalNumber, Finset, Fin, Not, Finset.ContainsCompletePartiteHypergraph
1 instances, coercions and auxiliary constants left out.
```
noncomputable def partiteExtremalNumber (n t r : ℕ) : ℕ :=
…
```
def Hypergraph.minChromaticEdges Minimum edge count for chromatic number k, with infinity when no such graph exists line 200 source
Source documentation
Minimum edge count for chromatic number k, with infinity when no such graph exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ENat
Proof uses: iInf, Finset, Fin, Finset.IsUniform, Finset.HasHypergraphChromaticNumber, Finset.card
9 instances, coercions and auxiliary constants left out.
```
noncomputable def minChromaticEdges (r k : ℕ) : ℕ∞ :=
…
```
def Hypergraph.blockSizeProfiles All block-size sequences of pairwise balanced designs on n labeled vertices line 206 source
Source documentation
All block-size sequences of pairwise balanced designs on n labeled vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, List
Proof uses: Finset.image, Fin, Finset.blockSizeProfile, Finset.filter, Finset.IsPairwiseBalancedDesign, Classical.propDecidable, Finset.powerset, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
noncomputable def blockSizeProfiles (n : ℕ) : Finset (List ℕ) :=
…
```