Notation for `zero_at_infinity_continuous_map`

Stream: maths

[Jireh Loreaux]

A function f : zero_at_infinity_continuous_map α β is a continuous function f : α → β which satisfies tendsto f (cocompact α) (𝓝 0); such a function is said to vanish at infinity. What should be the notation for such maps? In mathlib, we have C(α, β) for continuous functions and α →ᵇ β for bounded continuous functions (the latter is localized notation). In the literature, continuous functions vanishing at infinity are denoted C₀(α, β) (which @Heather Macbeth seems to prefer), whereas @Yaël Dillies suggested α →C₀ β.

[Yaël Dillies]

I want to change the notation for continuous_map from C(α, β) to α →C β because it is quite literally the only instance of prefix notation for morphisms in mathlib and makes things unreadable when nested.

[Jireh Loreaux]

I can't seem to create a poll, can you do it?

[Yaël Dillies]

I know this is very standard in the literature but such notation has already been abandoned by mathlib eons ago.

[Yaël Dillies]

Can't you? Here is the template.

/poll <name of the poll>
option1
option2

[Jireh Loreaux]

Does it just not preview correctly?

[Yaël Dillies]

Do NOT send anything else with the message, it will screw it up.

[Jireh Loreaux]

/poll Notation for continuous maps vanishing at infinity
α →C₀ β
C₀(α, β)

[Heather Macbeth]

I place a very high premium on notation which matches that used in the literature. I don't think Yaël's suggestion that we "abandoned [such an effort] eons ago" is correct.

[Heather Macbeth]

Yaël Dillies said:

I want to change the notation for continuous_map from C(α, β) to α →C β because it is quite literally the only instance of prefix notation for morphisms in mathlib and makes things unreadable when nested.

It's not the only instance, we also have it in the smooth manifolds library for smooth maps.

[Heather Macbeth]

And, to repeat, this kind of notation is ubiquitous in the literature (I am constantly writing things like "let $f\in C^{k, \alpha}_{-4}(M, \mathbb{R})$")

[Antoine Chambert-Loir]

By “both notation”, I mean that it could be nice to have α →C β and C(α , β).
Since in type theory the type of maps from α to β is denoted by α → β, i'd say the first one is more natural, but there are not enough decorations available for all imaginable spaces of maps.

[Heather Macbeth]

@Antoine Chambert-Loir I think if there are multiple notations, we lack the capability to declare one out of them as the preferred one. So in the places where the system itself selects notation (the "infoview" at screen right and the documentation), we won't control which one gets selected there.

[Floris van Doorn]

You can control which notation is printed with priorities, just like attributes: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20with.20implicit.20arguments.20.3F/near/200917268

[Heather Macbeth]

Then I see no objection to having both notations! (With C₀(α, β) as the default.)