roughNumbersUpTo — Mathlib

English

The positive non-k-smooth (i.e., k-rough) numbers up to N form the Finset of numbers n ∈ {0,1,...,N} with n ≠ 0 and n ∉ smoothNumbers(k).

Русский

Положительные не-k-гладкие (которые называются k-шероховатыми) числа до N образуют множество {n ∈ {0,1,...,N} | n ≠ 0 и n ∉ smoothNumbers(k)}.

LaTeX

$$$\mathrm{roughNumbersUpTo}(N,k) = \{ n \in \mathrm{Finset.range}(N+1) \mid n \neq 0 \land n \notin \mathrm{smoothNumbers}(k) \}$$$

Lean4

/-- The positive non-`k`-smooth (so "`k`-rough") numbers up to and including `N` as a `Finset` -/
def roughNumbersUpTo (N k : ℕ) : Finset ℕ :=
  {n ∈ Finset.range (N + 1) | n ≠ 0 ∧ n ∉ smoothNumbers k}

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