Notation for `nhds_within`

Stream: maths

[Yury G. Kudryashov]

What do you think about (a) introducing a notation for nhds_within? E.g., 𝓝[s] a? (b) using notation instead of def?
Removing def makes all lemmas about inf_principal work without extra dunfold.

[Yury G. Kudryashov]

@Patrick Massot @Sebastien Gouezel :up:

[Johan Commelin]

You mean that you want to abolish the def nhds_within and replace it with notation?

[Johan Commelin]

Does it help if you make nhds_within reducible, or an abbreviation?

[Yury G. Kudryashov]

AFAIR, either simp or rw won't be able to rewrite on lemmas about *_inf_principal in this case.

[Patrick Massot]

I like notations.

[Yury G. Kudryashov]

I think that we should have notation for 𝓝[Ici x] x, 𝓝[Iic x] x, 𝓝[Ioi x] x, 𝓝[Iio x] x, and 𝓝[{x}ᶜ] x. What about 𝓝ᵣ x, 𝓝ₗ x, 𝓝ᵣ' x, 𝓝ₗ' x, and 𝓝' x? My main concern is that we need to type x twice which is bad, e.g., in 𝓝[{(2 * k + 1) * π / 2}ᶜ] ((2 * k + 1) * π / 2).

[Eric Wieser]

Would 𝓝[≥] x, 𝓝[≤] x, 𝓝[>] x, 𝓝[<] x, and 𝓝[ᶜ] x be valid notation?

[Floris van Doorn]

those would be valid notation yeah, but they are pretty confusing to me (note that the inequality is to the left of the x...)

[Yury G. Kudryashov]

#10694

[Anatole Dedecker]

What about 𝓝⋆ instead of 𝓝' ? It has a clearer meaning to me, but maybe that's too annoying to type (note that it's \* not *)

[Yury G. Kudryashov]

So, which notation should we use? I have #10694 with 𝓝ᵣ x, 𝓝ₗ x, 𝓝ᵣ' x, 𝓝ₗ' x, and 𝓝' x but I can switch to some other notation easily.

[Sebastien Gouezel]

I am very happy with your notations. The only reason I haven't reviewed it yet is that the PR text still reads I'll add notation to module docs later today.:-)

[Yury G. Kudryashov]

Done.

[Eric Wieser]

(no objection from me, I only suggested the other notation to see if anyone else preferred it)

[Yury G. Kudryashov]

@Floris van Doorn I don't find @Eric Wieser 's notation confusing: 𝓝[<] x = 𝓝[Iio x] x = 𝓝[{y | y < x}] x agrees with x being on the right of the inequality sign.

[Yury G. Kudryashov]

Let me create a poll (closing 24 h from now).

[Yury G. Kudryashov]

/poll Notation for 𝓝[Ici x] x, 𝓝[Iic x] x, 𝓝[Ioi x] x, 𝓝[Iio x] x, and 𝓝[{x}ᶜ] x
𝓝ᵣ x, 𝓝ₗ x, 𝓝ᵣ' x, 𝓝ₗ' x, and 𝓝' x;
𝓝[≥] x, 𝓝[≤] x, 𝓝[>] x, 𝓝[<] x, and 𝓝[ᶜ] x;
𝓝[≥] x, 𝓝[≤] x, 𝓝[>] x, 𝓝[<] x, and 𝓝[≠] x

[Floris van Doorn]

Oh, my bad. I had it backwards indeed.

[Eric Wieser]

One more option would be to have 𝓝'[r] x as notation for 𝓝'[{y | r y x}] x and then 𝓝'[(≥)] x etc are supported automatically.

[Eric Wieser]

But that's more verbose and unfolds to something less nice.

[Yury G. Kudryashov]

Switched to 𝓝[≥] x, 𝓝[≤] x, 𝓝[>] x, 𝓝[<] x, and 𝓝[≠] x

[Yury G. Kudryashov]

#10694 is ready for review