Closed StevenClontz closed 6 days ago
Closes #920
Gives a dual alias "focal point" to our "generic point", as well as using "specialized" to reflect "generic" in an alias.
Since "focal point" is not super common in general topology, I think keeping the current main name is appropriate.
I am ok with this. Leaving it to someone else to formally review, so you get a second opinion.
Just saw this. Looks good!
Closes #920
Gives a dual alias "focal point" to our "generic point", as well as using "specialized" to reflect "generic" in an alias.
Since "focal point" is not super common in general topology, I think keeping the current main name is appropriate.