Theorem: mannTheorem (LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean)

State before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
⊢ min 1 (schnirelmannDensity A + schnirelmannDensity B) ≤ schnirelmannDensity (A + B)
Tactic:
sorry
State after:
no goals