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
𝜓	ps
𝜒	ch
𝜃	th
𝜏	ta
𝜂	et
𝜁	ze
𝜎	si
𝜌	rh
𝜇	mu
𝜆	la
𝜅	ka
↔	<->
∧	/\
∨	\/
,	,
if-	if-
⊼	-/\
⊻	\/_
⊽	-\/
∀	A.
setvar	setvar
𝑥	x
class	class
=	=
𝐴	A
𝐵	B
⊤	T.
𝑦	y
⊥	F.
hadd	hadd
cadd	cadd
𝑧	z
𝑤	w
𝑣	v
𝑢	u
𝑡	t
∃	E.
Ⅎ	F/
𝑓	f
𝑔	g
𝑠	s
[	[
/	/
]	]
∈	e.
∃*	E*
∃!	E!
{	{
∣	|
}	}
∧	./\
∨	.\/
≤	.<_
<	.<
+	.+
−	.-
×	.X.
/	./
↑	.^
0	.0.
1	.1.
∥	.||
∼	.~
⊥	._|_
⨣	.+^
✚	.+b
⊕	.(+)
∗	.*
·	.x.
∙	.xb
,	.,
⊗	.(x)
⚬	.o.
𝟎	.0b
𝐶	C
𝐷	D
𝑃	P
𝑄	Q
𝑅	R
𝑆	S
𝑇	T
𝑈	U
𝑒	e
ℎ	h
𝑖	i
𝑗	j
𝑘	k
𝑚	m
𝑛	n
𝑜	o
𝐸	E
𝐹	F
𝐺	G
𝐻	H
𝐼	I
𝐽	J
𝐾	K
𝐿	L
𝑀	M
𝑁	N
𝑉	V
𝑊	W
𝑋	X
𝑌	Y
𝑍	Z
𝑂	O
𝑟	r
𝑞	q
𝑝	p
𝑎	a
𝑏	b
𝑐	c
𝑑	d
𝑙	l
Ⅎ	F/_
≠	=/=
∉	e/
V	_V
CondEq	CondEq
[	[.
]	].
⦋	[_
⦌	]_
∖	\
∪	u.
∩	i^i
⊆	C_
⊊	C.
△	/_\
∅	(/)
if	if
𝒫	~P
⟨	<.
⟩	>.
∪	U.
∩	|^|
∪	U_
∩	|^|_
Disj	Disj_
↦	|->
Tr	Tr
I	_I
E	_E
Po	Po
Or	Or
Fr	Fr
Se	Se
We	We
×	X.
◡	`'
dom	dom
ran	ran
↾	|`
“	"
∘	o.
Rel	Rel
Pred	Pred
Ord	Ord
On	On
Lim	Lim
suc	suc
℩	iota
:	:
Fun	Fun
Fn	Fn
⟶	-->
–1-1→	-1-1->
–onto→	-onto->
–1-1-onto→	-1-1-onto->
‘	`
Isom	Isom
℩	iota_
∘f	oF
∘r	oR
[⊊]	[C.]
ω	_om
1st	1st
2nd	2nd
supp	supp
tpos	tpos
curry	curry
uncurry	uncurry
Undef	Undef
frecs	frecs
wrecs	wrecs
Smo	Smo
recs	recs
rec	rec
seqω	seqom
1o	1o
2o	2o
3o	3o
4o	4o
+o	+o
·o	.o
↑o	^o
Er	Er
/	/.
↑m	^m
↑pm	^pm
X	X_
≈	~~
≼	~<_
≺	~<
Fin	Fin
finSupp	finSupp
fi	fi
sup	sup
inf	inf
OrdIso	OrdIso
har	har
≼*	~<_*
CNF	CNF
TrPred	TrPred
TC	TC
𝑅1	R1
rank	rank
⊔	|_|
inl	inl
inr	inr
card	card
ℵ	aleph
cf	cf
AC	AC_
CHOICE	CHOICE
FinIa	Fin1a
FinII	Fin2
FinIII	Fin3
FinIV	Fin4
FinV	Fin5
FinVI	Fin6
FinVII	Fin7
GCH	GCH
Inaccw	InaccW
Inacc	Inacc
WUni	WUni
wUniCl	wUniCl
Tarski	Tarski
Univ	Univ
tarskiMap	tarskiMap
N	N.
+N	+N
·N	.N
<N	<N
+pQ	+pQ
·pQ	.pQ
<pQ	<pQ
~Q	~Q
Q	Q.
1Q	1Q
[Q]	/Q
+Q	+Q
·Q	.Q
*Q	*Q
<Q	<Q
P	P.
1P	1P
+P	+P.
·P	.P.
<P	<P
~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.
≤	<_
+∞	+oo
-∞	-oo
ℝ*	RR*
<	<
−	-
-	-u
ℕ	NN
2	2
3	3
4	4
5	5
6	6
7	7
8	8
9	9
ℕ0	NN0
ℕ0*	NN0*
ℤ	ZZ
;	;
ℤ≥	ZZ>=
ℚ	QQ
ℝ+	RR+
-𝑒	-e
+𝑒	+e
·e	*e
(,)	(,)
(,]	(,]
[,)	[,)
[,]	[,]
...	...
..^	..^
⌊	|_
⌈	|^
mod	mod
≡	==
seq	seq
↑	^
!	!
C	_C
♯	#
Word	Word
lastS	lastS
++	++
⟨“	<"
”⟩	">
substr	substr
prefix	prefix
splice	splice
reverse	reverse
repeatS	repeatS
cyclShift	cyclShift
cyclShiftOLD	cyclShiftOLD
t+	t+
t*	t*
↑𝑟	^r
t*rec	t*rec
shift	shift
sgn	sgn
ℜ	Re
ℑ	Im
∗	*
√	sqrt
abs	abs
±	+-
lim sup	limsup
⇝	~~>
⇝𝑟	~~>r
𝑂(1)	O(1)
≤𝑂(1)	<_O(1)
Σ	sum_
∏	prod_
FallFac	FallFac
RiseFac	RiseFac
BernPoly	BernPoly
exp	exp
e	_e
sin	sin
cos	cos
tan	tan
π	_pi
τ	_tau
∥	||
bits	bits
sadd	sadd
smul	smul
gcd	gcd
lcm	lcm
lcm	_lcm
ℙ	Prime
numer	numer
denom	denom
odℤ	odZ
ϕ	phi
pCnt	pCnt
ℤ[i]	Z[i]
AP	AP
MonoAP	MonoAP
PolyAP	PolyAP
Ramsey	Ramsey
#p	#p
Struct	Struct
sSet	sSet
Slot	Slot
ndx	ndx
Base	Base
↾s	|`s
+g	+g
.r	.r
*𝑟	*r
Scalar	Scalar
·𝑠	.s
·𝑖	.i
TopSet	TopSet
le	le
oc	oc
dist	dist
UnifSet	UnifSet
Hom	Hom
comp	comp
↾t	|`t
TopOpen	TopOpen
topGen	topGen
∏t	Xt_
0g	0g
Σg	gsum
Xs	Xs_
↑s	^s
ordTop	ordTop
ℝ*𝑠	RR*s
“s	"s
/s	/s
qTop	qTop
×s	Xs.
Moore	Moore
mrCls	mrCls
mrInd	mrInd
ACS	ACS
Cat	Cat
Id	Id
Homf	Homf
compf	comf
oppCat	oppCat
Mono	Mono
Epi	Epi
Sect	Sect
Inv	Inv
Iso	Iso
≃𝑐	~=c
⊆cat	C_cat
↾cat	|`cat
Subcat	Subcat
Func	Func
idfunc	idFunc
∘func	o.func
↾f	|`f
Full	Full
Faith	Faith
Nat	Nat
FuncCat	FuncCat
InitO	InitO
TermO	TermO
ZeroO	ZeroO
doma	domA
coda	codA
Arrow	Arrow
Homa	HomA
Ida	IdA
compa	compA
SetCat	SetCat
CatCat	CatCat
ExtStrCat	ExtStrCat
×c	Xc.
1stF	1stF
2ndF	2ndF
⟨,⟩F	pairF
evalF	evalF
curryF	curryF
uncurryF	uncurryF
Δfunc	DiagFunc
HomF	HomF
Yon	Yon
ODual	ODual
Proset	Proset
Dirset	Dirset
Poset	Poset
lt	lt
lub	lub
glb	glb
join	join
meet	meet
Toset	Toset
1.	1.
0.	0.
Lat	Lat
CLat	CLat
DLat	DLat
toInc	toInc
PosetRel	PosetRel
TosetRel	TosetRel
DirRel	DirRel
tail	tail
+𝑓	+f
Mgm	Mgm
Smgrp	Smgrp
Mnd	Mnd
MndHom	MndHom
SubMnd	SubMnd
freeMnd	freeMnd
varFMnd	varFMnd
EndoFMnd	EndoFMnd
Grp	Grp
invg	invg
-g	-g
.g	.g
~QG	~QG
SubGrp	SubGrp
NrmSGrp	NrmSGrp
GrpHom	GrpHom
GrpIso	GrpIso
≃𝑔	~=g
GrpAct	GrpAct
Cntr	Cntr
Cntz	Cntz
oppg	oppG
SymGrp	SymGrp
pmTrsp	pmTrsp
pmSgn	pmSgn
pmEven	pmEven
od	od
gEx	gEx
pGrp	pGrp
pSyl	pSyl
LSSum	LSSum
proj1	proj1
~FG	~FG
freeGrp	freeGrp
varFGrp	varFGrp
CMnd	CMnd
Abel	Abel
CycGrp	CycGrp
DProd	DProd
dProj	dProj
SimpGrp	SimpGrp
mulGrp	mulGrp
1r	1r
SRing	SRing
Ring	Ring
CRing	CRing
oppr	oppR
∥r	||r
Unit	Unit
Irred	Irred
invr	invr
/r	/r
RPrime	RPrime
RingHom	RingHom
RingIso	RingIso
≃𝑟	~=r
DivRing	DivRing
Field	Field
SubRing	SubRing
RingSpan	RingSpan
SubDRing	SubDRing
AbsVal	AbsVal
*-Ring	*Ring
*rf	*rf
LMod	LMod
·sf	.sf
LSubSp	LSubSp
LSpan	LSpan
LMHom	LMHom
LMIso	LMIso
≃𝑚	~=m
LBasis	LBasis
LVec	LVec
subringAlg	subringAlg
ringLMod	ringLMod
RSpan	RSpan
LIdeal	LIdeal
2Ideal	2Ideal
LPIdeal	LPIdeal
LPIR	LPIR
NzRing	NzRing
RLReg	RLReg
Domn	Domn
IDomn	IDomn
PID	PID
PsMet	PsMet
∞Met	*Met
Met	Met
ball	ball
fBas	fBas
filGen	filGen
MetOpen	MetOpen
metUnif	metUnif
ℂfld	CCfld
ℤring	ZZring
ℤRHom	ZRHom
ℤMod	ZMod
chr	chr
ℤ/nℤ	Z/nZ
ℝfld	RRfld
PreHil	PreHil
·if	.if
ocv	ocv
ClSubSp	ClSubSp
toHL	toHL
proj	proj
Hil	Hil
OBasis	OBasis
⊕m	(+)m
freeLMod	freeLMod
unitVec	unitVec
LIndF	LIndF
LIndS	LIndS
AssAlg	AssAlg
AlgSpan	AlgSpan
algSc	algSc
mPwSer	mPwSer
mVar	mVar
mPoly	mPoly
<bag	<bag
ordPwSer	ordPwSer
evalSub	evalSub
eval	eval
selectVars	selectVars
mHomP	mHomP
mPSDer	mPSDer
AlgInd	AlgInd
PwSer1	PwSer1
var1	var1
Poly1	Poly1
coe1	coe1
toPoly1	toPoly1
evalSub1	evalSub1
eval1	eval1
maMul	maMul
Mat	Mat
DMat	DMat
ScMat	ScMat
maVecMul	maVecMul
matRRep	matRRep
matRepV	matRepV
subMat	subMat
maDet	maDet
maAdju	maAdju
minMatR1	minMatR1
ConstPolyMat	ConstPolyMat
matToPolyMat	matToPolyMat
cPolyMatToMat	cPolyMatToMat
decompPMat	decompPMat
pMatToMatPoly	pMatToMatPoly
CharPlyMat	CharPlyMat
Top	Top
TopOn	TopOn
TopSp	TopSp
TopBases	TopBases
int	int
cls	cls
Clsd	Clsd
nei	nei
limPt	limPt
Perf	Perf
Cn	Cn
CnP	CnP
⇝𝑡	~~>t
Kol2	Kol2
Fre	Fre
Haus	Haus
Reg	Reg
Nrm	Nrm
CNrm	CNrm
PNrm	PNrm
Comp	Comp
Conn	Conn
1stω	1stc
2ndω	2ndc
Locally	Locally
𝑛-Locally	N-Locally
Ref	Ref
PtFin	PtFin
LocFin	LocFin
𝑘Gen	kGen
×t	tX
↑ko	^ko
KQ	KQ
Homeo	Homeo
≃	~=
Fil	Fil
UFil	UFil
UFL	UFL
FilMap	FilMap
fLimf	fLimf
fLim	fLim
fClus	fClus
fClusf	fClusf
CnExt	CnExt
TopMnd	TopMnd
TopGrp	TopGrp
tsums	tsums
TopRing	TopRing
TopDRing	TopDRing
TopMod	TopMod
TopVec	TopVec
UnifOn	UnifOn
unifTop	unifTop
UnifSt	UnifSt
UnifSp	UnifSp
toUnifSp	toUnifSp
Cnu	uCn
CauFilu	CauFilU
CUnifSp	CUnifSp
∞MetSp	*MetSp
MetSp	MetSp
toMetSp	toMetSp
norm	norm
NrmGrp	NrmGrp
toNrmGrp	toNrmGrp
NrmRing	NrmRing
NrmMod	NrmMod
NrmVec	NrmVec
normOp	normOp
NGHom	NGHom
NMHom	NMHom
II	II
–cn→	-cn->
Htpy	Htpy
PHtpy	PHtpy
≃ph	~=ph
*𝑝	*p
Ω1	Om1
Ω𝑛	OmN
π1	pi1
πn	piN
ℂMod	CMod
ℂVec	CVec
ℂPreHil	CPreHil
toℂPreHil	toCPreHil
CauFil	CauFil
Cau	Cau
CMet	CMet
CMetSp	CMetSp
Ban	Ban
ℂHil	CHil
ℝ^	RR^
𝔼hil	EEhil
vol*	vol*
vol	vol
MblFn	MblFn
𝐿1	L^1
∫1	S.1
∫2	S.2
∫	S.
⨜	S_
d	_d
0𝑝	0p
limℂ	limCC
D	_D
D𝑛	Dn
𝓑C𝑛	C^n
mDeg	mDeg
deg1	deg1
Monic1p	Monic1p
Unic1p	Unic1p
quot1p	quot1p
rem1p	rem1p
idlGen1p	idlGen1p
Poly	Poly
Xp	Xp
coeff	coeff
deg	deg
quot	quot
𝔸	AA
Tayl	Tayl
Ana	Ana
⇝𝑢	~~>u
log	log
↑𝑐	^c
logb	logb
arcsin	arcsin
arccos	arccos
arctan	arctan
area	area
γ	gamma
ζ	zeta
Γ	_G
log Γ	log_G
1/Γ	1/_G
θ	theta
Λ	Lam
ψ	psi
π	ppi
μ	mmu
σ	sigma
DChr	DChr
/L	/L
TarskiG	TarskiG
Itv	Itv
LineG	LineG
TarskiGC	TarskiGC
TarskiGB	TarskiGB
TarskiGCB	TarskiGCB
TarskiGE	TarskiGE
DimTarskiG≥	TarskiGDim>=
cgrG	cgrG
Ismt	Ismt
≤G	leG
hlG	hlG
pInvG	pInvG
∟G	raG
⟂G	perpG
hpG	hpG
midG	midG
lInvG	lInvG
cgrA	cgrA
inA	inA
≤∠	leA
eqltrG	eqltrG
toTG	toTG
𝔼	EE
Btwn	Btwn
Cgr	Cgr
EEG	EEG
.ef	.ef
Vtx	Vtx
iEdg	iEdg
Edg	Edg
UHGraph	UHGraph
USHGraph	USHGraph
UPGraph	UPGraph
UMGraph	UMGraph
USPGraph	USPGraph
USGraph	USGraph
SubGraph	SubGraph
FinUSGraph	FinUSGraph
NeighbVtx	NeighbVtx
UnivVtx	UnivVtx
ComplGraph	ComplGraph
ComplUSGraph	ComplUSGraph
VtxDeg	VtxDeg
RegGraph	RegGraph
RegUSGraph	RegUSGraph
EdgWalks	EdgWalks
Walks	Walks
WalksOn	WalksOn
Trails	Trails
TrailsOn	TrailsOn
Paths	Paths
SPaths	SPaths
PathsOn	PathsOn
SPathsOn	SPathsOn
ClWalks	ClWalks
Circuits	Circuits
Cycles	Cycles
WWalks	WWalks
WWalksN	WWalksN
WWalksNOn	WWalksNOn
WSPathsN	WSPathsN
WSPathsNOn	WSPathsNOn
ClWWalks	ClWWalks
ClWWalksN	ClWWalksN
ClWWalksNOn	ClWWalksNOn
ConnGraph	ConnGraph
EulerPaths	EulerPaths
FriendGraph	FriendGraph
Plig	Plig
GrpOp	GrpOp
GId	GId
inv	inv
/𝑔	/g
AbelOp	AbelOp
CVecOLD	CVecOLD
NrmCVec	NrmCVec
+𝑣	+v
BaseSet	BaseSet
·𝑠OLD	.sOLD
0vec	0vec
−𝑣	-v
normCV	normCV
IndMet	IndMet
·𝑖OLD	.iOLD
SubSp	SubSp
LnOp	LnOp
normOpOLD	normOpOLD
BLnOp	BLnOp
0op	0op
adj	adj
HmOp	HmOp
CPreHilOLD	CPreHilOLD
CBan	CBan
CHilOLD	CHilOLD
ℋ	~H
+ℎ	+h
·ℎ	.h
0ℎ	0h
−ℎ	-h
·ih	.ih
normℎ	normh
Cauchy	Cauchy
⇝𝑣	~~>v
Sℋ	SH
Cℋ	CH
⊥	_|_
+ℋ	+H
span	span
∨ℋ	vH
∨ℋ	\/H
0ℋ	0H
𝐶ℋ	C_H
projℎ	projh
0hop	0hop
Iop	Iop
+op	+op
·op	.op
−op	-op
+fn	+fn
·fn	.fn
normop	normop
ContOp	ContOp
LinOp	LinOp
BndLinOp	BndLinOp
UniOp	UniOp
HrmOp	HrmOp
normfn	normfn
null	null
ContFn	ContFn
LinFn	LinFn
adjℎ	adjh
bra	bra
ketbra	ketbra
≤op	<_op
eigvec	eigvec
eigval	eigval
Lambda	Lambda
States	States
CHStates	CHStates
HAtoms	HAtoms
⋖ℋ	<oH
𝑀ℋ	MH
𝑀ℋ*	MH*
class-n	class-n
class-o	class-o
_	_
.	.
/𝑒	/e
Monot	Monot
MGalConn	MGalConn
≲	.c_
oMnd	oMnd
oGrp	oGrp
toCyc	toCyc
sgns	sgns
⋘	<<<
Archi	Archi
SLMod	SLMod
oRing	oRing
oField	oField
↾v	|`v
PrmIdeal	PrmIdeal
MaxIdeal	MaxIdeal
IDLsrg	IDLsrg
Spec	Spec
UFD	UFD
dim	dim
/FldExt	/FldExt
/FinExt	/FinExt
/AlgExt	/AlgExt
[:]	[:]
subMat1	subMat1
litMat	litMat
CovHasRef	CovHasRef
Ldlf	Ldlf
Paracomp	Paracomp
~Met	~Met
pstoMet	pstoMet
HCmp	HCmp
ℚHom	QQHom
ℝHom	RRHom
ℝExt	RRExt
ℝ*Hom	RR*Hom
ManTop	ManTop
𝟭	_Ind
Σ*	sum*
∘f/c	oFC
sigAlgebra	sigAlgebra
sigaGen	sigaGen
𝔅ℝ	BrSiga
×s	sX
measures	measures
δ	Ddelta
a.e.	ae
~ a.e.	~ae
MblFnM	MblFnM
toOMeas	toOMeas
toCaraSiga	toCaraSiga
sitg	sitg
sitm	sitm
itgm	itgm
seqstr	seqstr
Fibci	Fibci
Prob	Prob
cprob	cprob
rRndVar	rRndVar
∘RV/𝑐	oRVC
repr	repr
vts	vts
TarskiG2D	TarskiG2D
AFS	AFS
leftpad	leftpad
𝜑′	ph'
𝜓′	ps'
𝜒′	ch'
𝜃′	th'
𝜏′	ta'
𝜂′	et'
𝜁′	ze'
𝜎′	si'
𝜌′	rh'
𝜑″	ph"
𝜓″	ps"
𝜒″	ch"
𝜃″	th"
𝜏″	ta"
𝜂″	et"
𝜁″	ze"
𝜎″	si"
𝜌″	rh"
𝜑0	ph0
𝜓0	ps0
𝜒0	ch0_
𝜃0	th0
𝜏0	ta0
𝜂0	et0
𝜁0	ze0
𝜎0	si0
𝜌0	rh0
𝜑1	ph1
𝜓1	ps1
𝜒1	ch1
𝜃1	th1
𝜏1	ta1
𝜂1	et1
𝜁1	ze1
𝜎1	si1
𝜌1	rh1
𝑎′	a'
𝑏′	b'
𝑐′	c'
𝑑′	d'
𝑒′	e'
𝑓′	f'
𝑔′	g'
ℎ′	h'
𝑖′	i'
𝑗′	j'
𝑘′	k'
𝑙′	l'
𝑚′	m'
𝑛′	n'
𝑜′	o'_
𝑝′	p'
𝑞′	q'
𝑟′	r'
𝑠′	s'_
𝑡′	t'
𝑢′	u'
𝑣′	v'_
𝑤′	w'
𝑥′	x'
𝑦′	y'
𝑧′	z'
𝑎″	a"
𝑏″	b"
𝑐″	c"
𝑑″	d"
𝑒″	e"
𝑓″	f"
𝑔″	g"
ℎ″	h"
𝑖″	i"
𝑗″	j"
𝑘″	k"
𝑙″	l"
𝑚″	m"
𝑛″	n"
𝑜″	o"_
𝑝″	p"
𝑞″	q"
𝑟″	r"
𝑠″	s"_
𝑡″	t"
𝑢″	u"
𝑣″	v"_
𝑤″	w"
𝑥″	x"
𝑦″	y"
𝑧″	z"
𝑎0	a0_
𝑏0	b0_
𝑐0	c0_
𝑑0	d0
𝑒0	e0
𝑓0	f0_
𝑔0	g0
ℎ0	h0
𝑖0	i0
𝑗0	j0
𝑘0	k0
𝑙0	l0
𝑚0	m0
𝑛0	n0_
𝑜0	o0_
𝑝0	p0
𝑞0	q0
𝑟0	r0
𝑠0	s0
𝑡0	t0
𝑢0	u0
𝑣0	v0
𝑤0	w0
𝑥0	x0
𝑦0	y0
𝑧0	z0
𝑎1	a1_
𝑏1	b1_
𝑐1	c1_
𝑑1	d1
𝑒1	e1
𝑓1	f1
𝑔1	g1
ℎ1	h1
𝑖1	i1
𝑗1	j1
𝑘1	k1
𝑙1	l1
𝑚1	m1
𝑛1	n1
𝑜1	o1_
𝑝1	p1
𝑞1	q1
𝑟1	r1
𝑠1	s1
𝑡1	t1
𝑢1	u1
𝑣1	v1
𝑤1	w1
𝑥1	x1
𝑦1	y1
𝑧1	z1
𝐴′	A'
𝐵′	B'
𝐶′	C'
𝐷′	D'
𝐸′	E'
𝐹′	F'
𝐺′	G'
𝐻′	H'
𝐼′	I'
𝐽′	J'
𝐾′	K'
𝐿′	L'
𝑀′	M'
𝑁′	N'
𝑂′	O'
𝑃′	P'
𝑄′	Q'
𝑅′	R'
𝑆′	S'
𝑇′	T'
𝑈′	U'
𝑉′	V'
𝑊′	W'
𝑋′	X'
𝑌′	Y'
𝑍′	Z'
𝐴″	A"
𝐵″	B"
𝐶″	C"
𝐷″	D"
𝐸″	E"
𝐹″	F"
𝐺″	G"
𝐻″	H"
𝐼″	I"
𝐽″	J"
𝐾″	K"
𝐿″	L"
𝑀″	M"
𝑁″	N"
𝑂″	O"
𝑃″	P"
𝑄″	Q"
𝑅″	R"
𝑆″	S"
𝑇″	T"
𝑈″	U"
𝑉″	V"
𝑊″	W"
𝑋″	X"
𝑌″	Y"
𝑍″	Z"
𝐴0	A0
𝐵0	B0
𝐶0	C0
𝐷0	D0
𝐸0	E0
𝐹0	F0
𝐺0	G0
𝐻0	H0
𝐼0	I0
𝐽0	J0
𝐾0	K0
𝐿0	L0
𝑀0	M0
𝑁0	N0
𝑂0	O0
𝑃0	P0
𝑄0	Q0
𝑅0	R0
𝑆0	S0
𝑇0	T0
𝑈0	U0
𝑉0	V0
𝑊0	W0
𝑋0	X0
𝑌0	Y0
𝑍0	Z0
𝐴1	A1_
𝐵1	B1_
𝐶1	C1_
𝐷1	D1_
𝐸1	E1
𝐹1	F1_
𝐺1	G1_
𝐻1	H1_
𝐼1	I1_
𝐽1	J1
𝐾1	K1
𝐿1	L1_
𝑀1	M1_
𝑁1	N1
𝑂1	O1_
𝑃1	P1
𝑄1	Q1
𝑅1	R1_
𝑆1	S1_
𝑇1	T1
𝑈1	U1
𝑉1	V1_
𝑊1	W1
𝑋1	X1
𝑌1	Y1
𝑍1	Z1
pred	_pred
Se	_Se
FrSe	_FrSe
trCl	_trCl
TrFo	_TrFo
AcyclicGraph	AcyclicGraph
Retr	Retr
PConn	PConn
SConn	SConn
CovMap	CovMap
∈𝑔	e.g
⊼𝑔	|g
∀𝑔	A.g
Fmla	Fmla
Sat	Sat
Sat∈	SatE
⊧	|=
=𝑔	=g
∧𝑔	/\g
¬𝑔	-.g
→𝑔	->g
↔𝑔	<->g
∨𝑔	\/g
∃𝑔	E.g
AxExt	AxExt
AxRep	AxRep
AxPow	AxPow
AxUn	AxUn
AxReg	AxReg
AxInf	AxInf
ZF	ZF
mCN	mCN
mVR	mVR
mType	mType
mTC	mTC
mAx	mAx
mVT	mVT
mREx	mREx
mEx	mEx
mDV	mDV
mVars	mVars
mRSubst	mRSubst
mSubst	mSubst
mVH	mVH
mPreSt	mPreSt
mStRed	mStRed
mStat	mStat
mFS	mFS
mCls	mCls
mPPSt	mPPSt
mThm	mThm
m0St	m0St
mSA	mSA
mWGFS	mWGFS
mSyn	mSyn
mESyn	mESyn
mGFS	mGFS
mTree	mTree
mST	mST
mSAX	mSAX
mUFS	mUFS
mUV	mUV
mVL	mVL
mVSubst	mVSubst
mFresh	mFresh
mFRel	mFRel
mEval	mEval
mMdl	mMdl
mUSyn	mUSyn
mGMdl	mGMdl
mItp	mItp
mFromItp	mFromItp
IntgRing	IntgRing
cplMetSp	cplMetSp
HomLimB	HomLimB
HomLim	HomLim
polyFld	polyFld
splitFld1	splitFld1
splitFld	splitFld
polySplitLim	polySplitLim
ZRing	ZRing
GF	GF
GF∞	GF_oo
~Qp	~Qp
/Qp	/Qp
Qp	Qp
Zp	Zp
_Qp	_Qp
Cp	Cp
𝛻	al
𝑥O	xO
𝑥L	xL
𝑥R	xR
𝑦O	yO
𝑦L	yL
𝑦R	yR
t++	t++
wsuc	wsuc
WLim	WLim
+no	+no
No	No
<s	<s
bday	bday
≤s	<_s
<<s	<<s
|s	|s
0s	0s
1s	1s
M	_M
O	_Old
N	_N
L	_L
R	_R
norec	norec
norec2	norec2
+s	+s
-us	-us
-s	-s
⊗	(x)
Bigcup	Bigcup
SSet	SSet
Trans	Trans
Limits	Limits
Fix	Fix
Funs	Funs
Singleton	Singleton
Singletons	Singletons
Image	Image
Cart	Cart
Img	Img
Domain	Domain
Range	Range
pprod	pprod
Apply	Apply
Cup	Cup
Cap	Cap
Succ	Succ
Funpart	Funpart
FullFun	FullFun
Restrict	Restrict
UB	UB
LB	LB
⟪	<<
⟫	>>
××	XX.
OuterFiveSeg	OuterFiveSeg
TransportTo	TransportTo
InnerFiveSeg	InnerFiveSeg
Cgr3	Cgr3
Colinear	Colinear
FiveSeg	FiveSeg
Seg≤	Seg<_
OutsideOf	OutsideOf
Line	Line
LinesEE	LinesEE
Ray	Ray
△	_/_\
△n	_/_\^n
Hf	Hf
Fne	Fne
gcdOLD	gcdOLD
Prv	Prv
∃**	E**
Ⅎ'	F//
{	{{
}	}}
sngl	sngl
tag	tag
Proj	Proj
⦅	(|
,	,,
⦆	|)
pr1	pr1
pr2	pr2
elwise	elwise
Moore	Moore_
Set⟶	-Set->
Top⟶	-Top->
Mgm⟶	-Mgm->
TopMgm⟶	-TopMgm->
curry_	curry_
uncurry_	uncurry_
[	[s
]struct	]s
ℝ≥0	RR>=0
ℝ>0	RR>0
Id	_Id
𝒫*	~P_*
𝒫*	~P^*
{R	{R
+∞eiτ	inftyexpitau
ℂ∞N	CCinftyN
1/2	1/2
+∞ei	inftyexpi
ℂ∞	CCinfty
ℂ̅	CCbar
+∞	pinfty
-∞	minfty
ℝ̅	RRbar
∞	infty
ℂ̂	CChat
ℝ̂	RRhat
+ℂ̅	+cc
-ℂ̅	-cc
<ℝ̅	<rr
Arg	Arg
·ℂ̅	.cc
-1ℂ̅	invc
iω↪ℕ	iomnn
ℕ̅	NNbar
ℤ̅	ZZbar
ℤ̂	ZZhat
∥ℂ	||C
FinSum	FinSum
ℝ-Vec	RRVec
End	End
↑↑	^^
TotBnd	TotBnd
Bnd	Bnd
Ismty	Ismty
ℝn	Rn
Ass	Ass
ExId	ExId
Magma	Magma
SemiGrp	SemiGrp
MndOp	MndOp
GrpOpHom	GrpOpHom
RingOps	RingOps
DivRingOps	DivRingOps
RngHom	RngHom
RngIso	RngIso
≃𝑟	~=R
Com2	Com2
Fld	Fld
CRingOps	CRingOps
Idl	Idl
PrIdl	PrIdl
MaxIdl	MaxIdl
PrRing	PrRing
Dmn	Dmn
IdlGen	IdlGen
⋉	|X.
≀	,~
∼	~
Rels	Rels
S	_S
Refs	Refs
RefRels	RefRels
RefRel	RefRel
CnvRefs	CnvRefs
CnvRefRels	CnvRefRels
CnvRefRel	CnvRefRel
Syms	Syms
SymRels	SymRels
SymRel	SymRel
Trs	Trs
TrRels	TrRels
TrRel	TrRel
EqvRels	EqvRels
EqvRel	EqvRel
CoElEqvRels	CoElEqvRels
CoElEqvRel	CoElEqvRel
Redunds	Redunds
Redund	Redund
redund	redund
DomainQss	DomainQss
DomainQs	DomainQs
Ers	Ers
ErALTV	ErALTV
MembErs	MembErs
MembEr	MembEr
Funss	Funss
FunsALTV	FunsALTV
FunALTV	FunALTV
Disjss	Disjss
Disjs	Disjs
Disj	Disj
ElDisjs	ElDisjs
ElDisj	ElDisj
Prt	Prt
LSAtoms	LSAtoms
LSHyp	LSHyp
⋖L	<oL
LFnl	LFnl
LKer	LKer
LDual	LDual
OP	OP
cm	cm
OL	OL
OML	OML
⋖	<o
Atoms	Atoms
AtLat	AtLat
CvLat	CvLat
HL	HL
LLines	LLines
LPlanes	LPlanes
LVols	LVols
Lines	Lines
Points	Points
PSubSp	PSubSp
pmap	pmap
+𝑃	+P
PCl	PCl
⊥𝑃	_|_P
PSubCl	PSubCl
LHyp	LHyp
LAut	LAut
WAtoms	WAtoms
PAut	PAut
LDil	LDil
LTrn	LTrn
Dil	Dil
Trn	Trn
trL	trL
TGrp	TGrp
TEndo	TEndo
EDRing	EDRing
EDRingR	EDRingR
DVecA	DVecA
DIsoA	DIsoA
DVecH	DVecH
ocA	ocA
vA	vA
DIsoB	DIsoB
DIsoC	DIsoC
DIsoH	DIsoH
ocH	ocH
joinH	joinH
LPol	LPol
LCDual	LCDual
mapd	mapd
HVMap	HVMap
HDMap1	HDMap1
HDMap	HDMap
HGMap	HGMap
HLHil	HLHil
−ℝ	-R
ℙ𝕣𝕠𝕛	PrjSp
ℙ𝕣𝕠𝕛n	PrjSpn
NoeACS	NoeACS
mzPolyCld	mzPolyCld
mzPoly	mzPoly
Dioph	Dioph
Pell1QR	Pell1QR
Pell14QR	Pell14QR
Pell1234QR	Pell1234QR
PellFund	PellFund
◻NN	[]NN
Xrm	rmX
Yrm	rmY
LFinGen	LFinGen
LNoeM	LNoeM
LNoeR	LNoeR
ldgIdlSeq	ldgIdlSeq
Monic	Monic
Poly<	Poly<
degAA	degAA
minPolyAA	minPolyAA
ℤ	_ZZ
IntgOver	IntgOver
MEndo	MEndo
CytP	CytP
TopSep	TopSep
TopLnd	TopLnd
r*	r*
hereditary	hereditary
MndRing	MndRing
Scott	Scott
Coll	Coll
C𝑐	_Cc
+𝑟	+r
-𝑟	-r
.𝑣	.v
PtDf	PtDf
RR3	RR3
line3	line3
(	(.
)	).
▶	->.
→	->..
,	,.
lim inf	liminf
~~>*	~~>*
SAlg	SAlg
SalOn	SalOn
SalGen	SalGen
Σ^	sum^
Meas	Meas
OutMeas	OutMeas
CaraGen	CaraGen
voln*	voln*
voln	voln
SMblFn	SMblFn
jph	jph
jps	jps
jch	jch
jth	jth
jta	jta
jet	jet
jze	jze
jps	jsi
jrh	jrh
jmu	jmu
jla	jla
℩'	iota'
defAt	defAt
'''	'''
((	((
))	))
''''	''''
_∉	e//
RePart	RePart
⇄	<>
Pairs	Pairs
Pairsproper	PrPairs
FermatNo	FermatNo
Even	Even
Odd	Odd
FPPr	FPPr
GoldbachEven	GoldbachEven
GoldbachOddW	GoldbachOddW
GoldbachOdd	GoldbachOdd
GrIsom	GrIsom
IsomGr	IsomGr
UPWalks	UPWalks
MgmHom	MgmHom
SubMgm	SubMgm
clLaw	clLaw
assLaw	assLaw
comLaw	comLaw
intOp	intOp
clIntOp	clIntOp
assIntOp	assIntOp
MgmALT	MgmALT
CMgmALT	CMgmALT
SGrpALT	SGrpALT
CSGrpALT	CSGrpALT
Rng	Rng
RngHomo	RngHomo
RngIsom	RngIsom
RngCat	RngCat
RngCatALTV	RngCatALTV
RingCat	RingCat
RingCatALTV	RingCatALTV
DMatALT	DMatALT
ScMatALT	ScMatALT
linC	linC
LinCo	LinCo
linIndS	linIndS
linDepS	linDepS
/f	/_f
Ο	_O
#b	#b
digit	digit
-aryF	-aryF
IterComp	IterComp
Ack	Ack
LineM	LineM
Sphere	Sphere
ThinCat	ThinCat
ProsetToCat	ProsetToCat
MndToCat	MndToCat
setrecs	setrecs
Pg	Pg
≥	>_
>	>
sinh	sinh
cosh	cosh
tanh	tanh
sec	sec
csc	csc
cot	cot
log_	log_
Reflexive	Reflexive
Irreflexive	Irreflexive
∀!	A!