 Free pro-p group

For finite $X$, this is the pro-p completion of the free group on $X$. Every function from $X$ to a pro-p group extends uniquely to a continuous group homomorphism. More generally one can require a basis tending to the identity and impose the universal property for maps with that convergence condition; alternatively the pro-$p$ completion of the abstract free group represents unrestricted maps from an arbitrary set. These infinite-rank conventions should not be conflated when interpreting generator cardinalities.