2002-05-24 08:29:16 +00:00
|
|
|
|
|
|
|
#
|
|
|
|
# Idea of "autocorrection" and parts of this file are shamelessly stolen
|
|
|
|
# from TeXMacs (they give vdhoeven@texmacs.org as contact)
|
|
|
|
#
|
|
|
|
# We do it a bit differently and allow corrections only to combine a symbol
|
|
|
|
# and a char to a new symbol.
|
|
|
|
#
|
2003-10-13 09:50:10 +00:00
|
|
|
#
|
|
|
|
|
2002-05-24 08:29:16 +00:00
|
|
|
| , \lfloor
|
|
|
|
\lfloor * |,
|
|
|
|
| ' \lceil
|
|
|
|
\lceil * |'
|
|
|
|
, | \rfloor
|
|
|
|
\rfloor * ,|
|
|
|
|
' | \rceil
|
|
|
|
\rceil * '|
|
|
|
|
\llbracket * [[*
|
|
|
|
\rrbracket * ]]*
|
2003-10-13 09:50:10 +00:00
|
|
|
|
2002-05-24 08:29:16 +00:00
|
|
|
\cap * \sqcap
|
|
|
|
\cup * \sqcup
|
|
|
|
\vee * \curlyvee
|
|
|
|
\curlyvee * \curlyveeuparrow
|
|
|
|
\curlyveeuparrow * \curlyveedownarrow
|
2019-06-03 09:37:15 +00:00
|
|
|
\curlyveedownarrow * \vee
|
2003-10-13 09:50:10 +00:00
|
|
|
|
2002-05-24 08:29:16 +00:00
|
|
|
< / \nless
|
|
|
|
> / \ngtr
|
|
|
|
< = \leqslant
|
|
|
|
> = \geqslant
|
|
|
|
\leqslant / \nleqslant
|
|
|
|
\geqslant / \ngeqslant
|
|
|
|
\leqslant * \leq
|
|
|
|
\geslant * \geq
|
|
|
|
\leq / \nleq
|
|
|
|
\geq / \ngeq
|
|
|
|
< < \ll
|
|
|
|
\ll < \lll
|
|
|
|
> > \gg
|
|
|
|
\gg > \ggg
|
|
|
|
\ll = \lleq
|
|
|
|
\lll = \llleq
|
|
|
|
\gg = \ggeq
|
|
|
|
\ggg = \gggeq
|
|
|
|
\ll / \nll
|
|
|
|
\lll / \nlll
|
|
|
|
\gg / \ngg
|
|
|
|
\ggg / \nggg
|
|
|
|
\lleq / \nlleq
|
|
|
|
\llleq / \nllleq
|
|
|
|
\ggeq / \nggeq
|
|
|
|
\gggeq / \ngggeq
|
|
|
|
< . \lessdot
|
|
|
|
. > \gtrdot
|
|
|
|
\leqslant . \lesseqdot
|
|
|
|
\gtrdot = \gtreqdot
|
2003-10-13 09:50:10 +00:00
|
|
|
|
2002-05-24 08:29:16 +00:00
|
|
|
< * \prec
|
|
|
|
> * \succ
|
|
|
|
\prec / \nprec
|
|
|
|
\succ / \nsucc
|
|
|
|
\prec = \preccurlyeq
|
|
|
|
\succ = \succcurlyeq
|
|
|
|
\preccurlyeq / \npreccurlyeq
|
|
|
|
\succcurlyeq / \nsucccurlyeq
|
|
|
|
\preccurlyeq * \preceq
|
|
|
|
\succcurlyeq * \succeq
|
|
|
|
\preceq / \npreceq
|
|
|
|
\succeq / \nsucceq
|
|
|
|
\npreceq * \precneqq
|
|
|
|
\nsucceq * \succneqq
|
|
|
|
\ll * \precprec
|
|
|
|
\precprec * \precprecprec
|
|
|
|
\gg * \succsucc
|
|
|
|
\succsucc * \succsuccsucc
|
|
|
|
\precprec = \precpreceq
|
|
|
|
\lll * \precprecprec
|
|
|
|
\precprecprec = \precprecpreceq
|
|
|
|
\succsucc = \succsucceq
|
|
|
|
\ggg = \succsuccsucc
|
|
|
|
\succsuccsucc = \succsuccsucceq
|
|
|
|
\precprec / \nprecprec
|
|
|
|
\precprecprec / \nprecprecprec
|
|
|
|
\succsucc / \nsuccsucc
|
|
|
|
\succsuccsucc / \nsuccsuccsucc
|
|
|
|
\precpreceq / \nprecpreceq
|
|
|
|
\precprecpreceq / \nprecprecpreceq
|
|
|
|
\succsucceq / \nsuccsucceq
|
|
|
|
\succsuccsucceq / \nsuccsuccsucceq
|
|
|
|
|
|
|
|
\prec . \precdot
|
|
|
|
\succ . \dotsucc
|
|
|
|
\precdot . \preceqdot
|
|
|
|
\dotsucc . \dotsucceq
|
|
|
|
\precprec * \llangle
|
|
|
|
\succsucc * \rrangle
|
|
|
|
|
|
|
|
< > \lessgtr
|
|
|
|
> < \gtrless
|
|
|
|
< ~ \lesssim
|
|
|
|
\lesssim ~ \lessapprox
|
|
|
|
\prec ~ \precsim
|
|
|
|
\precsim ~ \precapprox
|
|
|
|
> ~ \gtrsim
|
|
|
|
\gtrsim ~ \gtrapprox
|
|
|
|
\succ ~ \gtrsim
|
|
|
|
\gtrsim ~ \gtrapprox
|
|
|
|
\leq * \leqq
|
|
|
|
\geq * \geqq
|
|
|
|
\leq > \lesseqgtr
|
|
|
|
\geq < \gtrqless
|
|
|
|
|
|
|
|
- > \rightarrow
|
|
|
|
< - \leftarrow
|
|
|
|
\leftarrow > \leftrightarrow
|
|
|
|
\rightarrow - \longrightarrow
|
|
|
|
\leftarrow - \longleftarrow
|
|
|
|
\longleftarrow > \longleftrightarrow
|
|
|
|
= > \Rightarrow
|
2023-03-19 08:34:01 +00:00
|
|
|
= < \Leftarrow
|
|
|
|
\Rightarrow = \Longrightarrow
|
2023-03-19 09:50:13 +00:00
|
|
|
\Leftarrow > \Leftrightarrow
|
2023-03-19 08:34:01 +00:00
|
|
|
\Leftarrow = \Longleftarrow
|
|
|
|
\Longleftarrow > \Longleftrightarrow
|
2002-05-24 08:29:16 +00:00
|
|
|
|
2023-03-19 09:26:08 +00:00
|
|
|
\leftarrow * \longleftarrow
|
|
|
|
\longleftarrow * \longleftrightarrow
|
2023-03-19 09:50:13 +00:00
|
|
|
\longleftrightarrow * \leftrightarrow
|
|
|
|
\leftrightarrow * \leftarrow
|
2023-03-19 09:26:08 +00:00
|
|
|
\rightarrow * \longrightarrow
|
|
|
|
\longrightarrow * \longleftrightarrow
|
|
|
|
|
|
|
|
\Leftarrow * \Longleftarrow
|
|
|
|
\Longleftarrow * \Longleftrightarrow
|
2023-03-19 09:50:13 +00:00
|
|
|
\Longleftrightarrow * \Leftrightarrow
|
|
|
|
\Leftrightarrow * \Leftarrow
|
2023-03-19 09:26:08 +00:00
|
|
|
\Rightarrow * \Longrightarrow
|
|
|
|
\Longrightarrow * \Longleftrightarrow
|
2002-05-24 08:29:16 +00:00
|
|
|
|
|
|
|
@ * \circ
|
|
|
|
\circ / \varnothing
|
|
|
|
\circ + \oplus
|
|
|
|
\circ - \ominus
|
|
|
|
@ x \otimes
|
|
|
|
\circ : \oover
|
|
|
|
\circ . \odot
|
|
|
|
@ R \circledR
|
|
|
|
@ S \circledS
|
|
|
|
\varnothing * \oslash
|
|
|
|
@ \ \obslash
|
|
|
|
@ @ \infty
|
|
|
|
\circ < \olessthan
|
|
|
|
\circ > \ogreaterthan
|
|
|
|
\circ & \owedge
|
|
|
|
\circ | \obar
|
|
|
|
\obar * \ovee
|
|
|
|
\circ v \ovee
|
|
|
|
\circ @ \infty
|
|
|
|
@@ * \varocircle
|
|
|
|
-@ @ \infty
|
|
|
|
\circ * \box
|
|
|
|
\box + \boxplus
|
|
|
|
\box - \boxminus
|
|
|
|
\box x \boxtimes
|
|
|
|
\box . \boxdot
|
|
|
|
\box / \boxslash
|
|
|
|
\box \ \boxbslash
|
|
|
|
\box @ \boxcircle
|
|
|
|
\boxcircle * \boxbox
|
|
|
|
\box | \boxbar
|
|
|
|
\box * \bullet
|
|
|
|
\bullet * \blacksquare
|
2003-10-13 09:50:10 +00:00
|
|
|
|
2002-05-24 08:29:16 +00:00
|
|
|
= * \asymp
|
|
|
|
\asymp * \equiv
|
|
|
|
\equiv * \asympasymp
|
|
|
|
\asympasymp * \simsim
|
|
|
|
~ * \sim
|
|
|
|
\sim ~ \approx
|
|
|
|
\approx - \approxeq
|
|
|
|
\sim - \simeq
|
|
|
|
\sim = \cong
|
|
|
|
= / \neq
|
|
|
|
\asymp / \nasymp
|
|
|
|
\equiv / \nequiv
|
|
|
|
\asympasymp / \nasympasymp
|
|
|
|
\simsim / \nsimsim
|
|
|
|
\sim / \nsim
|
|
|
|
\approx / \napprox
|
|
|
|
\simeq / \nsimeq
|
|
|
|
\cong / \ncong
|
2003-10-13 09:50:10 +00:00
|
|
|
|
|
|
|
#| \|
|
2002-05-24 08:29:16 +00:00
|
|
|
| * \shortmid
|
|
|
|
\shortmid * \varshortmid
|
2019-06-03 08:21:40 +00:00
|
|
|
| | \|
|
|
|
|
\| | \interleave
|
|
|
|
\| * \shortparallel
|
2002-05-24 08:29:16 +00:00
|
|
|
| - \vdash
|
|
|
|
\vdash - \longvdash
|
2019-06-03 08:21:40 +00:00
|
|
|
\| - \Vdash
|
2002-05-24 08:29:16 +00:00
|
|
|
\Vdash - \longVdash
|
|
|
|
\interleave - \Vvdash
|
|
|
|
\Vvdash - \longVvdash
|
|
|
|
- | \dashv
|
|
|
|
|
|
|
|
< | \vartriangleleft
|
|
|
|
\vartriangleleft * \blacktriangleleft
|
|
|
|
\vartriangleleft / \ntriangleleft
|
|
|
|
\vartriangleleft = \trianglelefteqslant
|
|
|
|
\trianglelefteqslant / \ntrianglelefteqslant
|
|
|
|
\trianglelefteqslant * \trianglelefteq
|
|
|
|
\trianglelefteq / \ntriangleqleft
|
|
|
|
| > \vartriangleright
|
|
|
|
\vartriangleright * \blacktriangleright
|
|
|
|
\vartriangleright / \ntriangleright
|
|
|
|
\vartriangleright = \trianglerighteq
|
|
|
|
\trianglerighteq / \ntriangleqright
|
|
|
|
\trianglerighteq * \trianglerighteqslant
|
|
|
|
\trianglerighteqslant / \ntrianglerighteqslant
|
|
|
|
|
|
|
|
- * \um
|
|
|
|
+ - \pm
|
|
|
|
\pm * \upm
|
|
|
|
- + \mp
|
|
|
|
\mp * \ump
|
|
|
|
@ = \circeq
|
|
|
|
= @ \eqcirc
|
|
|
|
- @ \multimap
|
|
|
|
. = \doteq
|
2019-06-03 14:54:28 +00:00
|
|
|
.. . \ldots
|
2002-05-24 08:29:16 +00:00
|
|
|
\ldots * \cdots
|
2019-06-03 14:54:28 +00:00
|
|
|
\cdots * \vdots
|
|
|
|
\vdots * \ddots
|
|
|
|
\ddots * \iddots
|
|
|
|
\iddots * \ldots
|
2002-05-24 08:29:16 +00:00
|
|
|
: = \assign
|
|
|
|
+ = \plusassign
|
|
|
|
- = \minusassign
|
|
|
|
/ * \div
|
|
|
|
* * \ast
|
|
|
|
\ast * \times
|
|
|
|
\times * \cdot
|
2003-10-13 09:50:10 +00:00
|
|
|
|
2019-06-03 10:32:13 +00:00
|
|
|
\prec * \langle
|
|
|
|
\langle * \subset
|
2002-05-24 08:29:16 +00:00
|
|
|
\subset * \in
|
2003-10-13 09:50:10 +00:00
|
|
|
\in * \sqsubset
|
2002-05-24 08:29:16 +00:00
|
|
|
\subset = \subseteq
|
|
|
|
\subseteq / \nsubseteq
|
|
|
|
\subseteq * \subseteqq
|
2019-06-03 10:32:13 +00:00
|
|
|
\sqsubset * \leftslice
|
|
|
|
\leftslice * <
|
2003-10-13 09:50:10 +00:00
|
|
|
|
2002-05-24 08:29:16 +00:00
|
|
|
\subseteqq / \nsubseteqq
|
|
|
|
\nsubseteqq * \subsetneq
|
|
|
|
\subsetneq * \varsubsetneq
|
|
|
|
\varsubsetneq * \subsetneqq
|
|
|
|
\subsetneqq * \varsubsetneqq
|
|
|
|
\subset + \subsetplus
|
|
|
|
\subsetplus = \subsetpluseq
|
|
|
|
\subseteq + \subsetpluseq
|
|
|
|
\in / \nin
|
2019-06-03 10:32:13 +00:00
|
|
|
|
|
|
|
\succ * \rangle
|
|
|
|
\rangle * \supset
|
|
|
|
\supset * \ni
|
|
|
|
\ni * \sqsupset
|
2002-05-24 08:29:16 +00:00
|
|
|
\supset = \supseteq
|
|
|
|
\supseteq / \nsupseteq
|
|
|
|
\supseteq * \supseteqq
|
2019-06-03 10:32:13 +00:00
|
|
|
\sqsupset * \rightslice
|
|
|
|
\rightslice * >
|
2003-10-13 09:50:10 +00:00
|
|
|
|
2002-05-24 08:29:16 +00:00
|
|
|
\supseteqq / \nsupseteqq
|
|
|
|
\supseteq / \supsetneq
|
2019-06-03 10:32:13 +00:00
|
|
|
\supsetneq * \nsupseteq
|
2002-05-24 08:29:16 +00:00
|
|
|
\supset + \supsetplus
|
|
|
|
\supsetplus = \supsetpluseq
|
|
|
|
\supseteq + \supsetpluseq
|
|
|
|
\ni / \nni
|
|
|
|
|
|
|
|
#
|
|
|
|
# The following is available in TeXMacs, but not (yet) in LyX
|
|
|
|
#
|
|
|
|
|
|
|
|
#--| \longdashv
|
2019-06-03 08:21:40 +00:00
|
|
|
| = \vDash
|
2002-05-24 08:29:16 +00:00
|
|
|
#\vDash = \longvDash
|
|
|
|
#||= \VDash
|
|
|
|
#||== \longVDash
|
2019-06-03 08:21:40 +00:00
|
|
|
#| / \nmid
|
|
|
|
\| / \nparallel
|
|
|
|
\shortmid / \nshortmid
|
|
|
|
\shortparallel / \nshortparallel
|
|
|
|
\vdash / \nvdash
|
|
|
|
||- / \nVdash
|
2002-05-24 08:29:16 +00:00
|
|
|
#-|/ \ndashv
|
|
|
|
#-||/ \ndashV
|
2019-06-03 08:21:40 +00:00
|
|
|
\vDash / \nvDash
|
|
|
|
\nvDash * \nVDash
|
2002-05-24 08:29:16 +00:00
|
|
|
#=|/ \nDashv
|
|
|
|
#=||/ \nDashV
|
|
|
|
#
|
|
|
|
#<=**> \lesseqqgtr
|
|
|
|
#>=**< \gtreqqless
|
|
|
|
#<>/ \nlessgtr
|
|
|
|
#></ \ngtrless
|
|
|
|
#<~/ \nlesssim
|
|
|
|
#<~/* \lnsim
|
|
|
|
#<~~/ \nlessapprox
|
|
|
|
#<~~/* \lnapprox
|
|
|
|
#<*~/ \nprecsim
|
|
|
|
#<*~/* \precnsim
|
|
|
|
#<*~~/ \nprecapprox
|
|
|
|
#<*~~/* \precnapprox
|
|
|
|
#>~/ \ngtrsim
|
|
|
|
#>~/* \gnsim
|
|
|
|
#>~~/ \ngtrapprox
|
|
|
|
#>~~/* \gnapprox
|
|
|
|
#>*~/ \nsuccsim
|
|
|
|
#>*~/* \succnsim
|
|
|
|
#>*~~/ \nsuccapprox
|
|
|
|
#>*~~/* \succnapprox
|
|
|
|
#<=**/ \nleqq
|
|
|
|
#>=**/ \ngeqq
|
|
|
|
#<=*>/ \nlesseqgtr
|
|
|
|
#>=*</ \ngtreqless
|
|
|
|
#<=**>/ \nlesseqqgtr
|
|
|
|
#>=**</ \ngtreqqless
|
|
|
|
#<=*/* \lneq
|
|
|
|
#<=**/* \lneqq
|
|
|
|
#<=**/** \lvertneqq
|
|
|
|
#>=*/* \gneq
|
|
|
|
#>=**/* \gneqq
|
|
|
|
#>=**/** \gvertneqq
|
2019-06-03 08:21:40 +00:00
|
|
|
[[ * \llbracket
|
|
|
|
]] * \rrbracket
|
|
|
|
EE a \amalg
|
|
|
|
EE d \partial
|
|
|
|
EE p \wp
|
|
|
|
EE n \cap
|
|
|
|
EE u \cup
|
|
|
|
EE w \wedge
|
|
|
|
\wedge * \curlywedge
|
|
|
|
\curlywedge * \curlywedgeuparrow
|
|
|
|
\curlywedgeuparrow * \curlywedgedownarrow
|
2019-06-03 09:37:15 +00:00
|
|
|
\curlywedgedownarrow * \wedge
|
2019-06-03 08:21:40 +00:00
|
|
|
EE v \vee
|
|
|
|
EE x \times
|
2023-03-20 01:30:34 +00:00
|
|
|
EE V \forall
|
|
|
|
EE E \exists
|
2002-05-24 08:29:16 +00:00
|
|
|
|
|
|
|
# <***/ \nsqsubset
|
|
|
|
# <***= \sqsubseteq
|
|
|
|
# <***=/ \nsqsubseteq
|
|
|
|
# >*=/** \varsupsetneq
|
|
|
|
# >*=*/* \supsetneqq
|
|
|
|
# >*=*/** \varsupsetneqq
|
|
|
|
# >*** \sqsupset
|
|
|
|
# >***/ \nsqsupset
|
|
|
|
# >***= \sqsupseteq
|
|
|
|
# >***=/ \nsqsupseteq
|
|
|
|
|
2019-06-03 08:21:40 +00:00
|
|
|
( * \bigl(
|
|
|
|
\bigl( * \Bigl(
|
|
|
|
\Bigl( * \biggl(
|
|
|
|
\biggl( * \Biggl(
|
|
|
|
\Biggl( * (
|
|
|
|
|
|
|
|
) * \bigl)
|
|
|
|
\bigl) * \Bigl)
|
|
|
|
\Bigl) * \biggl)
|
|
|
|
\biggl) * \Biggl)
|
|
|
|
\Biggl) * )
|
|
|
|
|
|
|
|
[ * \bigl[
|
|
|
|
\bigl[ * \Bigl[
|
|
|
|
\Bigl[ * \biggl[
|
|
|
|
\biggl[ * \Biggl[
|
|
|
|
\Biggl[ * [
|
|
|
|
|
|
|
|
] * \bigl]
|
|
|
|
\bigl] * \Bigl]
|
|
|
|
\Bigl] * \biggl]
|
|
|
|
\biggl] * \Biggl]
|
|
|
|
\Biggl] * ]
|
|
|
|
|
|
|
|
] * \bigl]
|
|
|
|
\bigl] * \Bigl]
|
|
|
|
\Bigl] * \biggl]
|
|
|
|
\biggl] * \Biggl]
|
|
|
|
\Biggl] * ]
|
|
|
|
|
|
|
|
\{ * \bigl\{
|
|
|
|
\bigl\{ * \Bigl\{
|
|
|
|
\Bigl\{ * \biggl\{
|
|
|
|
\biggl\{ * \Biggl\{
|
|
|
|
\Biggl\{ * \{
|
|
|
|
|
|
|
|
\} * \bigl\}
|
|
|
|
\bigl\} * \Bigl\}
|
|
|
|
\Bigl\} * \biggl\}
|
|
|
|
\biggl\} * \Biggl\}
|
|
|
|
\Biggl\} * \}
|
2002-05-24 08:29:16 +00:00
|
|
|
|
|
|
|
# EE l \bigl
|
|
|
|
# EE m \bigm
|
|
|
|
# EE r \bigr
|
|
|
|
# EE @ \bigop
|
|
|
|
# EE L \int
|