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

16 declarations, 0 contain sorry, 0 declared as axioms

Uniform hypergraphs

A UniformHypergraph V k extends Mathlib's Hypergraph V with uniformity k and vertex set Set.univ. The vertex type includes isolated vertices. Finite edge families use Finset.IsUniform; UniformHypergraph.ofFinset converts them to this presentation.

The API includes complete subgraphs, maximal clique sizes, weak colorings, embeddings, and chromatic cardinals. The chromatic cardinal is zero when no proper coloring exists. Empty and singleton edges admit no weak proper coloring.

Imports (3)

Imported by 1 file

FormalConjecturesForMathlib.lean

structure UniformHypergraph A uniform Mathlib hypergraph whose vertex set is the entire ambient type line 42 source
Source documentation
A uniform Mathlib hypergraph whose vertex set is the entire ambient type.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
```
structure UniformHypergraph (V : Type*) (k : ℕ) extends Hypergraph V where
…
```
def UniformHypergraph.ofFinset A finite uniform edge family viewed as a uniform hypergraph line 53 source
Source documentation
A finite uniform edge family viewed as a uniform hypergraph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Finset.IsUniform, UniformHypergraph
Proof uses: Hypergraph, Hypergraph.ofEdgeFamily, Set.univ, UniformHypergraph.mk
5 instances, coercions and auxiliary constants left out.
```
def ofFinset {V : Type*} (H : Finset (Finset V)) (hH : H.IsUniform k) :
    UniformHypergraph V k where
…
```
Mentions: UniformHypergraph
theorem UniformHypergraph.mem_edgeSet_ofFinset line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Finset.IsUniform, Iff, Membership.mem, Set, Hypergraph.edgeSet, UniformHypergraph.toHypergraph, UniformHypergraph.ofFinset
Proof uses: Hypergraph.mem_edgeSet_ofEdgeFamily, Set.univ, Set.subset_univ
7 instances, coercions and auxiliary constants left out.
def UniformHypergraph.IsCompleteOn Every k-element subset of S is an edge line 66 source
Source documentation
Every k-element subset of S is an edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph, Finset
Proof uses: LE.le, Eq, Finset.card, Membership.mem, Set, Hypergraph.edgeSet, UniformHypergraph.toHypergraph
6 instances, coercions and auxiliary constants left out.
```
def IsCompleteOn {V : Type*} (H : UniformHypergraph V k) (S : Finset V) : Prop :=
…
```
Mentions: UniformHypergraph
def UniformHypergraph.cliqueSizes The sizes of the finite maximal complete subgraphs line 70 source
Source documentation
The sizes of the finite maximal complete subgraphs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph, Set
Proof uses: Set.ofPred, Exists, Finset, And, Maximal, UniformHypergraph.IsCompleteOn, Eq, Finset.card
3 instances, coercions and auxiliary constants left out.
```
def cliqueSizes {V : Type*} (H : UniformHypergraph V k) : Set ℕ :=
…
```
Mentions: UniformHypergraph
abbrev UniformHypergraph.IsProperColoring Weak proper coloring of the underlying Mathlib hypergraph line 74 source
Source documentation
Weak proper coloring of the underlying Mathlib hypergraph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph
Proof uses: Hypergraph.IsProperColoring, UniformHypergraph.toHypergraph
```
abbrev IsProperColoring {V : Type*} (H : UniformHypergraph V k) {C : Type*}
    (f : V → C) : Prop :=
…
```
Mentions: UniformHypergraph
theorem UniformHypergraph.isProperColoring_of_injective An injective coloring is proper when every edge has at least two vertices line 79 source
Source documentation
An injective coloring is proper when every edge has at least two vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph, LE.le, OfNat.ofNat, Function.Injective, UniformHypergraph.IsProperColoring
Proof uses: Hypergraph.IsUniform.isProperColoring_of_injective, UniformHypergraph.toHypergraph, UniformHypergraph.uniform
4 instances, coercions and auxiliary constants left out.
```
theorem isProperColoring_of_injective {V C : Type*} (H : UniformHypergraph V k)
    (hk : 2 ≤ k) {f : V → C} (hf : Function.Injective f) : H.IsProperColoring f :=
…
```
Mentions: UniformHypergraph
theorem UniformHypergraph.isProperColoring_ofFinset_iff The finite and possibly infinite presentations have the same proper colorings line 84 source
Source documentation
The finite and possibly infinite presentations have the same proper colorings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Finset.IsUniform, Iff, UniformHypergraph.IsProperColoring, UniformHypergraph.ofFinset, Finset.IsProperHypergraphColoring
Proof uses: Hypergraph.isProperColoring_ofEdgeFamily_iff, Set.univ, Membership.mem, Set, Set.subset_univ
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isProperColoring_ofFinset_iff {V C : Type*} (H : Finset (Finset V))
    (hH : H.IsUniform k) (f : V → C) :
    (ofFinset H hH).IsProperColoring f ↔ H.IsProperHypergraphColoring f := by
