922.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/922
[ErHa67b] Erdős, P. and Hajnal, András, On chromatic graphs. Mat. Lapok (1967), 1-4.
[Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35.
[Fo70b] Folkman, J. H., An upper bound on the chromatic number of a graph. (1970), 437-457.

Imports (1)

theorem Erdos922.erdos_922 sorry line 51 source
depends on sorry what this means
Statement uses: Iff, True, Nat, Fintype, SimpleGraph, Finset, Exists, And, LE.le, Eq, Set, Sym2, SimpleGraph.edgeSet, SimpleGraph.induce, EmptyCollection.emptyCollection, GE.ge, Real, Finset.card, HDiv.hDiv, HSub.hSub and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.