Statement of Erdős Problem 111: bipartizing finite subgraphs of uncountably chromatic graphs

These are the definitions from the upstream project's Mathlib-only Challenge.lean. The source and upstream comparison records are linked in the project card.

noncomputable def Erdos111.bipartizationNumber {V : Type u_1} {G : SimpleGraph V} (H : G.Subgraph) : ℕ

The least number of edges whose deletion leaves the subgraph H bipartite, for H with finitely many vertices (the only case used below).

Equations

• Erdos111.bipartizationNumber H = sInf {k : ℕ | ∃ D ⊆ H.edgeSet, D.ncard = k ∧ (H.deleteEdges D).coe.IsBipartite}

noncomputable def Erdos111.h {V : Type u_1} (G : SimpleGraph V) (n : ℕ) : ℕ

h G n is the least bound such that every subgraph of G on n vertices can be made bipartite by deleting at most h G n edges.

Equations

• Erdos111.h G n = sSup {k : ℕ | ∃ (H : G.Subgraph), H.verts.Finite ∧ H.verts.ncard = n ∧ Erdos111.bipartizationNumber H = k}

noncomputable def Erdos111.chromaticCardinal {V : Type u} (G : SimpleGraph V) : Cardinal.{u}

The chromatic number of G as a cardinal: the least cardinality of a set of colors that properly colors G.

Equations

• Erdos111.chromaticCardinal G = sInf {κ : Cardinal.{?u.1} | ∃ (α : Type ?u.1), Cardinal.mk α = κ ∧ Nonempty (G.Coloring α)}