801.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/801
[Er79g] Erdős, Paul, Some old and new problems in various branches of combinatorics. Proceedings of the Tenth Southeastern Conference on Combinatorics, Graph Theory and Computing (Florida Atlantic Univ., Boca Raton, Fla., 1979) (1979), 19-37.
[Al96b] Alon, Noga, Independence numbers of locally sparse graphs and a Ramsey type problem. Random Structures Algorithms (1996), 271-278.

Imports (1)

theorem Erdos801.erdos_801 sorry line 46 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, SimpleGraph, Fin, LE.le, SimpleGraph.indepNum, Real.sqrt, Finset, Finset.card, HMul.hMul, Real.log, Set.ncard, Sym2 and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
25 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.