57.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/57
[ErHa66] Erdős, P. and Hajnal, A., On chromatic number of graphs and set-systems. Acta Math. Acad. Sci. Hungar. (1966), 61-99.
[LiMo20] Liu, Hong and Montgomery, Richard, A solution to Erdős and Hajnal's odd cycle problem. arXiv:2010.15802 (2020).

Imports (1)

theorem Erdos57.erdos_57 sorry line 47 source
depends on sorry what this means
Statement uses: SimpleGraph, Eq, ENat, SimpleGraph.chromaticNumber, Top.top, Not, Summable, Real, Nat, SimpleGraph.oddCycleLengths, HDiv.hDiv, OfNat.ofNat, Membership.mem, Set, SummationFilter.unconditional
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
31 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.