362.lean`

2 declarations, 2 contain sorry, 0 declared as axioms

References:

erdosproblems.com/362
[Er65] Erdős, P., Extremal problems in number theory. Proc. Sympos. Pure Math., Vol. VIII (1965), 181-189.
[Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[SaSz65] Sárközi, A. and Szemerédi, E., Über ein Problem von Erdős und Moser. Acta Arith. (1965), 205-208.
[St80] Stanley, Richard P., Weyl groups, the hard Lefschetz theorem, and the Sperner property. SIAM J. Algebraic Discrete Methods (1980), 168-184.
[Ha77] Halász, G., Estimates for the concentration function of combinatorial number theory and probability. Period. Math. Hungar. (1977), 197-211.

Imports (1)

theorem Erdos362.erdos_362 sorry line 57 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Real, Finset, Nat, Finset.Nonempty, LE.le, Finset.card, Finset.filter, Eq, Finset.sum, Finset.powerset, HDiv.hDiv, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos362.erdos_362.variants.fixed_card sorry line 71 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Real, Finset, Nat, Finset.Nonempty, LE.le, Finset.card, Finset.filter, Eq, Finset.sum, Finset.powersetCard, HDiv.hDiv, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.