4 ms·
The funny symbol is called sqsubseteq and you can find that out by drawing it here: https://detexify.kirelabs.org/classify.html https://detexify.kirelabs.org/cl
by anfelor 5y ago
The funny symbol is called sqsubseteq and you can find that out by drawing it here: https://detexify.kirelabs.org/classify.html https://detexify.kirelabs.org/classify.html
But I agree that there needs to be a way to type latex Symbols quicker. The Lean Community did this quite well: hovering over a symbol in the docs gives you the correct ascii name.