S∞ = Equiv.Perm ℕ is a Polish topological group (issue #27, commit 2)

Building on the pointwise-convergence topology of PermTopology.lean:

• Equiv.Perm ℕ is a Polish space, as a closed subspace of (ℕ → ℕ) × (ℕ → ℕ) via the pair embedding (NatPerm.isClosedEmbedding_embed).
• Multiplication (σ, τ) ↦ σ * τ and inversion σ ↦ σ⁻¹ are continuous, so Equiv.Perm ℕ is a topological group (IsTopologicalGroup).

Continuity of multiplication factors coordinatewise through NatPerm.continuous_evalComp: (σ * τ) n = σ (τ n) evaluates σ at the continuously varying discrete index τ n. Inversion is immediate: the pair embedding intertwines it with Prod.swap.

instance NatPerm.instPolishSpacePermNat : PolishSpace (Equiv.Perm ℕ)

Equiv.Perm ℕ is Polish: a closed subspace of (ℕ → ℕ) × (ℕ → ℕ).

theorem NatPerm.continuous_mul : Continuous fun (p : Equiv.Perm ℕ × Equiv.Perm ℕ) => p.1 * p.2

Multiplication on Equiv.Perm ℕ is continuous.

theorem NatPerm.continuous_inv : Continuous fun (σ : Equiv.Perm ℕ) => σ⁻¹

Inversion on Equiv.Perm ℕ is continuous: embed intertwines it with Prod.swap.

instance NatPerm.instContinuousMulPermNat : ContinuousMul (Equiv.Perm ℕ)

instance NatPerm.instContinuousInvPermNat : ContinuousInv (Equiv.Perm ℕ)

instance NatPerm.instIsTopologicalGroupPermNat : IsTopologicalGroup (Equiv.Perm ℕ)

Equiv.Perm ℕ with the pointwise topology is a topological group.