TOC of Theorem List - brismu bridi

Home	brismu bridi Theorem List (Table of Contents)	< Wrap Next >
		Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Detailed Table of Contents Page List

Table of Contents Summary PART 1  LOGICAL CONNECTIVES
1.1  Basic syntax
1.2  Implication I: {ganai}
1.3  Conjunctions I: {ge}
1.4  Biconditionals I: {go}
1.5  Implication II
1.6  Conjunctions II
1.7  Disjunctions: {ga}, {.a}, {ja}, {gi'a}
1.8  Biconditionals II
1.9  Conversion I: {se}
1.10  Universal quantifiers I: {ro}
1.11  Identity: {du}
1.12  Boolean predicates: {cei'i}
1.13  Negation I: {gai'o}, {naku}
1.14  Mutual exclusion I
1.15  Extra connectives
PART 2  NON-LOGICAL CONNECTIVES
2.1  Sets I: {nomei}, {pamei}
2.2  Subsets
2.3  Internal hom I
2.4  Conversion II: {te}
2.5  Pairing: {ce}
2.6  Existential quantifiers I: {su'o}
2.7  Not-free quantification
2.8  Substitution I
2.9  Predicate Calculus
2.10  Substitution II
2.11  Sets II: {zilcmi}
2.12  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.13  Internal hom II: {kampu}
2.14  Union: {jo'e}
2.15  Intersection: {ku'a}
2.16  Internal bridi
2.17  Parallel reasoning: {fa'u}
2.18  Deletion: {zi'o}
2.19  Properties of relations
2.20  Existential quantifiers II: {pa da}
2.21  Abstract algebra I: magmas, semigroups, monoids
PART 3  NUMBERS
3.1  Natural numbers
3.2  Exponents I: {tenfa}
3.3  Logarithms: {dugri}
3.4  Cardinality
PART 4  MEREOLOGY
4.1  Parthood
PART 5  SPACE & SPACETIME
5.1  Two-dimensional Euclidean space
5.2  Three-dimensional Euclidean space
5.3  Minkowski spacetime
PART 6  RELATIONAL LOGIC
6.1  Lattice of relations
6.2  Fractions
6.3  Complex numbers
6.4  Functions I
6.5  Assorted claims
6.6  Ontological classes
6.7  Generated baseline ontology

Detailed Table of Contents
(* means the section header has a description) *PART 1  LOGICAL CONNECTIVES
*1.1  Basic syntax
*1.2  Implication I: {ganai}
1.3  Conjunctions I: {ge}
1.4  Biconditionals I: {go}
*1.5  Implication II
1.5.1  {na.a} sjnaa 109
1.5.2  {.anai} sjanai 115
1.5.3  {naja} sbnaja 120
1.5.4  {janai} sbjanai 126
1.5.5  {nagi'a} tnagiha 131
1.5.6  {gi'anai} tgihanai 136
1.6  Conjunctions II
1.6.1  More facts about {ge} ge-com-lem 141
1.6.2  {.e} sje 146
1.6.3  {je} sbje 151
1.6.4  {gi'e} tgihe 155
*1.7  Disjunctions: {ga}, {.a}, {ja}, {gi'a}
1.7.1  {ga} bga 160
1.7.2  {.a} sja 183
1.7.3  {ja} sbja 189
1.7.4  {gi'a} tgiha 193
1.8  Biconditionals II
1.8.1  {.o} sjo 197
1.8.2  {jo} sbjo 204
1.8.3  {gi'o} tgiho 208
1.9  Conversion I: {se}
1.10  Universal quantifiers I: {ro}
1.11  Identity: {du}
1.12  Boolean predicates: {cei'i}
*1.13  Negation I: {gai'o}, {naku}
*1.14  Mutual exclusion I
1.14.1  {gonai} bgon 298
1.14.2  {.onai} sjonai 304
1.14.3  {jonai} sbjonai 308
1.14.4  {gi'onai} tgihonai 312
1.15  Extra connectives
1.15.1  {ginai} bgagin 316
*PART 2  NON-LOGICAL CONNECTIVES
2.1  Sets I: {nomei}, {pamei}
2.1.1  {cmima} sbcmima 320
2.1.2  {nomei} snomei 324
2.1.3  {pamei} sbpamei 327
2.2  Subsets
2.2.1  {gripau} sbgripau 332
*2.3  Internal hom I
2.3.1  {ka} sc 341
2.3.2  {ckaji} sbckaji 343
2.3.3  {ckini} sbckini 348
2.3.4  {sefsi} sbsefsi 354
2.3.5  {simsa} sbsimsa 356
2.3.6  {dunli} sbdunli 365
2.3.7  {mintu} sbmintu 373
2.3.8  {steci} sbsteci 382
2.3.9  {mupli} sbmupli 387
2.3.10  {simxu} sbsimxu 394
2.4  Conversion II: {te}
2.5  Pairing: {ce}
2.6  Existential quantifiers I: {su'o}
2.7  Not-free quantification
2.8  Substitution I
2.9  Predicate Calculus
2.10  Substitution II
2.11  Sets II: {zilcmi}
2.11.1  {zilcmi} sbzilcmi 464
2.12  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.12.1  {po'u} brdpu 481
2.13  Internal hom II: {kampu}
2.13.1  {kampu} sbkampu 483
2.14  Union: {jo'e}
2.14.1  {jo'e} sjohe 487
2.15  Intersection: {ku'a}
2.15.1  {ku'a} skuha 491
*2.16  Internal bridi
2.16.1  {du'u} sdu 495
2.16.2  {bridi} sceho 496
2.16.3  {fatci} sbfatci 506
2.16.4  {nibli} sbnibli 511
2.16.5  {sigda} sbsigda 517
2.16.6  {tsida} sbtsida 519
2.16.7  {kanxe} sbkanxe 521
2.16.8  {vlina} sbvlina 523
2.16.9  {nalti} sbnalti 525
2.17  Parallel reasoning: {fa'u}
2.17.1  {fa'u} sfahu 528
2.18  Deletion: {zi'o}
*2.19  Properties of relations
2.19.1  Transitivity: {takni} sbtakni 539
2.19.2  Symmetry: {kinfi} sbkinfi 542
2.19.3  Reflexivity: {kinra} sbkinra 545
2.19.4  Euclidean: {efklipi}, {efklizu} sbefklipi 551
2.20  Existential quantifiers II: {pa da}
2.20.1  Uniqueness: {pombo} sbpombo 565
2.21  Abstract algebra I: magmas, semigroups, monoids
2.21.1  Magmas: {klojere} sbklojere 569
2.21.2  Semigroups: {kloje} sbkloje 571
2.21.3  Commutative operators: {cajni} sbcajni 573
2.21.4  Monoids: {sezni} sbsezni 575
2.21.5  Groups: {dukni} sbdukni 578
*PART 3  NUMBERS
*3.1  Natural numbers
3.1.1  Zero: {li no} sli 579
3.1.2  Successor I: {bai'ei}, {kacli'e} mbaihei 582
3.1.3  Natural number predicate: {kacna'u} bkacnahu 595
3.1.4  Successor II ax-succ-succ 598
3.1.5  Addition I: {su'i} msuhi 605
3.1.6  Addition II: {sumji} bsumji 609
3.1.7  Multiplication I: {pi'i} mpihi 613
3.1.8  Multiplication II: {pilji} bpilji 616
3.1.9  Comparison I: {kacme'a} bkacmeha 620
3.2  Exponents I: {tenfa}
3.3  Logarithms: {dugri}
3.4  Cardinality
3.4.1  {ka'au} mkahau 631
3.4.2  {kazmi} sbkazmi 632
3.4.3  Primes: {dilcysle}, {dilcymu'o} sbdilcysle 637
*PART 4  MEREOLOGY
4.1  Parthood
4.1.1  {pagbu} sbpagbu 642
4.1.2  {jompau} sbjompau 651
4.1.3  {kuzypau} sbkuzypau 655
PART 5  SPACE & SPACETIME
5.1  Two-dimensional Euclidean space
5.1.1  Compass directions sbberti 659
5.2  Three-dimensional Euclidean space
5.2.1  Spatial directions sbcrane 665
5.3  Minkowski spacetime
5.3.1  Events: {cfabalvi}, {mulpru} sbcfabalvi 674
5.3.2  Simultaneity: {cabna} sbcabna 678
5.3.3  Non-aorist events: {balvi}, {purci} sbbalvi 682
5.3.4  Elsewhen: {xlane} sbxlane 687
PART 6  RELATIONAL LOGIC
6.1  Lattice of relations
6.1.1  {ki'irni'i} sbkihirnihi 690
6.1.2  {ki'irdu'i} sbkihirduhi 695
6.1.3  {ki'irkanxe} sbkihirkanxe 699
6.1.4  {ki'irvlina} sbkihirvlina 701
6.2  Fractions
6.2.1  Rational number predicate: {frinyna'u} pfr 703
6.2.2  Square roots: {fe'a} pf 711
6.3  Complex numbers
6.3.1  Complex number predicate: {lujna'u} sblujnahu 714
6.3.2  Norm: {cu'a} pcn 722
6.3.3  Real number predicate: {mrena'u} sbmrenahu 725
6.4  Functions I
6.4.1  {fancu} sbfancu 728
6.4.2  {pagyfancu} sbpagyfancu 732
6.5  Assorted claims
6.5.1  {mapti} sbmapti 734
6.5.2  {drata} sbdrata 737
6.5.3  {frica} sbfrica 739
6.5.4  {nenri} sbnenri 741
6.5.5  {fatne} sbfatne 743
6.5.6  {rinka} sbrinka 745
6.6  Ontological classes
*6.6.1  Colors: {skari} sbskari 747
6.6.2  Families: {lanzu} sblanzu 752
6.7  Generated baseline ontology
6.7.1  Classes of selbri ax-kluselbri-baxso 813
6.7.2  Subrelations between selbri ax-gumri-mledi 1027

< Wrap Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1080

Copyright terms: Public domain

< Wrap Next >