How to distinguish infimum symbol from product symbol

Stream: new members

[Mitchell Lee]

Chapter 8 of Mathematics in Lean says:

Pay attention to the difference between the indexed infimum symbol ⨅ and the big product of types symbol Π. Depending on your font, those can be pretty hard to distinguish.

Can anyone recommend a font that makes them easy to distinguish?

[Eric Wieser]

Julia Mono is one option

[Eric Wieser]

But also, in vscode you can hover over them to find out which is which

[Mitchell Lee]

Thanks!

[Patrick Massot]

JetBrainsMono is another nice choice. But really the main thing is to be aware of the existence of both and the fact they are difficult to distinguish. Because when you see one of them it is really hard to know which it is. It is much easier if you saw both side by side.

[Junyan Xu]

In Lean 4 the latter (Π) is mostly replaced by the forall symbol, probably by mathport.
But it still appears in many docstrings. And Π₀ is still used as a notation for docs#DFinsupp. In total there are 997 appearances in 144 files.

[Junyan Xu]

But ∏ is yet something different (docs#Finset.prod) and still widely used.

[Mario Carneiro]

Note that big Pi is no longer a part of lean 4, although it is still reserved as a non-identifier character. It is added back as a type operator in mathlib