mem_smoothNumbersUpTo — Mathlib

English

For any N,k,n, n ∈ smoothNumbersUpTo(N,k) iff n ≤ N and n ∈ smoothNumbers(k).

Русский

Для любых N,k,n верно: n ∈ smoothNumbersUpTo(N,k) тогда и только тогда, когда n ≤ N и n ∈ smoothNumbers(k).

LaTeX

$$$n \in \mathrm{smoothNumbersUpTo}(N,k) \iff n \le N \land n \in \mathrm{smoothNumbers}(k)$$$

Lean4

theorem mem_smoothNumbersUpTo {N k n : ℕ} : n ∈ smoothNumbersUpTo N k ↔ n ≤ N ∧ n ∈ smoothNumbers k := by
  simp [smoothNumbersUpTo, lt_succ]

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