naming in docs#SubsetProperties

Stream: mathlib4

[Michael Rothgang]

Reading over that file, I was wondering about the naming scheme --- why results are namespaced or not.

Should docs#isCompact_of_isClosed_subset be named IsCompact.of_isClosed_subset instead?
This would match docs#IsCompact.image, docs#IsCompact.image_of_continuousOn and docs#IsCompact.diff --- which are mathematically similar and appear right next to it in the file.

[Michael Rothgang]

(Sorry, still figuring out which syntax to use for the linkifier. Bear with me.)

[Eric Wieser]

(docs#id links don't start with #)

[Michael Rothgang]

Same question for docs#isCompact_of_finite_subcover and docs#isCompact_of_finite_subfamily_closed.

Happy to make a PR if desired.

[Eric Wieser]

Thoe links seem not to work; I think you meant to drop the SubsetProperties bit?

[Jireh Loreaux]

Yes, docs#isCompact_of_isClosed_subset should probably be renamed to IsCompact.of_isClosed_subset which will activate dot notation. The other two you mentioned are okay the way they are because they don't have an IsCompact hypothesis.

[Michael Rothgang]

Submitted a PR for IsCompact.of_isClosed_subset at #7298.

[Michael Rothgang]

Thanks for clarifying the difference between these naming schemes. Is this (namespace if mentioned in hypotheses) a general convention?

[Yaël Dillies]

Yes, so long as it's not too ridiculous for unrelated reasons.

[Jireh Loreaux]

@Michael Rothgang do you understand why we do it in general? It's because of dot notation. That is, if you have a declaration Foo.bar (x : Foo) : ... := sorry, and then later you have x : Foo, you can write x.bar instead of Foo.bar x.

[Michael Rothgang]

@Jireh Loreaux Yes, I do. (I was mostly thinking about different reasons, though. I'll keep in mind that dot notation is the main one.)

[Jireh Loreaux]

"the main one" one might be slightly too strong, but certainly "an important one" is accurate. When responding to the questions you posed above, the primary things I considered were: dot notation, is it okay for this to be in the root namespace or is it to specialized?, and does it otherwise follow the naming conventions given in #naming ? Another question is: will it cause naming conflicts if it's in the root namespace (also relevant for determining whether a namespaced declaration should be protected)?