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

The hypothesis of countably_colorable_of_linear_proved is C-linearity (linear_of_bipartizationNumber_le), so the theorem is nonempty_coloring_of_linear. The reduction (tendsto_of_isEmpty_coloring) turns it into the limit for every graph that is not countably colorable, and a graph of chromatic number ℵ₁ is one of them.

theorem Erdos111.countably_colorable_of_linear_proved {V : Type u} (G : SimpleGraph V) (C : ℝ) (hC : ∀ (H : G.Subgraph), H.verts.Finite → ↑(bipartizationNumber H) ≤ C * ↑H.verts.ncard) : Nonempty (G.Coloring ℕ)

A graph in which every finite subgraph on m vertices can be made bipartite by deleting at most C m edges has countable chromatic number.

theorem Erdos111.tendsto_of_not_countably_colorable_proved {V : Type u} (G : SimpleGraph V) (hG : IsEmpty (G.Coloring ℕ)) : Filter.Tendsto (fun (n : ℕ) => ↑(h G n) / ↑n) Filter.atTop Filter.atTop

h G n / n → ∞ for every graph G that is not countably colorable.

theorem Erdos111.erdos_111_proved {V : Type u} (G : SimpleGraph V) (hG : chromaticCardinal G = Cardinal.aleph 1) : Filter.Tendsto (fun (n : ℕ) => ↑(h G n) / ↑n) Filter.atTop Filter.atTop

Erdős Problem 111: h G n / n → ∞ for every graph G of chromatic number ℵ₁.