…
```
Mentions: UniformHypergraph.ofFinset, UniformHypergraph.IsProperColoring
def UniformHypergraph.chromaticCardinal The infimum of cardinalities of color types admitting a proper coloring line 91 source
Source documentation
The infimum of cardinalities of color types admitting a proper coloring. The value is zero when no proper coloring exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph, Cardinal
Proof uses: InfSet.sInf, Set.ofPred, Exists, And, Eq, Cardinal.mk, UniformHypergraph.IsProperColoring
6 instances, coercions and auxiliary constants left out.
```
noncomputable def chromaticCardinal {V : Type u} (H : UniformHypergraph V k) : Cardinal.{u} :=
…
```
Mentions: UniformHypergraph
theorem UniformHypergraph.chromaticCardinal_le A proper coloring bounds the chromatic cardinal by the number of colors line 95 source
Source documentation
A proper coloring bounds the chromatic cardinal by the number of colors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph, UniformHypergraph.IsProperColoring, LE.le, Cardinal, UniformHypergraph.chromaticCardinal, Cardinal.mk
Proof uses: csInf_le', Set.ofPred, Exists, And, Eq, Exists.intro, And.intro, rfl
2 instances, coercions and auxiliary constants left out.
```
theorem chromaticCardinal_le {V C : Type u} (H : UniformHypergraph V k)
    {f : V → C} (hf : H.IsProperColoring f) : H.chromaticCardinal ≤ #C :=
…
```
Mentions: UniformHypergraph
theorem UniformHypergraph.chromaticCardinal_le_mk The vertex type itself always supplies enough colors when 2 ≤ k line 100 source
Source documentation
The vertex type itself always supplies enough colors when 2 ≤ k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph, LE.le, OfNat.ofNat, Cardinal, UniformHypergraph.chromaticCardinal, Cardinal.mk
Proof uses: UniformHypergraph.chromaticCardinal_le, id, UniformHypergraph.isProperColoring_of_injective, Function.injective_id
5 instances, coercions and auxiliary constants left out.
```
theorem chromaticCardinal_le_mk {V : Type u} (H : UniformHypergraph V k) (hk : 2 ≤ k) :
    H.chromaticCardinal ≤ #V :=
…
```
Mentions: UniformHypergraph
def UniformHypergraph.Appears An injective vertex map carrying every edge of F to an edge of H line 105 source
Source documentation
An injective vertex map carrying every edge of F to an edge of H.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph
Proof uses: Exists, And, Function.Injective, LE.le, Set, Hypergraph.edgeSet, Hypergraph.image, UniformHypergraph.toHypergraph
1 instances, coercions and auxiliary constants left out.
```
def Appears {W V : Type*} (F : UniformHypergraph W k)
    (H : UniformHypergraph V k) : Prop :=
…
```
Mentions: UniformHypergraph
theorem UniformHypergraph.Appears.trans Appearance is transitive under composition of injective vertex maps line 111 source
Source documentation
Appearance is transitive under composition of injective vertex maps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph, UniformHypergraph.Appears
Proof uses: And, Function.Injective, LE.le, Set, Hypergraph.edgeSet, Hypergraph.image, UniformHypergraph.toHypergraph, Exists.intro, Function.comp, And.intro, Function.Injective.comp, Eq.mpr, id, Eq, congrArg, Hypergraph, Eq.symm, Hypergraph.image_image, LE.le.trans, Set.image and 1 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem Appears.trans {U W V : Type*} {F : UniformHypergraph U k}
    {G : UniformHypergraph W k} {H : UniformHypergraph V k}
    (hFG : F.Appears G) (hGH : G.Appears H) : F.Appears H := by
…
```
Mentions: UniformHypergraph
abbrev UniformHypergraph.IsNColorable A weak proper coloring using at most n colors line 121 source
Source documentation
A weak proper coloring using at most n colors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph
Proof uses: Hypergraph.IsNColorable, UniformHypergraph.toHypergraph
```
abbrev IsNColorable {V : Type*} (F : UniformHypergraph V k) (n : ℕ) : Prop :=
…
```
Mentions: UniformHypergraph
def UniformHypergraph.HasAvoidingChromaticCardinal Some hypergraph of the same uniformity and chromatic cardinal κ omits F line 125 source
Source documentation
Some hypergraph of the same uniformity and chromatic cardinal κ omits F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, UniformHypergraph, Cardinal
Proof uses: Exists, DecidableEq, And, Eq, UniformHypergraph.chromaticCardinal, Not, UniformHypergraph.Appears
```
def HasAvoidingChromaticCardinal {W : Type u} (F : UniformHypergraph W k)
    (κ : Cardinal.{u}) : Prop :=
…
```
Mentions: UniformHypergraph
def UniformHypergraph.IsObligatory A finite uniform hypergraph is obligatory if it appears in every hypergraph of that uniformity whose chromatic cardinal exceeds ℵ₀ line 132 source
Source documentation
A finite uniform hypergraph is obligatory if it appears in every hypergraph of that uniformity whose chromatic cardinal exceeds ℵ₀.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fintype, UniformHypergraph
Proof uses: DecidableEq, LT.lt, Cardinal, Cardinal.aleph0, UniformHypergraph.chromaticCardinal, UniformHypergraph.Appears
3 instances, coercions and auxiliary constants left out.
```
def IsObligatory {W : Type u} [Fintype W] (F : UniformHypergraph W k) : Prop :=
…
```
Mentions: UniformHypergraph