948.lean`

2 declarations, 2 contain sorry, 0 declared as axioms

References:

erdosproblems.com/948
[Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72.
[ErGa91] Erdős, P. and Galvin, F., Some Ramsey-type theorems. Discrete Math. 87 (1991), 261–269.

Imports (1)

theorem Erdos948.erdos_948 sorry line 51 source
depends on sorry what this means
Statement uses: Iff, False, Exists, Nat, And, LT.lt, OfNat.ofNat, Int, Fin, StrictMono, Set.Infinite, Set.ofPred, Finset, Finset.Nonempty, Ne, Finset.sum
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos948.erdos_948.variants.monochromatic sorry line 63 source
depends on sorry what this means
Statement uses: Iff, False, Exists, Nat, And, LE.le, OfNat.ofNat, Int, Fin, StrictMono, Set.Infinite, Set.ofPred, LT.lt, Finset, Finset.Nonempty, Eq, Finset.sum
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.