Adding new theorem names with primes

Stream: mathlib4

[Aaron Hill]

We currently have frontier_Iio', which takes in an explicit Nonempty hypothesis (unlike frontier_Iio). As part of a PR, I need to add similar theorems for things like frontier_Icc and interior_Icc. Should I stick with the existing convention and call name it frontier_Icc', or should I come up with a non-primed name?

[Damiano Testa]

Others may have a different opinion, but a doc-string explaining that the unprimed version does not take the explicit hypothesis would be welcome to find, when scanning through the theorems. So, my suggestion would be to use the ' if that is the convention and add a doc-string.