open_nbhs -> mem_open

[affeldt-aist]

Motivation for this change

fixes #1969

fixes #2050

fyi: @CohenCyril @andrew-appel

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]

Is this sentence accurate ? What does it mean ?

[affeldt-aist]

Arg, that's a typo: it should be "now uses" :-)

[mkerjean]

I agree that the name change is welcomed. As long as the CI is green, it can be merged in my opinion (maybe once my comment about the changelog is clarified).

[CohenCyril]

From @mkerjean at #1969 (comment)

[open_nbhs_nbhs ] has a circular flavor : one can think that open_nbhs is the conjunction of open and nbhs and that the lemma looks circular.

open_nbhs is the conjunction of open and nbhs (as shown by open_nbhsE), just not definitionally as of now because there is a "simpler" definition. I'm wary of renaming it to mem_open knowing that it actually is more than that.

Something one could do instead is swap the definitional and propositional equality, i.e., have the statement
open_nbhs p = [set A in nbhs p | open A] be definitional and open_nbhs p A = open A /\ A p be propositional.
Because that's really the open neighborhoods of a point.

[CohenCyril]

I would keep the name but change the definition, and write a lemma stating

Lemma open_nbhs_mem (p : T) (A : set T) : open_nbhs p A = open A /\ A p.

[CohenCyril]

Suggested change

	Definition mem_open (p : T) (A : set T) := open A /\ A p.
	Definition open_nbhs (p : T) := open `&` nbhs p