@@ -136,6 +136,7 @@ $s class (/) $: <mi href="df-nul.html">∅</mi> $. $( ∅ or ∅ lo
136
136
$s class Undef $: <mi href="df-undef.html">Undef</mi> $.
137
137
$s class _E $: <mi href="df-eprel.html" mathvariant="normal">E</mi> $.
138
138
$s class _I $: <mi href="df-id.html" mathvariant="normal">I</mi> $.
139
+ $s class _S $: <mi href="df-ssr.html" mathvariant="normal">S</mi> $.
139
140
$s class O(1) $: <mrow href="df-o1.html"><mo>𝑂</mo><mo>⁡</mo><mfenced><mn>1</mn></mfenced></mrow> $.
140
141
$s class <_O(1) $: <mrow href="df-lo1.html"><mo>≤</mo><mo>𝑂</mo><mo>⁡</mo><mfenced><mn>1</mn></mfenced></mrow> $.
141
142
$s class odZ $: <msub href="df-odz.html"><mi>od</mi><mi>ℤ</mi></msub> $.
@@ -359,6 +360,11 @@ $s class AFS $: <mo href="df-afs.html">AFS</mo> $.
359
360
$s class Ismt $: <mo href="df-ismt.html">Ismt</mo> $.
360
361
$s class hpG $: <msub href="df-hpg.html"><mo>hp</mo> <mo>𝒢</mo></msub> $.
361
362
363
+ $( Spheres and lines in real Euclidean spaces $)
364
+
365
+ $s class LineM $: <msub href="df-line.html"><mo>Line</mo> <mo>M</mo></msub> $.
366
+ $s class Sphere $: <mo href="df-sph.html">Sphere</mo> $.
367
+
362
368
363
369
$( Commented out in set.mm
364
370
@@ -401,6 +407,7 @@ $s class ++ $: <mi href="df-concat.html"> ++ </mi> $.
401
407
$s class substr $: <mi href="df-substr.html"> substr </mi> $.
402
408
$s class splice $: <mi href="df-splice.html"> splice </mi> $.
403
409
$s class reverse $: <mi href="df-reverse.html">reverse</mi> $.
410
+ $s class leftpad $: <mi href="df-leftpad.html">leftpad</mi> $.
404
411
$s class shift $: <mi href="df-shft.html">shift</mi> $.
405
412
$s class Re $: <mi href="df-re.html">ℜ</mi> $.
406
413
$s class Im $: <mi href="df-im.html">ℑ</mi> $.
@@ -462,7 +469,7 @@ $s class FuncCat $: <mi href="df-fuc.html">FuncCat</mi> $.
462
469
$s class Arrow $: <mi href="df-arw.html">Arrow</mi> $.
463
470
$s class SetCat $: <mi href="df-setc.html">SetCat</mi> $.
464
471
$s class CatCat $: <mi href="df-catc.html">CatCat</mi> $.
465
- $s class Preset $: <mi href="df-preset .html"> Preset </mi> $.
472
+ $s class Proset $: <mi href="df-proset .html"> Proset </mi> $.
466
473
$s class Dirset $: <mi href="df-drs.html">Dirset</mi> $.
467
474
$s class Poset $: <mi href="df-poset.html">Poset</mi> $.
468
475
$s class lt $: <mi href="df-plt.html">lt</mi> $.
@@ -562,7 +569,7 @@ $s class MetOpen $: <mi href="df-mopn.html">MetOpen</mi> $.
562
569
$s class chr $: <mi href="df-chr.html">chr</mi> $.
563
570
$s class PreHil $: <mi href="df-phl.html">PreHil</mi> $.
564
571
$s class ocv $: <mi href="df-ocv.html">ocv</mi> $.
565
- $s class CSubSp $: <mi href="df-cs .html">CSubSp </mi> $.
572
+ $s class ClSubSp $: <mi href="df-css .html">ClSubSp </mi> $.
566
573
$s class toHL $: <mi href="df-thl.html">toHL</mi> $.
567
574
$s class proj $: <mi href="df-pj.html">proj</mi> $.
568
575
$s class Hil $: <mi href="df-hil.html">Hil</mi> $.
@@ -624,7 +631,7 @@ $s class Htpy $: <mi href="df-htpy.html"> Htpy </mi> $.
624
631
$s class PHtpy $: <mi href="df-phtpy.html">PHtpy</mi> $.
625
632
$s class CMod $: <mi href="df-clm.html">CMod</mi> $.
626
633
$s class CPreHil $: <mi href="df-cph.html">CPreHil</mi> $.
627
- $s class toCHil $: <mi href="df-tch .html">toCHil </mi> $.
634
+ $s class toCPreHil $: <mi href="df-tcph .html">toCPreHil </mi> $.
628
635
$s class CauFil $: <mi href="df-cfil.html">CauFil</mi> $.
629
636
$s class CauFilU $: <mi href="df-cfilu.html">CauFilU</mi> $.
630
637
$s class Cau $: <mi href="df-cau.html">Cau</mi> $.
@@ -846,6 +853,14 @@ $( Number Theory $)
846
853
$s class repr $: <mi href="df-repr.html">repr</mi> $.
847
854
$s class vts $: <mi href="df-vts.html">vts</mi> $.
848
855
856
+ $( Algebra $)
857
+ $s class toCyc $: <mi href="df-tocyc.html">toCyc</mi> $.
858
+ $s class dim $: <mi href="df-dim.html">dim</mi> $.
859
+ $s class /FldExt $: <msub href="df-fldext.html"><mo>/</mo><mi>FldExt</mi></msub> $.
860
+ $s class /FinExt $: <msub href="df-finext.html"><mo>/</mo><mi>FinExt</mi></msub> $.
861
+ $s class /AlgExt $: <msub href="df-algext.html"><mo>/</mo><mi>AlgExt</mi></msub> $.
862
+ $s class ( O [:] P ) $: <mfenced open='[' close=']'><mrow> #O# : #P# </mrow></mfenced> $.
863
+ $s class [:] $: <mfenced open='[' close=']' href="df-extdg.html"><mrow><mi>.</mi><mo>:</mo><mi>.</mi></mrow></mfenced> $.
849
864
850
865
$( Measure Theory $)
851
866
$s class sigAlgebra $: <mi href="df-siga.html">sigAlgebra</mi> $.
@@ -886,7 +901,6 @@ $s class GF $: <mi href="df-gf.html"> GF </mi> $.
886
901
$s class ~Qp $: <msub href="df-eqp.html"><mo>~</mo><msub><mi>ℚ</mi><mi>p</mi></msub></msub> $.
887
902
$s class /Qp $: <msub href="df-rqp.html"><mo>/</mo><msub><mi>ℚ</mi><mi>p</mi></msub></msub> $.
888
903
$s class Qp $: <msub href="df-qp.html"><mi>ℚ</mi><mi>p</mi></msub> $.
889
- $s class QpOLD $: <msub href="df-qpOLD.html"><mi>ℚOLD</mi><mi>p</mi></msub> $.
890
904
$s class Zp $: <msub href="df-zp.html"><mi>ℤ</mi><mi>p</mi></msub> $.
891
905
$s class _Qp $: <mover href="df-qpa.html"><msub><mi>ℚ</mi><mi>p</mi></msub> <mo>‾</mo></mover> $.
892
906
$s class Cp $: <msub href="df-cp.html"><mi>ℂ</mi><mi>p</mi></msub> $.
@@ -909,6 +923,7 @@ $s class Edg $: <mi href="df-edg.html"> Edg </mi> $.
909
923
$s class UPGraph $: <mi href="df-upgr.html"> UPGraph </mi> $.
910
924
$s class USPGraph $: <mi href="df-ushgr.html"> USHGraph </mi> $.
911
925
$s class FinUSGraph $: <mi href="df-fusg.html"> FinUSGraph </mi> $.
926
+ $s class AcyclicGraph $: <mi href="df-acycgr.html"> AcyclicGraph </mi> $.
912
927
$s class EulerPaths $: <mi href="df-eupth.html"> EulerPaths </mi> $.
913
928
$s class VtxDeg $: <mi href="df-vtxdg.html"> VtxDeg </mi> $.
914
929
$s class Walks $: <mi href="df-wlk.html">Walks</mi> $.
@@ -931,6 +946,7 @@ $s class RegUSGraph $: <mi href="df-rusgr.html">RegUSGraph</mi> $.
931
946
$s class ClWalks $: <mi href="df-clwlk.html">ClWalks</mi> $.
932
947
$s class ClWWalks $: <mi href="df-clwwlk.html">ClWWalks</mi> $.
933
948
$s class ClWWalksN $: <mi href="df-clwwlkn.html">ClWWalksN</mi> $.
949
+ $s class ClWWalksNOn $: <mi href="df-clwwlknon.html">ClWWalksNOn</mi> $.
934
950
935
951
$s class seqstr $: <msub href="df-sseq.html"><mi>seq</mi> <mo>str</mo></msub> $.
936
952
$s class Fibci $: <mi href="df-fibci.html">Fibci</mi> $.
@@ -949,9 +965,11 @@ $s class ( A ^^ B ) $: <mrow> #A# <mo href="df-finxp.html">↑↑</mo> #B#
949
965
950
966
951
967
$( Wolf Lammen $)
952
- $s wff x wl-el A $: <mrow> #A# <mo href="ax-wl-8cl.html">∈</mo> #B# </mrow> $.
953
- $s wff x wl-el2 A $: <mrow> #A# <mo href="df-wl-clelv2.html">∈</mo> #B# </mrow> $.
954
-
968
+ $s wff A. ( x wl-in A ) ph $: <mrow> <mo href="wl-ral.html">∀</mo> #x# <mo href="df-ral.html">:</mo> #A# <mspace width=.4em /> #ph# </mrow> $.
969
+ $s wff E. ( x wl-in A ) ph $: <mrow> <mo href="wl-rex.html">∃</mo> #x# <mo href="df-rex.html">:</mo> #A# <mspace width=.4em /> #ph# </mrow> $.
970
+ $s wff E! ( x wl-in A ) ph $: <mrow> <mo href="wl-reu.html">∃!</mo> #x# <mo href="df-reu.html">:</mo> #A# <mspace width=.4em /> #ph# </mrow> $.
971
+ $s wff E* ( x wl-in A ) ph $: <mrow> <msup href="wl-rmo.html"><mo>∃</mo><mo>*</mo></msup> #x# <mo href="df-rmo.html">:</mo> #A# #ph# </mrow> $.
972
+ $s class { x wl-in A | ph } $: <mfenced open="{" close="}"> <mrow>#x# <mo href="wl-crab.html">:</mo> #A# <mo lspace=.3em rspace=.3em>|</mo> #ph# </mrow></mfenced> $.
955
973
956
974
$( Removed as part of FL'mathbox
957
975
@@ -1338,7 +1356,9 @@ $( Alexander van der Vekens $)
1338
1356
$s class e// $: <mi href="df-nelbr">∉</mi> $.
1339
1357
$s class ~=c $: <msub href="df-cic.html"><mo>≃</mo> <mi>𝑐</mi></msub> $.
1340
1358
$s wff F defAt A $: <mrow> #F# <mi href="df-dfat.html">defAt</mi> #A# </mrow> $.
1359
+ $s class ( iota' x ph ) $: <mi href="df-aiota">ι</mi> $.
1341
1360
$s class ( A ''' B ) $: <mfenced><mrow>#A# <mi href="df-afv.html">'''</mi> #B#</mrow></mfenced> $.
1361
+ $s class ( F '''' A ) $: <mfenced><mrow>#F# <mi href="df-afv2.html">''''</mi> #A#</mrow></mfenced> $.
1342
1362
$s class (( A F B )) $: <mfenced open="((" close="))"><mrow>#A# #F# #B#</mrow></mfenced> $.
1343
1363
$s class FriendGraph $: <mi href="df-frgr.html">FriendGraph</mi> $.
1344
1364
$s class Trails $: <mi href="df-trls.html">Trails</mi> $.
@@ -1375,13 +1395,21 @@ $s class GoldbachOddW $: <mi href="df-gbow.html">GoldbachOddW</mi> $.
1375
1395
$s class GoldbachOdd $: <mi href="df-gbo.html">GoldbachOdd</mi> $.
1376
1396
1377
1397
$s class UPWalks $: <mi href="df-upwlks.html">UPWalks</mi> $.
1398
+
1399
+ $s wff [ x <> y ] ph $: <mrow><mfenced open="[" close="]" separators=""> #x# <mo href="df-ich.html">⇄</mo> #y# </mfenced> #ph# </mrow> $.
1400
+
1378
1401
$s class Pairs $: <mi href="df-spr.html">Pairs</mi> $.
1379
1402
1380
1403
$s class /_f $: <msub href="df-fdiv"><mi>/</mi> <mi>f<mi></msub> $.
1381
1404
$s class _O $: <mi href="df-bigo">O</mi> $.
1382
1405
$s class #b $: <msub href="df-blen"><mi>#</mi> <mi>b<mi></msub> $.
1383
1406
$s class digit $: <mi href="df-dig.html">digit</mi> $.
1384
1407
1408
+ $s class PrPairs $: <mi href="df-prpr.html">PrPairs</mi> $.
1409
+ $s class FPPr $: <mi href="df-fppr.html">FPPr</mi> $.
1410
+ $s class GrIsom $: <mi href="df-grisom.html">GrIsom</mi> $.
1411
+ $s class IsomGr $: <mi href="df-isomgr.html">IsomGr</mi> $.
1412
+
1385
1413
$( David A. Wheeler $)
1386
1414
$s class >_ $: <mi href="df-gte.html"> ≥ </mi> $.
1387
1415
$s class > $: <mi href="df-gt.html"> > </mi> $.
@@ -1415,15 +1443,6 @@ $s wff (. ph ,. ps ->. ch ). $: <mfenced mathcolor=#0D0 separators="">#ph# <mo m
1415
1443
$s wff (. ph ,. ps ,. ch ->. th ). $: <mfenced mathcolor=#0D0 separators="">#ph# <mo mathcolor=#0D0>,</mo> #ps# <mo mathcolor=#0D0>,</mo> #ch# <mo mathcolor=#0D0>→</mo> #th#</mfenced> $.
1416
1444
$s wff (. ph ,. ps ). $: <mfenced mathcolor=#0D0>#ph# #ps#</mfenced> $.
1417
1445
$s wff (. ph ,. ps ,. ch ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch#</mfenced> $.
1418
- $s wff (. ph ,. ps ,. ch ,. th ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th#</mfenced> $.
1419
- $s wff (. ph ,. ps ,. ch ,. th ,. ta ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th# #ta#</mfenced> $.
1420
- $s wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th# #ta# #et#</mfenced> $.
1421
- $s wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th# #ta# #et# #ze#</mfenced> $.
1422
- $s wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th# #ta# #et# #ze# #si#</mfenced> $.
1423
- $s wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th# #ta# #et# #ze# #si# #rh#</mfenced> $.
1424
- $s wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ,. mu ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th# #ta# #et# #ze# #si# #rh# #mu#</mfenced> $.
1425
- $s wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ,. mu ,. la ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th# #ta# #et# #ze# #si# #rh# #mu# #la#</mfenced> $.
1426
- $s wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ,. mu ,. la ,. ka ). $: <mfenced mathcolor=#0D0>#ph# #ps# #ch# #th# #ta# #et# #ze# #si# #rh# #mu# #la# #ka#</mfenced> $.
1427
1446
1428
1447
$( Jonathan Ben-Naim's $)
1429
1448
$s class _pred ( X , A , R ) $: <mrow> <mo>pred</mo> <mfenced>#X# #A# #R#</mfenced></mrow> $.
@@ -1448,9 +1467,13 @@ $s class RRbar $: <mover href="df-bj-rrbar.html"><mi>ℝ</mi> <mo>‾</mo
1448
1467
$s class RRhat $: <mover href="df-bj-rrhat.html"><mi>ℝ</mi> <mo>^</mo></mover> $.
1449
1468
$s class CCbar $: <mover href="df-bj-ccbar.html"><mi>ℂ</mi> <mo>‾</mo></mover> $.
1450
1469
$s class CChat $: <mover href="df-bj-cchat.html"><mi>ℂ</mi> <mo>^</mo></mover> $.
1470
+ $s class NNbar $: <mover href="df-bj-nnbar.html"><mi>ℕ</mi> <mo>‾</mo></mover> $.
1471
+ $s class ZZbar $: <mover href="df-bj-zzbar.html"><mi>ℤ</mi> <mo>‾</mo></mover> $.
1472
+ $s class ZZhat $: <mover href="df-bj-zzhat.html"><mi>ℤ</mi> <mo>^</mo></mover> $.
1473
+ $s class ||C $: <msub href="df-bj-divc.html"><mi>∥</mi> <mi>ℂ</mi></msub> $.
1451
1474
$s class CCinfty $: <msub href="df-bj-ccinfty"><mi>ℂ</mi> <mi>∞</mi></msub> $.
1452
1475
$s class infty $: <mi href="df-bj-infty">∞</mi> $.
1453
- $s class prcpal $: <mi href="df-bj-prcpal">prcpal< /mi> $.
1476
+ $s class iomnn $: <msub href="df-bj-iomnn.html"><mi>i< /mi> <mo>ω↪ℕ</mo></msub > $.
1454
1477
$s class Arg $: <mi href="df-bj-arg">Arg</mi> $.
1455
1478
$s class +cc $: <msub href="df-bj-addc.html"><mo>+</mo> <mover><mi>ℂ</mi> <mo>‾</mo></mover></msub> $.
1456
1479
$s class -cc $: <msub href="df-bj-oppc.html"><mo>-</mo> <mover><mi>ℂ</mi> <mo>‾</mo></mover></msub> $.
@@ -1472,17 +1495,63 @@ $s class uncurry_ $: <mi href="df-bj-unc">uncurry_</mi> $.
1472
1495
1473
1496
$s class [s B / A ]s S $: <mrow><mfenced open="[" close="]s" separators="/"> #B# #A# </mfenced> #S# </mrow> $.
1474
1497
1498
+ $s wff E** x ph $: <mrow> <msup href="df-bj-mo.html"><mo>∃</mo><mo>**</mo></msup> #x# <mspace width=.4em /> #ph# </mrow> $.
1499
+ $s wff F// x ph $: <mrow> <mo href="df-bj-nnf.html">Ⅎ'</mo> #x# <mspace width=.4em /> #ph# </mrow> $.
1500
+ $s class {R $: <msub href="df-bj-fractemp.html"><mo>{</mo> <mo>R</mo></msub> $.
1501
+ $s class inftyexpitau $: <msup href="df-bj-inftyexpitau.html"><mi>+∞e</mi> <mo>iτ</mo></msup> $.
1502
+ $s class CCinftyN $: <msub href="df-bj-ccinftyN.html"><mi>ℂ</mi> <mo>∞N</mo></msup> $.
1503
+ $s class 1/2 $: <mfrac href="df-bj-onehalf.html"><mn>1</mn> <mn>2</mn></mfrac> $.
1504
+ $s class <rr $: <msub href=""><mo><</mo> <mi>R</mi></msub> $.
1475
1505
$s wff Prv ph $: <mrow><mo href="ax-prv1.html">Prv</mo> #ph#</mrow> $.
1476
1506
$s wff F/ x e. A ph $: <mrow> <mo href="df-bj-rnf.html">Ⅎ</mo> #x# <mo>∈</mo> #A# <mspace width=.4em /> #ph# </mrow> $.
1477
- $s wff [b x /b y ]b ph $: <mrow><mfenced open="[b" close="]b" separators="/b"> #y# #x# </mfenced> #ph# </mrow> $.
1478
1507
$s wff if- ( ph , ps , ch ) $: <mrow> <mo href="df-bj-if.html">if-</mo> <mfenced>#ph# #ps# #ch#</mfenced></mrow> $.
1479
1508
$s class elwise $: <mi href="df-elwise.html">elwise</mi> $.
1480
1509
$s class ( A Proj B ) $: <mfenced><mrow>#A# <mo href="df-bj-proj.html">Proj</mo> #B#</mrow></mfenced> $.
1481
1510
$s class (| A |) $: <mfenced open="⦅" close="⦆">#A#</mfenced> $.
1482
1511
$s class FinSum $: <mo href="df-bj-finsum.html">FinSum</mo> $.
1483
1512
1513
+ $( Jim Kingdon $)
1514
+ $s class _tau $: <mi href="df-tau.html" mathvariant="normal"> τ </mi> $.
1515
+
1484
1516
$( Peter Mazsa $)
1517
+ $s class ,~ R $: <mrow><mo href="df-coss.html">≀</mo> #R# </mrow> $.
1518
+ $s class ~ A $: <mrow><mo href="df-coss.html">∼</mo> #A# </mrow> $.
1485
1519
$s class ( A |X. B ) $: <mrow> #A# <mo href="df-xrn.html">⋉</mo> #B# </mrow> $.
1520
+ $s class Rels $: <mi href="df-rels.html">Rels</mi> $.
1521
+ $s class Refs $: <mi href="df-refs.html">Refs</mi> $.
1522
+ $s class RefRels $: <mi href="df-refrels.html">RefRels</mi> $.
1523
+ $s wff RefRel R $: <mrow><mo href="df-refrel.html">RefRel</mo> #R#</mrow> $.
1524
+ $s class CnvRefs $: <mi href="df-cnvrefs.html">CnvRefs</mi> $.
1525
+ $s class CnvRefRels $: <mi href="df-cnvrefrels.html">CnvRefRels</mi> $.
1526
+ $s wff CnvRefRel R $: <mrow><mo href="df-cnvrefrel.html">CnvRefRel</mo> #R#</mrow> $.
1527
+ $s class Syms $: <mi href="df-syms.html">Syms</mi> $.
1528
+ $s class SymRels $: <mi href="df-symrels.html">SymRels</mi> $.
1529
+ $s wff SymRel R $: <mrow><mo href="df-symrel.html">SymRel</mo> #R#</mrow> $.
1530
+ $s wff CnvRefRel R $: <mrow><mo href="df-cnvrefrel.html">CnvRefRel</mo> #R#</mrow> $.
1531
+ $s class Trs $: <mi href="df-trs.html">Trs</mi> $.
1532
+ $s class TrRels $: <mi href="df-trsrels.html">TrRels</mi> $.
1533
+ $s wff TrRel R $: <mrow><mo href="df-trrel.html">TrRel</mo> #R#</mrow> $.
1534
+ $s class EqvRels $: <mi href="df-eqvrels.html">EqvRels</mi> $.
1535
+ $s wff EqvRel R $: <mrow><mo href="df-eqvrel.html">EqvRel</mo> #R#</mrow> $.
1536
+ $s class CoElEqvRels $: <mi href="df-coeleqvrels.html">CoElEqvRels</mi> $.
1537
+ $s wff CoElEqvRel R $: <mrow><mo href="df-coeleqvrel.html">CoElEqvRel</mo> #R#</mrow> $.
1538
+ $s class Redunds $: <mi href="df-redunds.html">Redunds</mi> $.
1539
+ $s wff A Redund <. B , C >. $: <mrow href="df-redund.html">#A# <mo>Redund</mo> <mfenced open="⟨" close="⟩">#B# #C#</mfenced></mrow> $.
1540
+ $s wff redund ( ph , ps , ch ) $: <mrow href="df-redundp.html"><mo>redund</mo> <mfenced>#ph# #ps# #ch#</mfenced></mrow> $.
1541
+ $s class DomainQss $: <mi href="df-dmqss.html">DomainQss</mi> $.
1542
+ $s wff R DomainQs A $: <mrow href="df-dmqs">#R# <mo>DomainQs</mo> #A#</mrow> $.
1543
+ $s class Ers $: <mi href="df-ers.html">Ers</mi> $.
1544
+ $s wff R ErALTV A $: <mrow>#R# <mo href="df-erALTV.html">ErALTV</mo> #A#</mrow> $.
1545
+ $s class MembErs $: <mi href="df-members.html">MembErs</mi> $.
1546
+ $s wff MembEr A $: <mrow><mo href="df-member.html">MembEr</mo> #A#</mrow> $.
1547
+ $s class Funss $: <mi href="df-funss.html">Funss</mi> $.
1548
+ $s class FunsALTV $: <mi href="df-funsALTV.html">FunsALTV</mi> $.
1549
+ $s wff FunALTV F $: <mrow><mo href="df-funALTV.html">FunALTV</mo> #F#</mrow> $.
1550
+ $s class Disjss $: <mi href="df-disjss.html">Disjss</mi> $.
1551
+ $s class Disjs $: <mi href="df-disjs.html">Disjs</mi> $.
1552
+ $s wff Disj R $: <mrow><mo href="df-disj.html">Disj</mo> #R#</mrow> $.
1553
+ $s class ElDisjs $: <mi href="df-eldisjs.html">ElDisjs</mi> $.
1554
+ $s wff ElDisj A $: <mrow><mo href="df-eldisj.html">ElDisj</mo> #A#</mrow> $.
1486
1555
1487
1556
$( Norm Megill $)
1488
1557
$s class <oL $: <msub href="df-lcv.html"><mo>⋖</mo> <mi>L</mi></msub> $.
@@ -1543,8 +1612,15 @@ $s class HGMap $: <mi href="df-hgmap.html">HGMap</mi> $.
1543
1612
$s class HLHil $: <mi href="df-hlhil.html">HLHil</mi> $.
1544
1613
$s class mapd $: <mi href="df-mapd.html">mapd</mi> $.
1545
1614
1546
- $( Jim Kingdon $)
1547
- $s class _tau $: <mi href="df-tau.html" mathvariant="normal"> τ </mi> $.
1615
+ $( Steven Nguyen $)
1616
+ $s class -R $: <msub href="df-resub.html"><mo>-</mo> <mi>ℝ</mi></msub> $.
1617
+ $s class PrjSp $: <mi href="df-prjsp.html">ℙ𝕣𝕠𝕛</mi> $.
1618
+ $s class PrjSpn $: <msub href="df-prjspn.html"><mi>ℙ𝕣𝕠𝕛</mi> <mi>n</mi></msub> $.
1619
+
1620
+ $( Rohan Ridenour $)
1621
+ $s class Scott A $: <mrow href="df-scott.html"><mo>Scott</mo> #A#</mrow> $.
1622
+ $s class ( F Coll A ) $: <mfenced><mrow>#F# <mo href="df-coll.html">Coll</mo> #A#</mrow></mfenced> $.
1623
+ $s class SimpGrp $: <mi href="df-simpg.html">SimpGrp</mi> $.
1548
1624
1549
1625
$( Schemes with unknown tokens:
1550
1626
$s class ==3 $: <mi> ≡₃ </mi> $.
1613
1689
@s class 9 @: <mn> 9 </mn> @.
1614
1690
$)
1615
1691
1616
- $s class 10 $: <mn href="df-10.html"> 10 </mn> $.
1617
-
1618
1692
$( Arithmetic number builder $)
1619
1693
$i class-n M $: <mi mathcolor=#808>M</mi> $.
1620
1694
$i class-n N $: <mi mathcolor=#808>N</mi> $.
@@ -1658,6 +1732,7 @@ $s wff ( ph /\ ps ) $: <mfenced><mrow> #ph# <mo linebreak=goodbreak lspace=.5em
1658
1732
$s wff ( ph \/ ps ) $: <mfenced><mrow> #ph# <mo linebreak=goodbreak lspace=.5em rspace=.5em href="df-or.html">∨</mo> #ps# </mrow></mfenced> $.
1659
1733
$s wff ( ph -/\ ps ) $: <mfenced><mrow> #ph# <mo linebreak=goodbreak lspace=.5em rspace=.5em href="df-nan.html">⊼</mo> #ps# </mrow></mfenced> $.
1660
1734
$s wff ( ph \/_ ps ) $: <mfenced><mrow> #ph# <mo linebreak=goodbreak lspace=.5em rspace=.5em href="df-xor.html">⊻</mo> #ps# </mrow></mfenced> $.
1735
+ $s wff ( ph -\/ ps ) $: <mfenced><mrow> #ph# <mo linebreak=goodbreak lspace=.5em rspace=.5em href="df-nor.html">⊽</mo> #ps# </mrow></mfenced> $.
1661
1736
1662
1737
$( Quantifiers $)
1663
1738
$s wff A. x e. A ph $: <mrow> <mo href="df-ral.html">∀</mo> #x# <mo href="df-ral.html">∈</mo> #A# <mspace width=.4em /> #ph# </mrow> $.
@@ -1670,8 +1745,8 @@ $s wff E! x ph $: <mrow> <mo href="df-eu.html">∃!</mo> #x# <mspace width=.
1670
1745
$s wff E* x ph $: <mrow> <msup href="df-mo.html"><mo>∃</mo><mo>*</mo></msup> #x# <mspace width=.4em /> #ph# </mrow> $.
1671
1746
$s wff F/ x ph $: <mrow> <mo href="df-nf.html">Ⅎ</mo> #x# <mspace width=.4em /> #ph# </mrow> $.
1672
1747
$s wff F/_ x A $: <mrow> <munder><mo href="df-nfc.html"> Ⅎ </mo><mo> _ </mo></munder> #x# <mspace width=.4em /> #A# </mrow> $.
1673
- $s wff nfOLD x ph $: <mrow> <mo href="df-nfOLD.html">ℲOLD</mo> #x# <mspace width=.4em /> #ph# </mrow> $.
1674
1748
1749
+ $s wff E! x e. A , y e. B ph $: <mrow> <mo href="df-2reu.html">∃!</mo> #x# <mo href="df-reu.html">∈</mo> #A#, #y# <mo href="df-2reu.html">∈</mo> #B# <mspace width=.4em /> #ph# </mrow> $.
1675
1750
1676
1751
1677
1752
@@ -1977,7 +2052,9 @@ $s class S.2 $: <msup href="df-itg2.html"><mo>∫</mo> <mn>2</mn></msup> $.
1977
2052
$s class area $: <mo href="df-area.html">area</mo> $.
1978
2053
1979
2054
$( Operator Constants - usually not used outside definition $)
1980
- $s class +c $: <msub href="df-cda.html"> <mo>+</mo> <mo>c</mo> </msub> $.
2055
+ $s class ( A |_| B ) $: <mfenced><mrow>#A# <mi href="df-dju"> ⊔︀ </mi> #B#</mrow></mfenced> $.
2056
+ $s class inl $: <mo href="df-inl.html">inl</mo> $.
2057
+ $s class inr $: <mo href="df-inr.html">inr</mo> $.
1981
2058
$s class + $: <mo href="df-add.html">+</mo> $.
1982
2059
$s class - $: <mo href="df-sub.html">−</mo> $.
1983
2060
$s class / $: <mo href="df-div.html">÷</mo> $.
0 commit comments