Erdős problem 1036
Let be a graph on vertices which does not contain a trivial (empty or complete) graph on more than vertices. Must contain at least many induced subgraphs which are not pairwise isomorphic?
Sources
FormalConjectures/ErdosProblems/
1036.lean
Retained formal statement
Erdős and Hajnal [ErHa89b] proved that if does not contain a complete bipartite graph or its complement on more than vertices then contains at least many non-isomorphic induced subgraphs.
∀ (c : ℝ), 0 < c → ∃ δ, 0 < δ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), Erdos1036.NoLargeInducedBipartite G (c * Real.log ↑n) → Erdos1036.HasManyNonIsomorphicInducedSubgraphs G (2 ^ (δ * ↑n))SolvedStatement only, no proof