[Merged by Bors] - refactor(*): add a notation for nhds_within

[urkud]

The definition is still there and can be used too.

---

[sgouezel]

I'm fine with the notation, but I think I'd rather keep the definition: one shouldn't need to know what principal means to be able to use neighborhood_within, and the definition hides it away.

[PatrickMassot]

I'm fine with the notation, but I think I'd rather keep the definition: one shouldn't need to know what principal means to be able to use neighborhood_within, and the definition hides it away.

What I've seen in this PR doesn't suggest that it requires to know more about the definition. And I really like the new notation (but I think everybody agrees here). I'd merge this.

[urkud]

I'm fine with the notation, but I think I'd rather keep the definition: one shouldn't need to know what principal means to be able to use neighborhood_within, and the definition hides it away.

What I've seen in this PR doesn't suggest that it requires to know more about the definition. And I really like the new notation (but I think everybody agrees here). I'd merge this.

You need to know that this is a notation, not a definition in order to understand why simp [← nhds_within_univ] fails. I can revert parts of the PR that remove the definition.

[sgouezel]

Since Patrick likes it the way it is, I can live with it. So, Yury, do as you think is best, and then you can merge it.
bors d+

[bors]

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[PatrickMassot]

I really don't have a strong opinion here, but I haven't seen anything shocking in the new proofs, and I also trust Yury.

[urkud]

and I also trust Yury.

I think that notation + def vs notation matters mostly for new users, and you shouldn't trust me here. I definitely can live with any of these options. Here is the differences I spotted while porting the code:

• with notation + def if users want to rw/simp using a lemma expecting f ⊓ 𝓟 s, then they need to simp/dsimp/dunfold/rw nhds_within first.
• with notation (no def) users can't do simp [← nhds_within_univ] anymore and sometimes they can be surprised by simp/rw rewriting nhds part of nhds_within notation.

TL;DR: I agree with @sgouezel that notation + def has less surprising behavior and unfolding nhds_within when we want it is not hard, so I should revert part of my PR.

[urkud]

I had a green light with the previous version and built the new version (some changes reverted) locally, so
bors merge

[urkud]

bors r-

[bors]

Canceled.

[urkud]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests