False ↔ ∀ (ε : ℝ), 0 < ε → ∀ (C : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (∀ (d : ℕ), {v | (G.neighborSet v).ncard = d}.ncard ≤ 2) → (1 / 2 + ε) * ↑n < ↑(Set.range fun v => (G.neighborSet v).ncard).ncard → ∃ s, Erdos1037.IsTrivialSet G s ∧ C * Real.log ↑n < ↑s.ncard