smoothNumbersUpTo — Mathlib

English

For natural numbers N and k, smoothNumbersUpTo(N,k) is the Finset of all n with 0 ≤ n ≤ N and n ∈ smoothNumbers(k).

Русский

Для натуральных чисел N и k множество smoothNumbersUpTo(N,k) состоит из всех n, таких что 0 ≤ n ≤ N и n ∈ smoothNumbers(k).

LaTeX

$$$\mathrm{smoothNumbersUpTo}(N,k) = \{ n \in \mathrm{Finset.range}(N+1) \mid n \in \mathrm{smoothNumbers}(k) \}$$$

Lean4

/-- The `k`-smooth numbers up to and including `N` as a `Finset` -/
def smoothNumbersUpTo (N k : ℕ) : Finset ℕ :=
  {n ∈ Finset.range (N + 1) | n ∈ smoothNumbers k}

Похожие утверждения