Erdős problem 1193
Let and let be a non-decreasing function of which is always .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/1193.leanFalse ↔ ∀ (A : Set ℕ) (g : ℕ → ℕ), Monotone g → (∀ (n : ℕ), 0 < g n) → {n | AdditiveCombinatorics.sumRep A n = g n}.lowerDensity = 0SolvedStatement only, no proof
Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:1193 - PLBY Lean proofs
ErdosProblems.Erdos1193
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine