English
The set of k-rough numbers up to N is the biUnion over primes p with k ≤ p ≤ N of the sets {m ∈ {1,...,N} | p | m}.
Русский
Множество k-шероховатых чисел до N является биобъединением по простым p с k ≤ p ≤ N множеств {m ≤ N | p | m}.
LaTeX
$$$\mathrm{roughNumbersUpTo}(N,k) = \Big( (N+1).primesBelow \ k.primesBelow \Big).biUnion\!\big( \lambda p, \{ m \in \{0,1,\dots, N\} \mid m \neq 0 \land p \mid m \} \big)$$$
Lean4
/-- The set of `k`-rough numbers `≤ N` can be written as the union of the sets of multiples `≤ N`
of primes `k ≤ p ≤ N`. -/
theorem roughNumbersUpTo_eq_biUnion (N k) :
roughNumbersUpTo N k =
((N + 1).primesBelow \ k.primesBelow).biUnion fun p ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m} :=
by
ext m
simp only [roughNumbersUpTo, mem_smoothNumbers_iff_forall_le, not_and, not_forall, not_lt, exists_prop,
Finset.mem_range, Finset.mem_filter, Finset.mem_biUnion, Finset.mem_sdiff, mem_primesBelow,
show ∀ P Q : Prop, P ∧ (P → Q) ↔ P ∧ Q by tauto]
simp_rw [← exists_and_left, ← not_lt]
refine exists_congr fun p ↦ ?_
have H₁ : m ≠ 0 → p ∣ m → m < N + 1 → p < N + 1 := fun h₁ h₂ h₃ ↦ (le_of_dvd (Nat.pos_of_ne_zero h₁) h₂).trans_lt h₃
have H₂ : m ≠ 0 → p ∣ m → ¬m < p := fun h₁ h₂ ↦ not_lt.mpr <| le_of_dvd (Nat.pos_of_ne_zero h₁) h₂
grind
