Notation for ext_chart_at

Stream: maths

[Winston Yin]

Would anyone object to a new notation for docs#ext_chart_at? They are quite a pain to type repetitively when working with manifolds. I propose 𝓔(I, x) to mean ext_chart_at I x, where the script E is entered with \MCE.

[Winston Yin]

PR #17294 shows the effect of the new notation for ext_chart_at.

[Floris van Doorn]

I haven't found ext_chart_at particularly annoying to write myself, so I'm neutral towards this proposal.
If we do this, do we want similar notation for chart_at?

[Winston Yin]

• 𝓔(I, x) is much shorter, allowing formulas involving them to look like their regular mathematical counterparts. For me, it has made reading and thinking about these formulas much quicker.
• I find myself going back and adding parentheses to ext_chart_at I x all the time when I need to append .symm, .source, .target. Writing 𝓔(I, x) would eliminate the need for this decision.
• The notation 𝓝 for nhds seems like a negative improvement (5 keystrokes instead of 4 including shift key) compared to 𝓔 for ext_chart_at (5 instead of 14).

[Winston Yin]

As for chart_at, I guess a natural choice would be 𝓒 (\MCC), but it looks so darn similar to 𝓔.

[Winston Yin]

One alternative proposal would be to use 𝓒(H, x) (script C) for chart_at and e𝓒(I, x) or 𝓒ₑ(I, x) for ext_chart_at (also script C).

[Kevin Buzzard]

If you just want this for files you're writing you can use local notation, this trick (or a local abbreviation) is used several times in mathlib to save typing

[Floris van Doorn]

Not everything is about saving keystrokes. We use 𝓝 in mathlib because it is commonly used notation for neighborhoods.

[Patrick Massot]

Winston, the neighborhood notation does save key, you only need to type \nh to trigger it.

[Winston Yin]

I suppose a local notation is sufficient for my use. Thanks for the comments!