English
m ∈ factoredNumbers s iff every prime divisor of m lies in s.
Русский
m ∈ factoredNumbers s тогда и только тогда, когда все простые делители m принадлежат s.
LaTeX
$$m ∈ \mathrm{factoredNumbers}(s) \iff ∀ p, p.Prime \rightarrow p ∣ m \rightarrow p ∈ s$$
Lean4
/-- `m` is `s`-factored if and only if all prime divisors of `m` are in `s`. -/
theorem mem_factoredNumbers' {s : Finset ℕ} {m : ℕ} : m ∈ factoredNumbers s ↔ ∀ p, p.Prime → p ∣ m → p ∈ s :=
by
obtain ⟨p, hp₁, hp₂⟩ := exists_infinite_primes (1 + Finset.sup s id)
rw [mem_factoredNumbers_iff_forall_le]
refine
⟨fun ⟨H₀, H₁⟩ ↦ fun p hp₁ hp₂ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero H₀) hp₂) hp₁ hp₂, fun H ↦
⟨fun h ↦ lt_irrefl p ?_, fun p _ ↦ H p⟩⟩
calc
p ≤ s.sup id := Finset.le_sup (f := @id ℕ) <| H p hp₂ <| h.symm ▸ dvd_zero p
_ < 1 + s.sup id := (lt_one_add _)
_ ≤ p := hp₁
