Initial topology induced by a family of functions

[mkerjean]

Motivation for this change

Enhances initial_topoly.v by constructing the topology induced by a family of functions, instead of a single one.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[mkerjean]

The CI is red, and I do not understand why (is it a Nix error ?). Lemma https://github.com/mkerjean/analysis/blob/47c3e604894453fcad960c298b127a3d813c3aed/theories/topology_theory/initial_topology.v#L362 (https://github.com/mkerjean/analysis/blob/47c3e604894453fcad960c298b127a3d813c3aed/theories/topology_theory/initial_topology.v#L362) is said not to compile while the whole library compiles on my computer. Can someone help me understand what's going on? This is a small PR, and I would prefer not to let it gather dust for too long.