Skip to content

Erdős problem 75

Start work

Is there a graph of chromatic number ℵ_ 1 with ℵ_ 1 vertices such that for all ε > 0, if n is sufficiently large and H is a subgraph on n vertices, then H contains an independent set of size > n ^ (1 - ε)?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

75.lean

Retained formal statement1 of 1

Is there a graph of chromatic number ℵ_ 1 with ℵ_ 1 vertices such that for all ε > 0, if n is sufficiently large and H is a subgraph on n vertices, then H contains an independent set of size > n ^ (1 - ε)?

FormalConjectures/ErdosProblems/75.leanErdos75.erdos_757 linesExact file
True ↔  ∃ V G,    G.chromaticCardinal = Cardinal.aleph 1 ∧      Cardinal.mk V = Cardinal.aleph 1 ∧        ∀ ε > 0,          ∀ᶠ (n : ℕ) in Filter.atTop,            ∀ (H : G.Subgraph), H.verts.ncard = n → ∃ I, ↑I ⊆ H.verts ∧ G.IsIndepSet ↑I ∧ ↑I.card > ↑n ^ (1 - ε)
OpenStatement only, no proof