869.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/869
[ErNa88] Erdős, Paul and Nathanson, Melvyn B., Partitions of bases into disjoint unions of bases. J. Number Theory (1988), 1-9.
[Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. (1992), 34-50.
[La26] Larsen, D., Three questions of Erdős–Nathanson on asymptotic bases of order 2. arXiv:2603.03472 (2026).

Imports (1)

theorem Erdos869.erdos_869 sorry line 49 source
depends on sorry what this means
Statement uses: Iff, False, Set, Nat, Disjoint, Set.IsAsymptoticAddBasisOfOrder, OfNat.ofNat, Exists, And, LE.le, Union.union, Membership.mem, Not, SDiff.sdiff, Singleton.singleton
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.