Zulip Chat Archive

Stream: maths

Topic: Notation for `nhds_within`


view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 05:48):

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.

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 05:50):

@Patrick Massot @Sebastien Gouezel :up:

view this post on Zulip Johan Commelin (Jul 30 2020 at 07:28):

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

view this post on Zulip Johan Commelin (Jul 30 2020 at 07:28):

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

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 07:43):

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

view this post on Zulip Patrick Massot (Jul 30 2020 at 09:13):

I like notations.


Last updated: May 06 2021 at 18:20 UTC