English
The pair of maps F(n) = support of factorization of n and G(S) = ∏ p ∈ S p realizes a inverse relationship between squarefree naturals and finite sets of primes.
Русский
Пара отображений F(n) = опорa разложения n по простым и G(S) = ∏ p в S p образуют взаимно обратную связь между квадратно свободными натуральными числами и конечными множествами простых чисел.
LaTeX
$$$F(n) := (\\\\text{factorization}(n)).\\\\text{support}, \\\\ G(S) := \\\\prod_{p \\\\in S} p, \\\\text{then } F(n) \\\\text{and } G(S) \hspace{1pt} \text{form an inverse correspondence between } \\\\{n \\\\mid \\\\operatorname{Squarefree}(n)\\\\} \\\\text{and } \\\\{S \\\\mid \\\\forall p \\\\in S, p.\\\\Prime\\\\}.$$$
Lean4
theorem prod_primeFactors_invOn_squarefree :
Set.InvOn (fun n : ℕ ↦ (factorization n).support) (fun s ↦ ∏ p ∈ s, p) {s | ∀ p ∈ s, p.Prime} {n | Squarefree n} :=
⟨fun _s ↦ primeFactors_prod, fun _n ↦ prod_primeFactors_of_squarefree⟩
