mmascii - Metamath Proof Explorer

Symbol to ASCII Correspondence for Text-Only Browsers (in order of appearance in $c and $v statements in the database)

Symbol	ASCII
(	(
)	)
->	->
-.	-.
wff	wff
|-	|-
ph	ph
ps	ps
ch	ch
th	th
ta	ta
et	et
ze	ze
si	si
rh	rh
<->	<->
\/	\/
/\	/\
-/\	-/\
T.	T.
F.	F.
A.	A.
set	set
x	x
y	y
z	z
w	w
v	v
u	u
=	=
class	class
A	A
B	B
e.	e.
E.	E.
[	[
/	/
]	]
f	f
g	g
E!	E!
E*	E*
t	t
{	{
|	|
}	}
C	C
D	D
P	P
Q	Q
R	R
S	S
T	T
U	U
e	e
h	h
i	i
j	j
k	k
m	m
n	n
o	o
E	E
F	F
G	G
H	H
I	I
J	J
K	K
L	L
M	M
N	N
V	V
W	W
X	X
Y	Y
Z	Z
O	O
s	s
r	r
q	q
p	p
a	a
b	b
c	c
d	d
l	l
=/=	=/=
e/	e/
_V	_V
[_	[_
]_	]_
\	\
u.	u.
i^i	i^i
C_	C_
C.	C.
(/)	(/)
if	if
,	,
~P	~P
<.	<.
>.	>.
U.	U.
|^|	|^|
U_	U_
|^|_	|^|_
Tr	Tr
_E	_E
_I	_I
Po	Po
Or	Or
Fr	Fr
We	We
Ord	Ord
On	On
Lim	Lim
suc	suc
om	om
X.	X.
`'	`'
dom	dom
ran	ran
|`	|`
"	"
o.	o.
Rel	Rel
Fun	Fun
Fn	Fn
:	:
-->	-->
-1-1->	-1-1->
-onto->	-onto->
-1-1-onto->	-1-1-onto->
`	`
Isom	Isom
|->	|->
1st	1st
2nd	2nd
iota	iota
rec	rec
1o	1o
2o	2o
+o	+o
.o	.o
^o	^o
Er	Er
/.	/.
^m	^m
^pm	^pm
X_	X_
~~	~~
~<_	~<_
~<	~<
Fin	Fin
Undef	Undef
iota_	iota_
sup	sup
R1	R1
rank	rank
card	card
aleph	aleph
cf	cf
+c	+c
N.	N.
+N	+N
.N	.N
<N	<N
+pQ	+pQ
.pQ	.pQ
~Q	~Q
Q.	Q.
1Q	1Q
+Q	+Q
.Q	.Q
*Q	*Q
<Q	<Q
P.	P.
1P	1P
+P.	+P.
.P.	.P.
<P	<P
+pR	+pR
.pR	.pR
~R	~R
R.	R.
0R	0R
1R	1R
-1R	-1R
+R	+R
.R	.R
<R	<R
<R	<RR
CC	CC
RR	RR
0	0
1	1
_i	_i
+	+
x.	x.
-	-
-u	-u
<_	<_
NN	NN
NN0	NN0
ZZ	ZZ
QQ	QQ
RR+	RR+
+oo	+oo
-oo	-oo
RR*	RR*
<	<
2	2
3	3
4	4
5	5
6	6
7	7
8	8
9	9
10	10
|_	|_
mod	mod
==	==
(,)	(,)
(,]	(,]
[,)	[,)
[,]	[,]
ZZ>=	ZZ>=
...	...
seq1	seq1
shift	shift
limsup	limsup
seq	seq
seq0	seq0
^	^
sqr	sqr
Re	Re
Im	Im
*	*
abs	abs
!	!
_C	_C
#	#
~~>	~~>
sum_	sum_
-cn->	-cn->
exp	exp
_e	_e
sin	sin
cos	cos
pi	pi
Top	Top
TopSp	TopSp
Bases	Bases
topGen	topGen
X.t	tX
int	int
cls	cls
Clsd	Clsd
nei	nei
limPt	limPt
Cn	Cn
CnP	CnP
Haus	Haus
Met	Met
MetSp	MetSp
ball	ball
Open	Open
~~>m	~~>m
Cau	Cau
CMet	CMet
Grp	Grp
Id	Id
inv	inv
/g	/g
^g	^g
Abel	Abel
SubGrp	SubGrp
GrpAct	GrpAct
Ring	Ring
DivRing	DivRing
*-Fld	*-Fld
CVec	CVec
NrmCVec	NrmCVec
+v	+v
BaseSet	BaseSet
.s	.s
0v	0v
-v	-v
norm	norm
IndMet	IndMet
.i	.i
SubSp	SubSp
LnOp	LnOp
normOp	normOp
BLnOp	BLnOp
0op	0op
adj	adj
HmOp	HmOp
CPreHil	CPreHil
CBan	CBan
CHil	CHil
Poset	Poset
supw	supw
infw	infw
Lat	Lat
log	log
GrpHom	GrpHom
GrpIso	GrpIso
SymGrp	SymGrp
Toset	Toset
fi	fi
Homeo	Homeo
~=	~=
subSp	subSp
fBas	fBas
filGen	filGen
Fil	Fil
fLim1	fLim1
FilMap	FilMap
fLimf	fLimf
Comp	Comp
Fre	Fre
Con	Con
Plig	Plig
Dir	Dir
tail	tail
Ass	Ass
ExId	ExId
Magma	Magma
SemiGrp	SemiGrp
Mnd	Mnd
Com2	Com2
Fld	Fld
~H	~H
+h	+h
.h	.h
0h	0h
-h	-h
.ih	.ih
normh	normh
Cauchy	Cauchy
~~>v	~~>v
SH	SH
CH	CH
_|_	_|_
+H	+H
span	span
vH	vH
\/H	\/H
0H	0H
C_H	C_H
proj	proj
0hop	0hop
Iop	Iop
+op	+op
.op	.op
-op	-op
+fn	+fn
.fn	.fn
normop	normop
ConOp	ConOp
LinOp	LinOp
BndLinOp	BndLinOp
UniOp	UniOp
HrmOp	HrmOp
normfn	normfn
null	null
ConFn	ConFn
LinFn	LinFn
adjh	adjh
bra	bra
ketbra	ketbra
<_op	<_op
eigvec	eigvec
eigval	eigval
Lambda	Lambda
States	States
CHStates	CHStates
Atoms	Atoms
<o	<o
MH	MH
MH*	MH*
ph'	ph'
ps'	ps'
ch'	ch'
th'	th'
ta'	ta'
et'	et'
ze'	ze'
si'	si'
rh'	rh'
ph"	ph"
ps"	ps"
ch"	ch"
th"	th"
ta"	ta"
et"	et"
ze"	ze"
si"	si"
rh"	rh"
ph0	ph0
ps0	ps0
ch0_	ch0_
th0	th0
ta0	ta0
et0	et0
ze0	ze0
si0	si0
rh0	rh0
ph1	ph1
ps1	ps1
ch1	ch1
th1	th1
ta1	ta1
et1	et1
ze1	ze1
si1	si1
rh1	rh1
a'	a'
b'	b'
c'	c'
d'	d'
e'	e'
f'	f'
g'	g'
h'	h'
i'	i'
j'	j'
k'	k'
l'	l'
m'	m'
n'	n'
o'	o'
p'	p'
q'	q'
r'	r'
s'	s'
t'	t'
u'	u'
v'	v'
w'	w'
x'	x'
y'	y'
z'	z'
a"	a"
b"	b"
c"	c"
d"	d"
e"	e"
f"	f"
g"	g"
h"	h"
i"	i"
j"	j"
k"	k"
l"	l"
m"	m"
n"	n"
o"	o"
p"	p"
q"	q"
r"	r"
s"	s"
t"	t"
u"	u"
v"	v"
w"	w"
x"	x"
y"	y"
z"	z"
a0	a0
b0	b0
c0_	c0_
d0	d0
e0	e0
f0_	f0_
g0	g0
h0	h0
i0	i0
j0	j0
k0	k0
l0	l0
m0	m0
n0_	n0_
o0	o0
p0	p0
q0	q0
r0	r0
s0	s0
t0	t0
u0	u0
v0	v0
w0	w0
x0	x0
y0	y0
z0	z0
a1	a1
b1	b1
c1_	c1_
d1	d1
e1	e1
f1	f1
g1	g1
h1	h1
i1	i1
j1	j1
k1	k1
l1	l1
m1	m1
n1	n1
o1	o1
p1	p1
q1	q1
r1	r1
s1	s1
t1	t1
u1	u1
v1	v1
w1	w1
x1	x1
y1	y1
z1	z1
A'	A'
B'	B'
C'	C'
D'	D'
E'	E'
F'	F'
G'	G'
H'	H'
I'	I'
J'	J'
K'	K'
L'	L'
M'	M'
N'	N'
O'	O'
P'	P'
Q'	Q'
R'	R'
S'	S'
T'	T'
U'	U'
V'	V'
W'	W'
X'	X'
Y'	Y'
Z'	Z'
A"	A"
B"	B"
C"	C"
D"	D"
E"	E"
F"	F"
G"	G"
H"	H"
I"	I"
J"	J"
K"	K"
L"	L"
M"	M"
N"	N"
O"	O"
P"	P"
Q"	Q"
R"	R"
S"	S"
T"	T"
U"	U"
V"	V"
W"	W"
X"	X"
Y"	Y"
Z"	Z"
A0	A0
B0	B0
C0	C0
D0	D0
E0	E0
F0	F0
G0	G0
H0	H0
I0	I0
J0	J0
K0	K0
L0	L0
M0	M0
N0	N0
O0	O0
P0	P0
Q0	Q0
R0	R0
S0	S0
T0	T0
U0	U0
V0	V0
W0	W0
X0	X0
Y0	Y0
Z0	Z0
A1	A1_
B1	B1_
C1	C1_
D1	D1_
E1	E1
F1	F1_
G1	G1_
H1	H1_
I1	I1_
J1	J1
K1	K1
L1	L1_
M1	M1_
N1	N1
O1	O1_
P1	P1
Q1	Q1
R1_	R1_
S1	S1_
T1	T1
U1	U1
V1	V1_
W1	W1
X1	X1
Y1	Y1
Z1	Z1
fns	_fns
pred	_pred
Se	_Se
FrSe	_FrSe
trCl	_trCl
TrFo	_TrFo
||	||
gcd	gcd
Prime	Prime
Pred	Pred
Trcl	Trcl
No	No
<s	<s
bday	bday
gcdOLD	gcdOLD
A1	A1
A2	A2
B1	B1
B2	B2
C1	C1
C2	C2
D1	D1
D2	D2
F1	F1
F2	F2
G1	G1
G2	G2
H1	H1
H2	H2
I1	I1
I2	I2
L1	L1
L2	L2
M1	M1
M2	M2
O1	O1
O2	O2
Ro1	Ro1
Ro2	Ro2
S1	S1
S2	S2
V1	V1
V2	V2
V3	V3
+t	+t
-t	-t
.t	.t
~t	~t
0t	0t
1t	1t
+w	+w
-w	-w
.w	.w
0w	0w
~w	~w
(+)	(+)
[.]	[.]
<>	<>
()	()
until	until
t+	t+
t*	t*
pr	pr
pr	prj
cset	cset
LatAlg	LatAlg
cur1	cur1
cur2	cur2
mxl	mxl
mnl	mnl
ub	ub
lb	lb
Preset	Preset
ge	ge
se	se
AntiDir	AntiDir
OrHom	OrHom
DecFun	DecFun
OrIso	OrIso
prod3	prod3_
prod_	prod_
Com1	Com1
Free	Free
star	star
^md	^md
Str	Str
Strx	Strx
len	len
conc	conc
str	str
Tofld	Tofld
zeroDiv	zeroDiv
Vec	Vec
SubVec	SubVec
RVec	RVec
+m	+m
xm	xm
.m	.m
RAffSp	RAffSp
topX	topX
TopGrp	TopGrp
Dgra	Dgra
Alg	Alg
dom	dom_
cod	cod_
id	id_
o	o_
Ded	Ded
Cat	Cat
hom	hom
Epi	Epi
Monic	Monic
Iso	Iso
cinv	cinv
Func	Func
Isofunc	Isofunc
SubCat	SubCat
Tarski	Tarski
tarskiMap	tarskiMap
tar	tar
tr	tr
Uni	Uni
line	line
Plibg	Plibg
Plibg0	Plibg0
Plibg1	Plibg1
Plibg2	Plibg2
Plibg3	Plibg3
Plibg4a	Plibg4a
Plibg4b	Plibg4b
seg	seg
1stc	1stc
2ndc	2ndc
Fne	Fne
Ref	Ref
PtFin	PtFin
LocFin	LocFin
Kol2	Kol2
Reg	Reg
Nrm	Nrm
UFil	UFil
fClus	fClus
fClusf	fClusf
II	II
~~>t	~~>t
TotBnd	TotBnd
Bnd	Bnd
Ismty	Ismty
RRn	Rn
PHtpy	PHtpy
~=ph	~=ph
pi1b	pi1b
*p	*p
pi1	pi1
RngHom	RngHom
RngIso	RngIso
~=r	~=r
CRing	CRing
Idl	Idl
PrIdl	PrIdl
MaxIdl	MaxIdl
PrRing	PrRing
Dmn	Dmn
IdlGen	IdlGen
Prt	Prt
HypGrph	HypGrph
PsGrph	PsGrph
SmpGrph	SmpGrph
Smo	Smo
.	(.
.	).
⊢	|-.
Struct	Struct
StrBldr	StrBldr
base	base
le	le
PosetNEW	PosetNEW
lt	lt
geNEW	geNEW
gt	gt
lub	lub
glb	glb
join	join
meet	meet
1.	1.
0.	0.
LatNEW	LatNEW
ComplLat	ComplLat
oc	oc
OP	OP
cm	cm
OL	OL
OML	OML
<oNEW	<oNEW
AtomsNEW	AtomsNEW
AtLat	AtLat
HL	HL
+g	+g
GrpNEW	GrpNEW
0g	0g
-g	-g
AbelNEW	AbelNEW
.r	.r
RingNEW	RingNEW
1rNEW	1rNEW
DivRingNEW	DivRingNEW
invr	invr
*v	*v
Ring*	Ring*
DivRing*	DivRing*
vbase	vbase
vadd	vadd
vsca	vsca
LVec	LVec
0vNEW	0vNEW
ip	ip
PreHil	PreHil
+ss	+ss
ocv	ocv
CSubSp	CSubSp
Hil	Hil
Lines	Lines
Points	Points
PSubSp	PSubSp
pmap	pmap
+P	+P
_|_P	_|_P

Copyright terms: Public domain