factoredNumbers_mono

Mathlib.NumberTheory.SmoothNumbers

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

← MathLib Explorer

English

If s ≤ t, then factoredNumbers(s) ⊆ factoredNumbers(t).

Русский

Если s ⊆ t, то factoredNumbers(s) ⊆ factoredNumbers(t).

LaTeX

$$factoredNumbers(s) ⊆ factoredNumbers(t) (when s ≤ t)$$

Lean4

@[gcongr]
theorem factoredNumbers_mono {s t : Finset ℕ} (hst : s ≤ t) : factoredNumbers s ⊆ factoredNumbers t := fun _ hx ↦
  ⟨hx.1, fun p hp ↦ hst <| hx.2 p hp⟩

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

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

Разделы

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

Аффилиация

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