quartztz::lean-symb

Lean 4 symbol reference

Statically (for now) generated from lean4-vscode's abbreviations.json file. Please let me know if anything changes!
Click on a symbol to see more details.
The symbol represents where the cursor will be placed for bracket-like abbreviations.
α\a
β\b
γ\g
δ\de
ε\e
ζ\ze
η\et
θ\th
ι\io
κ\ka
λ\la
μ\m
ν\nu
ξ\xi
ο\omicron
π\pi
ρ\rh
σ\si
ς\vsi
τ\ta
υ\upsilon
φ\ph
χ\c
ψ\ps
ω\om
Α\Alpha
Β\Beta
Γ\Gamma
Δ\Delta
Ε\Epsilon
Ζ\Zeta
Η\Eta
Θ\Theta
Ι\Iota
Κ\GK
Λ\L
Μ\GM
Ν\GN
Ξ\GX
Ο\Omicron
Π\p
Π₀\Pi0
Ρ\GR
Σ\S
Τ\Tau
Υ\Upsilon
Φ\GF
Χ\GC
Ψ\GP
Ω\ohm
Ͱ\Heta
ͱ\heta
Ϳ\Yot
ϐ\varbeta
ϑ\vartheta
ϕ\varphi
ϖ\varpi
ϗ\varkai
Ϛ\Stigma
ϛ\stigma
Ϝ\Digamma
ϝ\digamma
Ϟ\Koppa
ϟ\koppa
Ϡ\Sampi
ϡ\sampi
Ϣ\Shei
ϣ\shei
Ϥ\Fei
ϥ\fei
Ϧ\Khei
ϧ\khei
Ϩ\Hori
ϩ\hori
Ϫ\Gangia
ϫ\gangia
Ϭ\Shima
ϭ\shima
Ϯ\Dei
ϯ\dei
ϰ\varkappa
ϱ\varrho
Ϸ\Sho
ϸ\sho
Ϻ\San
ϻ\san
À\`A
Á\'A
Â\^{A}
Ã\~A
Ä\"A
Å\angstrom
Æ\AE
Ç\cC
È\`E
É\'E
Ê\^{E}
Ë\"E
Ì\`I
Í\'I
Î\^{I}
Ï\"I
Ð\DH
Ñ\~N
Ò\`O
Ó\'O
Ô\^{O}
Õ\~O
Ö\"O
Ù\`U
Ú\'U
Û\^{U}
Ü\"U
Ý\'Y
Þ\TH
à\`a
á\'a
â\^{a}
ã\~a
ä\"a
å\aa
æ\ae
ç\cc
è\`e
é\'e
ê\^{e}
ë\"e
ì\`i
í\'i
î\^{i}
ï\"i
ð\dh
ñ\~{n}
ò\`o
ó\'o
ô\^{o}
õ\~o
ö\"o
ø\/o
ù\`u
ú\'u
û\^{u}
ü\"u
ý\'y
ÿ\"y
Ā\-{A}
ā\-{a}
Č\vC
č\vc
Ď\vD
ď\vd
Ē\-{E}
ē\-{e}
Ě\vE
ě\ve
Ī\-{I}
ī\-{i}
Į\kI
į\ki
ı\imath
Ł\/L
Ō\-{O}
ō\-{o}
Œ\OE
œ\oe
Ū\-{U}
ū\-{u}
ƛ\Gl-
ȩ\ce
\_(
\_)
\_+
\_-
̲\_--
\_=
\_a
\_e
\_h
\_i
\_j
\_k
\_l
\_m
\_n
\_o
\_p
\_r
\_s
\_t
\_u
\_v
\_x
⁻¹\-
⁻²\-2
⁻³\-3
⁻¹'\preim
ᵃᵒᵖ\addopposite
ᵐᵒᵖ\mulopposite
ᵒᵈ\od
ᵒᵖ\opposite
\^(
\^)
\^+
\^-
\^0
¹\^1
²\^2
³\^3
\^4
\^5
\^6
\^7
\^8
\^9
\^=
\^A
\^B
\^D
\^E
\^G
\^H
\^I
\^J
\^K
\^L
\^M
\^N
\^O
\^P
ᴿ\^R
\^T
\^U
\^V
\^W
\^a
\^b
\^d
\^e
\^f
\^g
ʰ\^h
\^i
ʲ\^j
\^k
ˡ\^l
\^m
\^n
\^o
\^p
ʳ\^r
ˢ\^s
\^t
\^u
\^v
ʷ\^w
ˣ\^x
ʸ\^y
\^z
\^SM
\^TM
ʱ\^hhook
ʴ\^turnedr
ʵ\^turnedrhook
ʶ\^Rinverted
ˠ\^gamma
ˤ\^stop
\^Ae
\^Bbarred
\^Ereversed
\^Nreversed
\^Ou
\^turneda
\^alpha
\^turnedae
\^schwa
\^eopen
\^turnede
\^turnedi
\^eng
\^oopen
\^otop
\^obottom
\^usideways
\^turnedm
\^ain
\^beta
\^vargamma
\^varphi
\^chi
\^turnedalpha
\^ccurl
\^eth
\^ereversedopen
\^gscript
\^turnedh
\^istroke
\^iota
\^Ismall
\^Istroke
\^jtail
\^lretroflexhook
\^lhook
\^Lsmall
\^mhook
\^turnedmleg
\^nlefthook
\^nretroflexhook
\^Nsmall
\^obarred
\^phi
\^shook
\^esh
\^twithpalatalhook
\^ubar
\^upsilon
\^Usmall
\^vhook
\^turnedv
\^zretroflexhook
\^zcurl
\^ezh
ᶿ\^theta
\0
\1
\2
\3
\4
\5
\6
\7
\8
\9
\^heng
\^ls
\^ltilde
\^uhook
𝐀\bfA
𝐁\bfB
𝐂\bfC
𝐃\bfD
𝐄\bfE
𝐅\bfF
𝐆\bfG
𝐇\bfH
𝐈\bfI
𝐉\bfJ
𝐊\bfK
𝐋\bfL
𝐌\bfM
𝐍\bfN
𝐎\bfO
𝐏\bfP
𝐐\bfQ
𝐑\bfR
𝐒\bfS
𝐓\bfT
𝐔\bfU
𝐕\bfV
𝐖\bfW
𝐗\bfX
𝐘\bfY
𝐙\bfZ
𝐚\bfa
𝐛\bfb
𝐜\bfc
𝐝\bfd
𝐞\bfe
𝐟\bff
𝐠\bfg
𝐡\bfh
𝐢\bfi
𝐣\bfj
𝐤\bfk
𝐥\bfl
𝐦\bfm
𝐧\bfn
𝐨\bfo
𝐩\bfp
𝐪\bfq
𝐫\bfr
𝐬\bfs
𝐭\bft
𝐮\bfu
𝐯\bfv
𝐰\bfw
𝐱\bfx
𝐲\bfy
𝐳\bfz
𝐴\MiA
𝐵\MiB
𝐶\MiC
𝐷\MiD
𝐸\MiE
𝐹\MiF
𝐺\MiG
𝐻\MiH
𝐼\MiI
𝐽\MiJ
𝐾\MiK
𝐿\MiL
𝑀\MiM
𝑁\MiN
𝑂\MiO
𝑃\MiP
𝑄\MiQ
𝑅\MiR
𝑆\MiS
𝑇\MiT
𝑈\MiU
𝑉\MiV
𝑊\MiW
𝑋\MiX
𝑌\MiY
𝑍\MiZ
𝑎\Mia
𝑏\Mib
𝑐\Mic
𝑑\Mid
𝑒\Mie
𝑓\Mif
𝑔\Mig
𝑖\Mii
𝑗\Mij
𝑘\Mik
𝑙\Mil
𝑚\Mim
𝑛\Min
𝑜\Mio
𝑝\Mip
𝑞\Miq
𝑟\Mir
𝑠\Mis
𝑡\Mit
𝑢\Miu
𝑣\Miv
𝑤\Miw
𝑥\Mix
𝑦\Miy
𝑧\Miz
𝑨\MIA
𝑩\MIB
𝑪\MIC
𝑫\MID
𝑬\MIE
𝑭\MIF
𝑮\MIG
𝑯\MIH
𝑰\MII
𝑱\MIJ
𝑲\MIK
𝑳\MIL
𝑴\MIM
𝑵\MIN
𝑶\MIO
𝑷\MIP
𝑸\MIQ
𝑹\MIR
𝑺\MIS
𝑻\MIT
𝑼\MIU
𝑽\MIV
𝑾\MIW
𝑿\MIX
𝒀\MIY
𝒁\MIZ
𝒂\MIa
𝒃\MIb
𝒄\MIc
𝒅\MId
𝒆\MIe
𝒇\MIf
𝒈\MIg
𝒉\MIh
𝒊\MIi
𝒋\MIj
𝒌\MIk
𝒍\MIl
𝒎\MIm
𝒏\MIn
𝒐\MIo
𝒑\MIp
𝒒\MIq
𝒓\MIr
𝒔\MIs
𝒕\MIt
𝒖\MIu
𝒗\MIv
𝒘\MIw
𝒙\MIx
𝒚\MIy
𝒛\MIz
𝒜\McA
\McB
𝒞\McC
𝒟\McD
\McE
\McF
𝒢\McG
\McH
𝒥\McJ
𝒦\McK
\McL
\McM
𝒩\McN
𝒪\McO
𝒬\McQ
\McR
𝒮\McS
𝒯\McT
𝒰\McU
𝒱\McV
𝒲\McW
𝒳\McX
𝒴\McY
𝒵\McZ
𝒶\Mca
𝒷\Mcb
𝒸\Mcc
𝒹\Mcd
\Mce
𝒻\Mcf
\Mcg
𝒽\Mch
𝒾\Mci
𝒿\Mcj
𝓀\Mck
𝓁\Mcl
𝓂\Mcm
𝓃\Mcn
\Mco
𝓅\Mcp
𝓆\Mcq
𝓇\Mcr
𝓈\Mcs
𝓉\Mct
𝓊\Mcu
𝓋\Mcv
𝓌\Mcw
𝓍\Mcx
𝓎\Mcy
𝓏\Mcz
𝓐\MCA
𝓑\MCB
𝓒\MCC
𝓓\MCD
𝓔\MCE
𝓕\MCF
𝓖\MCG
𝓗\MCH
𝓘\MCI
𝓙\MCJ
𝓚\MCK
𝓛\MCL
𝓜\MCM
𝓝\MCN
𝓞\MCO
𝓟\MCP
𝓠\MCQ
𝓡\MCR
𝓢\MCS
𝓣\MCT
𝓤\MCU
𝓥\MCV
𝓦\MCW
𝓧\MCX
𝓨\MCY
𝓩\MCZ
𝓪\MCa
𝓫\MCb
𝓬\MCc
𝓭\MCd
𝓮\MCe
𝓯\MCf
𝓰\MCg
𝓱\MCh
𝓲\MCi
𝓳\MCj
𝓴\MCk
𝓵\MCl
𝓶\MCm
𝓷\MCn
𝓸\MCo
𝓹\MCp
𝓺\MCq
𝓻\MCr
𝓼\MCs
𝓽\MCt
𝓾\MCu
𝓿\MCv
𝔀\MCw
𝔁\MCx
𝔂\MCy
𝔃\MCz
𝔄\MfA
𝔅\MfB
\MfC
𝔇\MfD
𝔈\MfE
𝔉\MfF
𝔊\MfG
\MfH
𝔍\MfJ
𝔎\MfK
𝔏\MfL
𝔐\MfM
𝔑\MfN
𝔒\MfO
𝔓\MfP
𝔔\MfQ
𝔖\MfS
𝔗\MfT
𝔘\MfU
𝔙\MfV
𝔚\MfW
𝔛\MfX
𝔜\MfY
\MfZ
𝔞\Mfa
𝔟\Mfb
𝔠\Mfc
𝔡\Mfd
𝔢\Mfe
𝔣\Mff
𝔤\Mfg
𝔥\Mfh
𝔦\Mfi
𝔧\Mfj
𝔨\Mfk
𝔩\Mfl
𝔪\Mfm
𝔫\Mfn
𝔬\Mfo
𝔭\Mfp
𝔮\Mfq
𝔯\Mfr
𝔰\Mfs
𝔱\Mft
𝔲\Mfu
𝔳\Mfv
𝔴\Mfw
𝔵\Mfx
𝔶\Mfy
𝔷\Mfz
𝔻\bbD
𝔼\bbE
𝔾\bbG
𝕀\bbI
𝕁\bbJ
𝕃\bbL
𝕄\bbM
𝕆\bbO
𝕊\bbS
𝕋\bbT
𝕌\bbU
𝕍\bbV
𝕎\bbW
𝕏\bbX
𝕐\bbY
𝕒\bba
𝕓\bbb
𝕔\bbc
𝕕\bbd
𝕖\bbe
𝕗\bbf
𝕘\bbg
𝕙\bbh
𝕚\bbi
𝕛\bbj
𝕜\bbk
𝕝\bbl
𝕞\bbm
𝕟\bbn
𝕠\bbo
𝕡\bbp
𝕢\bbq
𝕣\bbr
𝕤\bbs
𝕥\bbt
𝕦\bbu
𝕧\bbv
𝕨\bbw
𝕩\bbx
𝕪\bby
𝕫\bbz
𝟘\b0
𝟙\b1
𝟚\b2
𝟛\b3
𝟜\b4
𝟝\b5
𝟞\b6
𝟟\b7
𝟠\b8
𝟡\b9
\bsum
𝟬\sb0
𝟭\sb1
𝟮\sb2
𝟯\sb3
𝟰\sb4
𝟱\sb5
𝟲\sb6
𝟳\sb7
𝟴\sb8
𝟵\sb9
\Im
\Re
\mathscr{I}
\quad
\wp
¬\!
\&
\and
\v
\top
\bot
\+
\veebar
\barwedge
\And
\Or
\curlyvee
\curlywedge
\heyting
\hnot
\|=>
\entails
\-|
\models
\|=
\||-
\|||-
\||=
\nvdash
\nvDash
\nVdash
\nVDash
\l
\r
\iff
\l--
\hom
\lr--
\u
\d
\ud-
\nwarrow
\nearrow
\dr-
\dl-
\l=
\u=
\=>
\d=
\lr=
\ud=
\ul=
\ur=
\dr=
\dl=
\nattrans
\nleftarrow
\nrightarrow
\nleftrightarrow
\nLeftarrow
\nLeftrightarrow
\nRightarrow
\r-l-
\u-d-
\leftrightarrows
\leftleftarrows
\u-2
\r-2
\downdownarrows
\d-u-
\r-3
\twoheadleftarrow
\uu-
\twoheadrightarrow
\dd-
\leftharpoonup
\leftharpoondown
\uprightharpoon
\upleftharpoon
\rightharpoonup
\rightharpoondown
\downrightharpoon
\downleftharpoon
\leftrightharpoons
\rightleftharpoons
\leftarrowtail
\pr
\hookleftarrow
\hookrightarrow
\l~
\leadsto
\looparrowleft
\looparrowright
\leftrightsquigarrow
\curvearrowleft
\curvearrowright
\circlearrowleft
\circlearrowright
\squigarrowright
\Lsh
\Rsh
\l-|
\u-|
\ma
\d-|
\ud-|
\dz
\l==
\r==
\u==
\d==
\specializes
\functor
\-o
∘*\o*
\oplus
\o--
\ox
\o/
\o.
\oo
\circledast
\o=
\o-
\b+
\b-
\bx
\intercal
\O*
\O.
\O+
→₀\to0
→₁\to1
→₁ₛ\to1s
→ₐ\toa
→ᵇ\tob
→ₗ\tol
→ₛₗ\tosl
→ₘ\tom
→ₚ\rp
→ₛ\tos
¿\?
\Bumpeq
\bumpeq
\.=
\.=.
\fallingdotseq
\risingdotseq
\:=
\eqcolon
\eqcirc
\=o
\(=
\and=
\or=
\*=
\t=
\def=
\m=
\==
\nequiv
\===
\~
\nsim
\-~
\equiv
\nsimeq
\iso
\ncong
\~~
\napprox
\~~-
\~~~
\backcong
\asymp
\between
\neq
\leqslant
\leqq
\lneqq
\lessapprox
\lessgtr
\lesseqgtr
\geqslant
\geqq
\gneqq
\gtrapprox
\gtrless
\gtreqless
\ll
\gg
\Ll
\ggg
\prec
\preceq
\precapprox
\curlyeqprec
\precnapprox
\succ
\succcurlyeq
\succapprox
\curlyeqsucc
\succnapprox
\covers
\gtrdot
⩿\wcovby
\notlt
\ngtr
\nleqq
\ngeqq
\nprec
\nsucc
\vartriangleleft
\vartriangleright
\trianglelefteq
\trianglerighteq
\npreceq
\nsucceq
\ntriangleleft
\ntriangleright
\ntrianglelefteq
\ntrianglerighteq
\squbn
\squpn
\|
\nmid
\parallel
\nparallel
\<~nn
\>~nn
\inf
\lub
\infi
\wr
\supsetneqq
\in
\notin
\ni
\nni
\emptyset
\\\
\increment
\smallsetminus
\.-
\ssub
\ssup
\nsubset
\nsupset
\ss
\supseteqq
\nsubseteqq
\nsupseteqq
\subsetneqq
\ssqub
\ssqup
\squb
\squp
\Subset
\Supset
\i
\union
\u.
\u+
\I
⋂₀\I0
\U
⋃₀\U0
\Cap
\Cup
\U.
\U+
\supr
\all
∀ᶠ\allf
∀ᵐ\allm
\exists
∃ᶠ\exf
\nexists
Ø\O
\compl
\complementprefix
𝒫\powerset
\aleph
ℵ₀\aleph0
\beth
\gimel
\daleth
\C
\H
\N
ℕ∞\enat
\bp
\Q
\R
ℝ≥0\Rge0
ℝ≥0∞\ennreal
\Z
ℤ√\Zsqrt
𝔸\A
𝔹\bb
𝔽\F
𝕂\K
\prod
∏ᶠ\finprod
\amalg
\sum
∑ᶠ\finsum
\integral
\oint
\oiint
\integral-
±\pm
×\x
÷\division
\minus
\mp
\.+
\asterisk
\ast
\*
\divideontimes
·\.
\o
\span
\tr
\root
\surd3
\surd4
\pd
\nabla
\propto
\infty
\hbar
\ell
\ltimes
\rtimes
\leftthreetimes
\frown
\smallsmile
×ˢ\xs
×ᶠ\xf
\pitensorproduct
\X
⨿\coprod
¼\frac14
½\frac12
¾\frac34
\textfractionsolidus
\per
\frac13
\frac23
\frac15
\frac25
\frac35
\frac45
\frac16
\frac56
\frac18
\frac38
\frac58
\frac78
\frac1
\rightangle
\angle
\measuredangle
\sphericalangle
\therefore
\because
\qed
\:
\::
\-:
\::-
\:~
\?=
\bowtie
\#
(☐)\()
(☐)_\()_
[☐]\[]
[☐]_\[]_
{☐}\{}
{☐}_\{}_
«☐»\f<<>>
‖☐‖\||||
‖☐‖₊\nnnorm
‹☐›\f<>
⁅☐⁆\[--]
⌈☐⌉\ceil
⌈☐⌉₊\nceil
⌊☐⌋\floor
⌊☐⌋₊\nfloor
⟦☐⟧\[[]]
⟨☐⟩\<>
⟮☐⟯\([])'
⦃☐⦄\{{}}
⦋☐⦌\s[]
⸨☐⸩\(())
«\f<<
»\f>>
\||
\lq
\rq
\glq
\ldq
\rdq
\glqq
\ldots
\f<
\f>
\textlquill
\textrquill
\...
\ddots
\lceil
\cuR
\lfloor
\clR
\ulcorner
\urcorner
\llcorner
\lrcorner
\(b
\rbag
\[[
\]]
\<
\>
\<<
\>>
\([
\])
\{{
\}}
\((
\))
\ldata
\rdata
\llbracket
\rrbracket
¢\cent
£\pounds
¤\currency
¥\yen
؋\afghani
฿\textbaht
\textcolonmonetary
\cruzeiro
\textlira
\mill
\naira
\peseta
\rupee
\textwon
\dong
\euro
\kip
\tugrik
\drachma
\textpeso
\guarani
\austral
\hryvnia
\cedi
\spesmilo
\tenge
\manat
\ruble
\lari
\ounce
𐆎\nomisma
K\kelvin
\n\n
¡\r!
¦\brokenbar
§\section
©\copyright
ª\ordfeminine
®\circledR
°\degree
µ\textmu
\paragraph
º\ordmasculine
\^perp
\en
\em
\dagger
\ddagger
\smul
\but
\permil
\textpertenthousand
\prime
\backprime
\textreferencemark
\!!
\textinterrobang
\undertie
\tie
\??
\!?
\textdiscount
\celsius
\numero
\textcircledP
\textrecipe
\telephone
\mho
\textestimated
\facsimile
\backepsilon
\backsim
\dotsquare
\diamond
\rightthreetimes
\backsimeq
\pitchfork
\eqslantless
\eqslantgtr
\lnapprox
\gnapprox
\vdots
\diameter
\apl
\circledS
\---
\--_
\--.
\--=
\sqb
\square
\sqo
\sq.
\blacksquare
\reb
\rew
\pab
\paw
\bigtriangleup
\blacktriangle
\triangle
\rhd
\t
\transport
\bigtriangledown
\blacktriangledown
\triangledown
\Tr
\lhd
\tb
\triangleleft
\dib
\diw
\di.
\ciw
\ci..
\ci.
\cib
\textopenbullet
\boxmid
\ciO
\sq
\bigstar
\caution
\radioactive
\biohazard
\Frowny
\Smiley
\blacksmiley
\female
\male
\spadesuit
\diamondsuit
\clubsuit
\heartsuit
\note
\textmusicalnote
\flat
\natural
\die
\warning
\scissor
\Letter
\checkmark
\textdied
\maltese
\st4
\lozenge
\st8
\st6
\st12
\perp
\lsimplex
\rsimplex
\lf
\quot
\tiny
⧿\miny
\uncertainty
\partnership
\^Hstroke
\^oe
\sbs
🚧\construction
🛇\prohibited
🛑\octagonal
made with love by quartztz.com