I would like to use those same characters, and where applicable with the same sizes and alignments of related characters, everywhere — in my editor, my linters and formatters, my diff tools and version control system UIs, my greybeard CLI text file batch processing incantations, everywhere.
All that really needs is languages that use Unicode characters like ≤, fonts that include all the relevant glyphs, and tools that provide a simple way to enter those characters. But all of these are important, because right now we don’t have simple, standardised ways of doing these things, and so we mostly don’t do them at all.
It’s obviously not a big deal, just a small “quality of life” improvement, but it’s 2024 and I don’t see any good reason why we can’t have nice things. :-)