lattice shortcuts

Stream: general

[Floris van Doorn]

As @Jeremy Avigad pointed out a while ago, it's a bit annoying to type lattice operations. I also noticed this. I made a PR to add a couple more leanprover/vscode-lean#194. After the PR there are 9 ways to input supr and infi and 4 ways to input sup and meet:
for supr: bigjoin, biglub, bigsqcup, bigsup, Sup, Join, Lub, Sqcup and supr
for sup: sup, join, lub and sqcup
dually for inf and infi

You now have to type inftyfor ∞, supseteq for ⊇ and bowtie (unused) for ⋈.

[Floris van Doorn]

I also changed \nin to mean \notin, that one got me a couple of times. There are some other changes, like \inter for \cap. Feel free to suggest others (and if people want, I'll also make this PR to Emacs mode).

[Floris van Doorn]

Currently \d and \i are for ↓ and ∩. I would slightly prefer δ and ι. Opinions?

[Alex J. Best]

I'd agree but not strongly enough that I'd want to change if anyone was really unhappy.
For reference, δ is used 1200 times and ↓ only 20.
ι is 3000 times and ∩ 1000.
So \d seems like a no brainer, \i is closer and I'd imagine a lot of people are used to using \cap anyway for ∩.
While we're at it what about \t for τ . (and then ▸ could take \tr and \tri etc.). Its a bit more controversial I'm sure as ▸ is used 1405 times in mathlib and τ only 190, but it would start to make it more consistent: for a greek letter type \ and the first letter of its latin name.

[Edward Ayers]

I have a take on this:

        "tr": "◂", "tl" : "▸",                           "tu" : "▾", "td" : "▴",
        "lr": "<", "ll" : ">", "lre" : "≤", "lle" : "≥", "lu" : "∨", "ld" : "∧", "luu": "⋁", "ldd": "⋀",
        "sr": "⊏", "sl" : "⊐", "sre" : "⊑", "sle" : "⊒", "su" : "⊔", "sd" : "⊓", "suu": "⨆", "sdd": "⨅",
        "cr": "⊂", "cl" : "⊃", "cre" : "⊆", "cle" : "⊇", "cu" : "∪", "cd" : "∩", "cuu": "⋃", "cdd": "⋂",
        "ir": "⊲", "il" : "⊳", "ire" : "⊴", "ile" : "⊵", "iu" : "∇", "id" : "∆",
        "vr": "≺", "vl" : "≻", "vre" : "≼", "vle" : "≽", "vu" : "⋎", "vd" : "⋏",

[Alex J. Best]

Wow, I think your left/rightness of triangles convention is the opposite of tex's though!

[Edward Ayers]

Ah man I've been reading triangles wrong my whole life!

[Mario Carneiro]

how does this convention interact with \l for lambda vs left arrow?

[Johan Commelin]

left arrow should of course be \al, and then there will also be \ar and \ad and \au.

[Johan Commelin]

I think \lam and \lef both occur often enough that we can switch \l to lambda. Reprogramming the muscle memory will only take 37 days.

[Jeremy Avigad]

When this settles, I'll update the text of MiL to include the new lattice shortcuts.

[Edward Ayers]

Mario Carneiro said:

how does this convention interact with \l for lambda vs left arrow?

        "-r"  : "→", "-l"  : "←", "-u"  : "↑", "-d"  : "↓", "-lr" : "↔", "-ud": "↕", "-rr" : "⟶", "-ll" : "⟵",
        "mtr" : "↦", "mtl" : "↤", "mtu" : "↥", "mtd" : "↧",
        "epl" : "↞", "epr" : "↠", "epu" : "↟", "epd" : "↡",
        "hpl" : "↩", "hpr" : "↪",              "hpd" : "↷",
        "ltr" : "↝", "ltl" : "↜",
        "mol" : "↢", "mor" : "↣",
        "=l" : "⇐", "=u"  : "⇑", "=r" :  "⇒", "=d" :  "⇓", "=lr" : "⇔", "=ud" : "⇕",
        "=ul" : "⇖", "=ur" : "⇗", "=dr" : "⇘", "=dl" : "⇙",
        "fl" : "⥢", "fr": "⥤", "fu": "⥣", "fd": "⥥",
        "hlu" : "↼", "hru": "⇀", "hur" : "↾", "hdr" : "⇂", "hld" : "↽", "hul" : "↿",  "hrd" : "⇁",  "hdl" : "⇃",
        "zr" : "⇝", "zl" : "⇜", "zlr" : "↭", "zd" : "↯", "zrr" : "⟿",

[Edward Ayers]

        "al": "α", "be": "β", "ga": "γ", "de": "δ", "ep": "ε", "ze": "ζ",
        "et": "η", "th": "θ", "io": "ι", "ka": "κ", "la": "λ", "mu": "μ",
        "nu": "ν", "xi": "ξ", "pi": "π", "rh": "ρ", "si": "σ",
        "ta": "τ", "ph": "φ", "ch": "χ", "ps": "ψ", "om": "ω",