mathlib3

e27e99b9 - docs(undergrad): add pointwise convergence (#15601)

docs(undergrad): add pointwise convergence (#15601) We could link to the definition of the product topology but I think it makes more sense to point out this theorem stating that convergence for the product topology is pointwise convergence.