pi-base
use coherent terminology
Inspired by recent discussions in mathlib, e.g. https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2318397.20rename.20RestrictGenTopology.20to.20IsRestrictGen
There are several inequivalent notions of "generated" in the literature: generated by maps, generated by subspaces, generated by a subbasis... However, I believe "coherent" is a pretty unambiguous term to describe spaces whose topoogy is determined by a family of subspaces. This PR introduces the term in pi-Base.
Closes #1265 (including addressing @prabau's feedback there).
Background: The terminology of a topology "coherent with a family of subsets" appears in Willard, problem 9M, which is the reference used in Wikipedia. But it does not appear anywhere in Encyclopedia of General Topology (Hart, Nagata, Vaughan eds.) for example. They do mention the terminology "determined by ..." on page 44. I also check google scholar and "coherent" does not seem to be used much in the sense above. It does appear as "coherent" by itself with the different meaning of spectral space (P75), where we already have it as an alias.
So bottom line: It seems a useful summary to describe some of the properties as the topology being coherent with a certain collection of subspaces/subsets. This can certainly be added to the description itself, with a reference to Coherent in wikipedia. But it does not seem useful to add it as an alias in some of the cases, especially when there is another common terminology and practically nobody uses the coherent terminology for the name of the property.
For example, for P90 (Alexandrov): "Coherent with finite subspaces" is not useful as an alias, as people looking for that property will not search it by that name. But we can add it at the end of the third bullet, maybe something like "... That is, the topology on $X$ is coherent with the collection of finite subspaces."
Same thing with P81, etc.
For the "k"-properties and variants, it's less clear to me. I don't know if anybody used "coherent ..." as the name of the property, but it could be useful to have it due to the ambiguities of all these related properties.
Thoughts?
FYI: https://math.stackexchange.com/questions/1047888/are-countably-compactly-generated-spaces-paracompact
Interesting terminology: "countably compactly generated" for $k_\omega$-space. I have no idea and did not take the time to look if that's even in use or just made up by that user. But it's not bad, although still ambiguous.
@StevenClontz I have merged #1265, as it was more self-contained and not controversial. As for introducing "coherent" terminology, one could mention it in the description of properties, but adding it as an alias is not clear that it would be the right thing to do. See reasons in my comments above. It seems that @ccaruvana also has some reservations.