mmascii - Metamath Proof Explorer

Symbol to ASCII Correspondence for Text-Only Browsers (in order of first appearance)

Symbol	ASCII
(	(
)	)
→	->
¬	-.
wff	wff
⊢	|-
φ	ph
ψ	ps
χ	ch
θ	th
τ	ta
↔	<->
⋁	\/
⋀	/\
η	et
ζ	ze
σ	si
∀	A.
set	set
x	x
y	y
z	z
w	w
v	v
u	u
=	=
class	class
A	A
B	B
∈	e.
∃	E.
[	[
/	/
]	]
f	f
g	g
∃!	E!
∃*	E*
t	t
{	{
∣	|
}	}
C	C
D	D
P	P
Q	Q
R	R
S	S
T	T
U	U
F	F
G	G
≠	=/=
∉	e/
V	V
[	[_
]	]_
∖	\
∪	u.
∩	i^i
⊆	(_
⊂	(.
∅	(/)
if	if
,	,
ρ	rh
℘	P~
⟨	<.
⟩	>.
∪	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
×	X.
◡	`'
dom	dom
ran	ran
↾	|`
“	"
∘	o.
Rel	Rel
Fun	Fun
Fn	Fn
:	:
–→	-->
–1-1→	-1-1->
–onto→	-onto->
–1-1-onto→	-1-1-onto->
‘	`
Isom	Isom
h	h
j	j
k	k
m	m
n	n
o	o
H	H
J	J
K	K
L	L
M	M
N	N
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
rec	rec
↦	|->
1st	1st
2nd	2nd
1o	1o
2o	2o
+o	+o
·o	.o
↑o	^o
Er	Er
/	/.
↑m	^m
↑pm	^pm
X	X_
≈	~~
≼	~<_
≺	~<
sup	sup
R1	R1
rank	rank
card	card
ℵ	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
<ℝ	<RR
ℂ	CC
ℝ	RR
0	0
1	1
i	i
+	+
·	x.
−	-
-	-u
≤	<_
ℕ	NN
ℕ0	NN0
ℤ	ZZ
ℚ	QQ
ℝ+	RR+
+∞	+oo
-∞	-oo
ℝ*	RR*
<	<
2	2
3	3
4	4
5	5
6	6
7	7
8	8
9	9
10	10
⌊	|_
seq1	seq1
shift	shift
(,)	(,)
(,]	(,]
[,)	[,)
[,]	[,]
ℤ≥	ZZ>
...	...
lim sup	limsup
seq	seq
seq0	seq0
↑	^
√	sqr
ℜ	Re
ℑ	Im
∗	*
abs	abs
!	!
C	C.
⇝	~~>
Σ	sum_
–cn→	-cn->
exp	exp
e	e
sin	sin
cos	cos
π	pi
Top	Top
TopSp	TopSp
Bases	Bases
topGen	topGen
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
Abel	Abel
SubGrp	SubGrp
Ring	Ring
CVec	CVec
NrmCVec	NrmCVec
+v	+v
Base	Base
·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
join	join
meet	meet
Lat	Lat
log	log
ℋ	H~
+h	+h
·h	.h
0h	0h
−h	-h
·ih	.ih
normh	normh
Cauchy	Cauchy
⇝v	~~>v
Sℋ	SH
Cℋ	CH
⊥	_|_
+ℋ	+H
span	span
∨ℋ	vH
∨ℋ	\/H
0ℋ	0H
Cℋ	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
Mℋ	MH
Mℋ*	MH*
GrpHom	GrpHom
GrpIso	GrpIso
SymGrp	SymGrp
gcd	gcd
l	l
fi	fi
EucTop	EucTop
Homeo	Homeo
~=	~=
subSp	subSp
Fil	Fil
fLim	fLim
T0	T0
T1	T1
Con	Con
Dgra	Dgra
Alg	Alg
dom	dom_
cod	cod_
id	id_
o	o_
Ded	Ded
Cat	Cat
hom	hom
Epi	Epi
Monic	Monic
Iso	Iso
Func	Func
O1	O1
M1	M1
O2	O2
M2	M2
I1	I1
D1	D1
C1	C1
Ro1	Ro1
I2	I2
D2	D2
C2	C2
Ro2	Ro2
Subcl	Subcl
Tarski	Tarski
HypGrph	HypGrph
PsGrph	PsGrph
SmpGrph	SmpGrph

Copyright terms: Public domain