Metamath Proof Explorer This is the GIF version. Change to Unicode version

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

 Symbol ASCII ( ) -> -. wff |- ph ps ch th ta et ze si rh mu la ka <-> \/ /\ -/\ \/_ T. F. hadd hadd cadd cadd , A. set x y z w v u t E. F/ class = A B [ / ] e. f g E! E* { | } ./\ .\/ .<_ .< .+ .- .X. ./ .^ .0. .1. .|| .~ ._|_ .+^ .+b .(+) .* .x. .xb ., .(x) .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 s r q p a b c d l F/_ =/= e/ _V CondEq CondEq [. ]. [_ ]_ \ u. i^i C_ C. (/) if ~P <. >. U. |^| U_ |^|_ Disj Disj_ |-> Tr _E _I Po Or Fr Se Se We Ord On Lim suc om X. `' dom ran |` " o. Rel iota : Fun Fn --> -1-1-> -onto-> -1-1-onto-> ` Isom oF oR 1st 2nd tpos tpos curry curry uncurry uncurry [] [C.] Undef iota_ Smo recs recs rec seq𝜔 seqom 1o 2o 3o 4o +o .o ^o Er /. ^m ^pm X_ ~~ ~<_ ~< Fin fi sup OrdIso OrdIso har har * ~<_* CNF CNF TC R1 rank card aleph cf AC AC_ CHOICE CHOICE +c FinIa Fin1a FinII Fin2 FinIII Fin3 FinIV Fin4 FinV Fin5 FinVI Fin6 FinVII Fin7 GCH GCH InaccW Inacc WUni WUni wUniCl wUniCl Tarski Univ tarskiMap N. +N .N = QQ RR+ -e +e *e (,) (,] [,) [,] ... ..^ ..^ |_ mod == seq ^ ! _C # Word Word concat concat <" "> substr substr splice splice reverse reverse shift Re Im * sqr abs +- limsup ~~> ~~>r O(1) <_O(1) sum_ exp _e sin cos tan pi || bits bits sadd sadd smul smul gcd Prime numer numer denom denom odZ phi pCnt Z[i] AP AP MonoAP MonoAP PolyAP PolyAP Ramsey Ramsey Struct Struct ndx sSet sSet Slot Slot Base ↾s |`s +g .r *r Scalar Scalar .s .i TopSet TopSet le oc dist UnifSet Hom comp comp ↾t |`t TopOpen topGen Xt_ s Xs_ s ^s ordTop ordTop RR*s 0g g gsum s "s s /s qTop qTop s Xs. Moore Moore mrCls mrCls mrInd mrInd ACS ACS Cat Id f Homf compf comf oppCat oppCat Mono Mono Epi Epi Sect Sect Inv Inv Iso cat C_cat cat |`cat Subcat Subcat Func idfunc idFunc func o.func f |`f Full Full Faith Faith Nat Nat FuncCat FuncCat domA coda codA Nat Arrow Homa HomA Ida IdA compa compA SetCat CatCat CatCat c Xc. F 1stF F 2ndF ⟨,⟩F pairF evalF evalF curryF curryF uncurryF uncurryF Δfunc DiagFunc HomF HomF Yon Yon Preset Dirset Dirset Poset lt lub glb join meet Toset Toset 1. 0. Lat CLat ODual ODual toInc toInc DLat DLat PosetRel TosetRel supw infw LatRel DirRel tail Mnd Grp invg +f -g .g .g MndHom MndHom SubMnd SubMnd freeMnd freeMnd varFMnd varFMnd ~QG ~QG SubGrp SubGrp NrmSGrp NrmSGrp GrpHom GrpIso GrpIso 𝑔 ~=g GrpAct SymGrp Cntr Cntr Cntz Cntz oppg oppG od gEx gEx pGrp pGrp pSyl pSyl LSSum proj1 ~FG ~FG freeGrp freeGrp varFGrp varFGrp CMnd CMnd Abel CycGrp CycGrp DProd DProd dProj dProj mulGrp mulGrp Ring CRing 1r oppr oppR r ||r Unit Unit Irred Irred invr /r /r RingHom RingHom RingIso RingIso DivRing Field Field SubRing SubRing RingSpan RingSpan AbsVal AbsVal *Ring *rf LMod .sf LSubSp LSpan LMHom LMHom LMIso LMIso 𝑚 ~=m LBasis LBasis 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 AssAlg AssAlg AlgSpan AlgSpan algSc algSc mPwSer mPwSer mVar mVar mPoly mPoly evalSub evalSub eval eval mHomP mHomP mPSDer mPSDer bag t Kol2 Fre Haus Reg Nrm CNrm CNrm PNrm PNrm Comp Con 1stc 2ndc Locally Locally 𝑛Locally N-Locally 𝑘Gen kGen tX ^ko KQ KQ Homeo ~= Fil UFil UFL UFL FilMap fLimf fLim fClus fClusf CnExt CnExt TopMnd TopMnd TopGrp tsums tsums TopRing TopDRing TopDRing TopMod TopMod TopVec UnifOn UnifOn unifTop unifTop UnifSt UnifSt UnifSp UnifSp toUnifSp toUnifSp Cnu uCn CauFilu CauFilU CUnifSp CUnifSp *MetSp MetSp toMetSp toMetSp norm NrmGrp NrmGrp toNrmGrp toNrmGrp NrmRing NrmRing NrmMod NrmMod NrmVec NrmVec normOp NGHom NGHom NMHom NMHom II -cn-> Htpy Htpy PHtpy ~=ph *p Om1 OmN pi1 piN CMod CMod CPreHil toCHil toCHil CauFil CauFil Cau CMet CMetSp CMetSp Ban Ban CHil vol* vol MblFn MblFn L^1 S.1 S.2 S. _ S_ _d 0p lim limCC _D Dn C^n mDeg mDeg deg1 deg1 Monic1p Monic1p Unic1p Unic1p quot1p quot1p rem1p rem1p idlGen1p idlGen1p Poly Poly Xp coeff coeff deg deg quot quot AA Tayl Tayl Ana Ana ~~>u log ^c arcsin arcsin arccos arccos arctan arctan area area gamma theta Λ Lam ψ psi π ppi mmu sigma DChr DChr /L UHGrph UHGrph UMGrph UMGrph USLGrph USLGrph USGrph USGrph Neighbors Neighbors ComplUSGrph ComplUSGrph UnivVertex UnivVertex Walks Walks Trails Trails Paths Paths SPaths SPaths WalkOn WalkOn TrailOn TrailOn PathOn PathOn Circuits Circuits Cycles Cycles ConnGrph ConnGrph VDeg VDeg EulPaths EulPaths Plig RPrime RPrime t+ t* GrpOp GId GId inv /g ^g AbelOp SubGrpOp Ass ExId Magma SemiGrp MndOp MndOp GrpOpHom GrpOpHom GrpOpIso RingOps DivRingOps *-Fld Com2 Fld CVecOLD NrmCVec +v BaseSet .sOLD 0vec -v CV normCV IndMet .iOLD SubSp LnOp normOpOLD BLnOp 0op adj HmOp CPreHilOLD CBan CHilOLD ~H +h .h 0h -h .ih normh Cauchy ~~>v SH CH _|_ +H span vH \/H 0H C_H projh 0hop Iop +op .op -op +fn .fn normop ConOp LinOp BndLinOp UniOp HrmOp normfn null ConFn LinFn adjh bra ketbra <_op eigvec eigval Lambda States CHStates HAtoms HAtoms g <->g \/g E.g Fmla Sat SatE |= AxExt AxRep AxPow AxUn AxReg AxInf ZF 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 ^r rec t*rec prod_ FallFac FallFac RiseFac RiseFac Pred TrPred No > XX. EE Btwn Cgr Cgr OuterFiveSeg TransportTo TransportTo InnerFiveSeg Cgr3 Cgr3 Colinear FiveSeg Seg<_ OutsideOf OutsideOf Line Line LinesEE LinesEE Ray Ray BernPoly BernPoly Hf Hf gcdOLD Fne Ref PtFin LocFin TotBnd Bnd Ismty Rn RngHom RngIso ~=r CRingOps CRingOps Idl PrIdl MaxIdl PrRing Dmn IdlGen Prt 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 m (+)m freeLMod freeLMod unitVec unitVec LIndF LIndF LIndS LIndS LNoeR LNoeR ldgIdlSeq ldgIdlSeq Monic Poly< Poly< degAA degAA minPolyAA minPolyAA ℤ _ZZ IntgOver IntgOver pmTrsp pmTrsp pmSgn pmSgn maMul maMul Mat Mat maDet maDet maAdju maAdju MEndo MEndo SubDRing SubDRing CytP CytP TopSep TopSep TopLnd TopLnd +r -r .v PtDf RR3 line3 jph jph jps jps jch jch jth jth jta jta jet jet jze jze jps jsi jrh jrh jmu jmu jla jla defAt defAt ''' ''' (( (( )) )) FriendGrph FriendGrph >_ > sinh sinh cosh cosh tanh tanh sec csc cot _ _ . sgn sgn ⌈ ceiling log_ log_ (. ). ->. ->.. ,. ph' ps' ch' th' ta' et' ze' si' rh' ph" ps" ch" th" ta" et" ze" si" rh" ph0 ps0 ch0_ th0 ta0 et0 ze0 si0 rh0 ph1 ps1 ch1 th1 ta1 et1 ze1 si1 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" a0_ b0_ c0_ d0 e0 f0_ g0 h0 i0 j0 k0 l0 m0 n0_ o0_ p0 q0 r0 s0 t0 u0 v0 w0 x0 y0 z0 a1_ b1_ c1_ d1 e1 f1 g1 h1 i1 j1 k1 l1 m1 n1 o1_ p1 q1 r1 s1 t1 u1 v1 w1 x1 y1 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" A0 B0 C0 D0 E0 F0 G0 H0 I0 J0 K0 L0 M0 N0 O0 P0 Q0 R0 S0 T0 U0 V0 W0 X0 Y0 Z0 A1_ B1_ C1_ D1_ E1 F1_ G1_ H1_ I1_ J1 K1 L1_ M1_ N1 O1_ P1 Q1 R1_ S1_ T1 U1 V1_ W1 X1 Y1 Z1 _pred _Se _FrSe _trCl _TrFo LSAtoms LSAtoms LSHyp LSHyp L
 Copyright terms: Public domain W3C validator