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

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/ Ⅎ nfOLD [ [ / / ] ] 𝑠 s ∈ e. 𝑓 f 𝑔 g ∃! 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 E _E I _I 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_ ∘𝑓 oF ∘𝑟 oR [⊊] [C.] ω _om 1st 1st 2nd 2nd supp supp tpos tpos curry curry uncurry uncurry Undef Undef wrecs wrecs Smo Smo recs recs rec rec seq𝜔 seqom 1𝑜 1o 2𝑜 2o 3𝑜 3o 4𝑜 4o +𝑜 +o ·𝑜 .o ↑𝑜 ^o Er Er / /. ↑𝑚 ^m ↑pm ^pm X X_ ≈ ~~ ≼ ~<_ ≺ ~< Fin Fin finSupp finSupp fi fi sup sup inf inf OrdIso OrdIso har har ≼* ~<_* CNF CNF TC TC 𝑅1 R1 rank rank card card ℵ aleph cf cf AC AC_ CHOICE CHOICE +𝑐 +c 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 = ℚ QQ ℝ+ RR+ -𝑒 -e +𝑒 +e ·e *e (,) (,) (,] (,] [,) [,) [,] [,] ... ... ..^ ..^ ⌊ |_ ⌈ |^ mod mod ≡ == seq seq ↑ ^ ! ! C _C # # Word Word lastS lastS ++ ++ ⟨“ <" ”⟩ "> substr substr splice splice reverse reverse repeatS repeatS cyclShift cyclShift 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 ∥ || 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 ndx ndx sSet sSet Slot Slot 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 Preset Preset Dirset Dirset Poset Poset lt lt lub lub glb glb join join meet meet Toset Toset 1. 1. 0. 0. Lat Lat CLat CLat ODual ODual toInc toInc DLat DLat PosetRel PosetRel TosetRel TosetRel DirRel DirRel tail tail +𝑓 +f Mgm Mgm SGrp SGrp Mnd Mnd MndHom MndHom SubMnd SubMnd freeMnd freeMnd varFMnd varFMnd 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 mulGrp mulGrp 1r 1r SRing SRing Ring Ring CRing CRing oppr oppR ∥r ||r Unit Unit Irred Irred invr invr /r /r RingHom RingHom RingIso RingIso ≃𝑟 ~=r DivRing DivRing Field Field SubRing SubRing RingSpan RingSpan 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 AssAlg AssAlg AlgSpan AlgSpan algSc algSc mPwSer mPwSer mVar mVar mPoly mPoly 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ℂHil toCHil 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 Cn 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 ConnGraph ConnGraph EulerPaths EulerPaths FriendGraph FriendGraph Plig Plig RPrime RPrime 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 ⋖ℋ g ↔𝑔 <->g ∨𝑔 \/g ∃𝑔 E.g Fmla Fmla Sat Sat Sat∈ SatE ⊧ |= 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 QpOLD QpOLD Zp Zp _Qp _Qp Cp Cp TrPred TrPred wsuc wsuc wsucOLD wsucOLD WLim WLim WLimOLD WLimOLD No No > ×× 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 [ [b / /b ]b ]b sngl sngl tag tag Proj Proj ⦅ (| , ,, ⦆ |) pr1 pr1 pr2 pr2 Moore Moore_ Set⟶ -Set-> curry_ curry_ uncurry_ uncurry_ ℝ≥0 RR>=0 ℝ>0 RR>0 Diag Diag inftyexpi inftyexpi ℂ∞ CCinfty ℂ̅ CCbar +∞ pinfty -∞ minfty ℝ̅ RRbar ∞ infty ℂ̂ CChat ℝ̂ RRhat +ℂ̅ +cc -ℂ̅ -cc prcpal prcpal Arg Arg ·ℂ̅ .cc -1ℂ̅ invc FinSum FinSum ℝ-Vec RRVec τ _tau ↑↑ ^^ ∈ wl-el ∈ wl-el2 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 Prt Prt LSAtoms LSAtoms LSHyp LSHyp ⋖L
. → ->.. , ,. 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 defAt defAt ''' ''' (( (( )) )) RePart RePart prefix prefix FermatNo FermatNo Even Even Odd Odd GoldbachEven GoldbachEven GoldbachOdd GoldbachOdd GoldbachOddALTV GoldbachOddALTV UPWalks UPWalks Pairs Pairs 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 setrecs setrecs Pg Pg ≥ >_ > > sinh sinh cosh cosh tanh tanh sec sec csc csc cot cot _ _ . . log_ log_ Reflexive Reflexive Irreflexive Irreflexive ∀! A!
 Copyright terms: Public domain W3C validator