mem_smoothNumbers_of_lt — Mathlib

English

Every m with 0 < m < n is in n.smoothNumbers.

Русский

Каждое m, удовлетворяющее 0 < m < n, лежит в n.smoothNumbers.

LaTeX

$$$0 < m \wedge m < n \Rightarrow m \in n.\mathrm{smoothNumbers}$$$

Lean4

/-- All `m`, `0 < m < n` are `n`-smooth numbers -/
theorem mem_smoothNumbers_of_lt {m n : ℕ} (hm : 0 < m) (hmn : m < n) : m ∈ n.smoothNumbers :=
  smoothNumbers_eq_factoredNumbers _ ▸
    ⟨ne_zero_of_lt hm, fun _ h => Finset.mem_range.mpr <| lt_of_le_of_lt (le_of_mem_primeFactorsList h) hmn⟩

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