921.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/921
[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.
[Ga63] Gallai, T., Kritische Graphen. I. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1963), 165-192.
[KST84] Kierstead, H. A., Szemerédi, E. and Trotter, W. T., On coloring graphs with locally small chromatic number. Combinatorica (1984), 183-185.

Imports (1)

theorem Erdos921.erdos_921 sorry line 55 source
depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Exists, Real, And, LT.lt, Filter.Eventually, SimpleGraph, Fin, Eq, ENat, SimpleGraph.chromaticNumber, Membership.mem, Set, SimpleGraph.oddCycleLengths, HMul.hMul, HPow.hPow and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
50 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.