Erdős problem 488

Let $A$ be a finite set and $B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}.$ Is it true that, for every $m>n\geq \max(A)$ , $\frac{\lvert B\cap [1,m]\rvert }{m}< 2\frac{\lvert B\cap [1,n]\rvert}{n}?$

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

488.lean

Retained formal statement1 of 1

Let $A$ be a finite set and $B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}.$ Is it true that, for every $m>n\geq \max(A)$ , $\frac{\lvert B\cap [1,m]\rvert }{m}< 2\frac{\lvert B\cap [1,n]\rvert}{n}?$

FormalConjectures/ErdosProblems/488.leanErdos488.erdos_48810 linesExact file

1True ↔2  ∀ (A : Finset ℕ),3    A.Nonempty →4      0 ∉ A →5        1 ∉ A →6          ∀ (n m : ℕ),7            m > n →8              A.max ≤ ↑n →9                ↑{x ∈ Finset.Icc 1 m | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑m <10                  2 * ↑{x ∈ Finset.Icc 1 n | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑n

OpenStatement only, no proof