smoothNumbers_mono

Mathlib.NumberTheory.SmoothNumbers

URI: https://scilib.ai/kg/mathlib#Nat.smoothNumbers_mono

← MathLib Explorer

English

If N ≤ M then N.smoothNumbers is a subset of M.smoothNumbers.

Русский

Если N ≤ M, то N.smoothNumbers ⊆ M.smoothNumbers.

LaTeX

$$$N \le M \Rightarrow N.\mathrm{smoothNumbers} \subseteq M.\mathrm{smoothNumbers}$$$

Lean4

@[gcongr]
theorem smoothNumbers_mono {N M : ℕ} (hNM : N ≤ M) : N.smoothNumbers ⊆ M.smoothNumbers := fun _ hx ↦
  ⟨hx.1, fun p hp => (hx.2 p hp).trans_le hNM⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru