primeFactors_subset_of_mem_factoredNumbers

English

If m ∈ factoredNumbers(s), then m.primeFactors ⊆ s.

Русский

Если m ∈ factoredNumbers(s), то m.primeFactors ⊆ s.

LaTeX

$$m.primeFactors ⊆ s$$

Lean4

/-- The `Finset` of prime factors of an `s`-factored number is contained in `s`. -/
theorem primeFactors_subset_of_mem_factoredNumbers {s : Finset ℕ} {m : ℕ} (hm : m ∈ factoredNumbers s) :
    m.primeFactors ⊆ s := by
  rw [mem_factoredNumbers] at hm
  exact fun n hn ↦ hm.2 n (mem_primeFactors_iff_mem_primeFactorsList.mp hn)

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