Symmetric difference notation

Stream: general

[Yaël Dillies]

The current notation for docs#symm_diff is Δ. This conflicts with the use of Δ as a variable in docs#simplex_category.eq_comp_δ_of_not_surjective'.

What should we do? Change the notation to another unicode triangle? Localize it?

[Yaël Dillies]

This conflict is preventing me from slightly tweaking the imports in #6476.

[Reid Barton]

Certainly letters shouldn't be notation

[Reid Barton]

At least not notation for operators, that's just weird

[Reid Barton]

($\omega$ as localized notation for omega seems ok for instance)

[Reid Barton]

https://unicode-explorer.com/c/2206 suggests that it but perhaps also other unicode characters could be used for symmetric difference

[Reid Barton]

(and that it might also be used for more interesting things)

[Bryan Gin-ge Chen]

As the one who introduced the notation, I'm perfectly fine with it being changed or localized.

(Actually, I think I copied it from this snippet but I'm happy to take the blame!)

[Kyle Miller]

I think it's common to find a stylized capital delta in the literature - i.e., a triangle. Options:

• ∆ is INCREMENT in the mathematical operators block
• △ is WHITE UP-POINTING TRIANGLE in the geometric shapes block

I found one place that suggested to use the first symbol for symmetric difference. Whatever the choice, localizing the notation seems like a good idea.

[Yaël Dillies]

△ looks rather horrendous to me, so what about using ∆? Also, do we want to localize or rather leave a comment saying "localize as soon as you need the notation for something else"?

[Yaël Dillies]

I don't know how far we are from having Laplace.

[Kyle Miller]

Maybe prefix vs infix is enough to disambiguate them anyway.

[Eric Wieser]

In the short term, you can use \fr<<>> to escape the identifier in the downstream lemma

[Yaël Dillies]

\f<<>> is enough btw

[Eric Wieser]

I probably meant to say that,

[Yaël Dillies]

#13217