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.

[zstone1]

Note that I have used sup_topology for this sometimes, as in completely_regular_uniformity. I am pretty sure its the construction you want.

Im definitely happy to have "initial for multiple functions at once" be more ergonomic, so glad to see this PR. But mostly wanted to highlight this alternative definition. It might make some proofs factor better using the existing machinery, E.G. like uniform structure for sup topology for free.

[mkerjean]

Note that I have used sup_topology for this sometimes, as in completely_regular_uniformity. I am pretty sure its the construction you want.

Im definitely happy to have "initial for multiple functions at once" be more ergonomic, so glad to see this PR. But mostly wanted to highlight this alternative definition. It might make some proofs factor better using the existing machinery, E.G. like uniform structure for sup topology for free.

Oh yes, I overlooked that, of course, sup + initial is initial_fam. Not sure this PR is necessary then, maybe just a documentation issue. I've also refined one lemma about initial topology (cvg_image has become cvg_initial and cvg_image and continuous_initial have been added to get rid of the hypothesis about the surjectivity of the function). Maybe the PR can be reduced to these lemmas + an indication in the header on how to define the initial topology for a family of functions.