Metamath Proof Explorer Most Recent Proofs |
||
Mirrors > Home > MPE Home > Th. List > Recent | Other > MM 100 |
The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.
Other links Email: Norm Megill. Mailing list: Metamath Google Group Updated 12-Mar-2018 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (28-Feb-2018) Filip Cernatescu's Milpgame is now stored on the Metamath site, with source code maintained on GitHub. See the link for instructions and other information.
(27-Feb-2018) Bill Hale has released an app for the Apple iPad and desktop computer that allows you to browse Metamath theorems and their proofs.
(17-Jan-2018) Dylan Houlihan has kindly provided a new mirror site. He has also provided an rsync server; type "rsync uk.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").
(15-Jan-2018) The metamath program, version 0.157, has been updated to implement the file inclusion conventions described in the 21-Dec-2017 entry of mmnotes.txt.
(11-Dec-2017) I added a paragraph, suggested by Gérard Lang, to the distinct variable description here.
(10-Dec-2017) Per FL's request, his mathbox will be removed from set.mm. If you wish to export any of his theorems, today's version (master commit 1024a3a) is the last one that will contain it.
(11-Nov-2017) Alan Sare updated his completeusersproof program.
(3-Oct-2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript. He also wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.
(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)
(26-Sep-2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.
(24-Sep-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.
(3-Sep-2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.
(7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.
(1-Jul-2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).
(7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.
(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.
(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62. Older news...
Color key: | Metamath Proof Explorer | Hilbert Space Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
16-Mar-2018 | binomrisefac 25278 | A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018.) |
RiseFac RiseFac RiseFac | ||
15-Mar-2018 | hashfzdm 27941 | The size of a function with a finite set of sequential integers, starting with 0, as domain equals the right border of this range increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.) |
13-Mar-2018 | binomfallfac 25277 | A version of the binomial theorem using falling factorials instead of exponentials. (Contributed by Scott Fenton, 13-Mar-2018.) |
FallFac FallFac FallFac | ||
13-Mar-2018 | binomfallfaclem2 25276 | Lemma for binomfallfac 25277. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.) |
FallFac FallFac FallFac FallFac FallFac FallFac | ||
13-Mar-2018 | binomfallfaclem1 25275 | Lemma for binomfallfac 25277. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.) |
FallFac FallFac | ||
12-Mar-2018 | sibfof 24576 | Applying function operations on simple functions results in simple functions with regard to the the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.) |
sigaGen RRHomScalar measures sitg sitg sitg | ||
11-Mar-2018 | frgregordn0 28113 | If a nonempty friendship graph is k-regular, its order is k(k-1)+1. This corresponds to the third claim in the proof of the friendship theorem in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
FriendGrph VDeg | ||
11-Mar-2018 | usgreghash2spot 28112 | In a finite k-regular graph with N vertices there are N times " choose 2 " paths with length 2, according to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by ordered triples, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
USGrph VDeg 2SPathOnOt | ||
11-Mar-2018 | 2spotmdisj 28111 | The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
2SPathOnOt Disj | ||
11-Mar-2018 | 2spot0 28107 | If there are no vertices, then there are no paths (of length 2), too. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
2SPathOnOt | ||
11-Mar-2018 | kcnktkm1cn 27933 | k times k minus 1 is a complex number if k is a complex number. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
11-Mar-2018 | 3xpfi 27932 | The cross product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
11-Mar-2018 | cnflduss 19249 | The uniform structure of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
UnifStℂ_{fld} metUnif | ||
11-Mar-2018 | xmetutop 18553 | The topology induced by a uniform structure generated by an extended metric is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018.) |
unifTopmetUnif | ||
11-Mar-2018 | psmetutop 18552 | The topology induced by a uniform structure generated by a metric is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet unifTopmetUnif | ||
11-Mar-2018 | elbl4 18545 | Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blval2 18544 | The ball around a point , alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blssexps 18395 | Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blssps 18393 | Any point in a ball can be centered in another ball that is a subset of . (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | ssblps 18391 | The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | unirnblps 18388 | The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blelrnps 18385 | A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blcntrps 18381 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | xblcntrps 18379 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blrnps 18377 | Membership in the range of the ball function. Note that is the collection of all balls for metric . (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blfps 18375 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blss2ps 18372 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | xblss2ps 18370 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 18373 for extended metrics, we have to assume the balls are a finite distance apart, or else will not even be in the infinity ball around . (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | xblpnfps 18364 | The infinity ball in an extended metric is the set of all points that are a finite distance from the center. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blcomps 18362 | Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | elbl2ps 18358 | Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | elblps 18356 | Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | blvalps 18354 | The ball around a point is the set of all points whose distance from is less than the ball's radius . (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | psmetlecl 18285 | Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
10-Mar-2018 | usgreg2spot 28110 | In a finite k-regular graph the set of all paths of length two is the union of all the paths of length 2 over the vertices which are in the the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
2SPathOnOt USGrph VDeg 2SPathOnOt | ||
10-Mar-2018 | usgreghash2spotv 28109 | According to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For simple paths of length 2 represented by ordered triples, we have again k*(k-1) such paths. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
2SPathOnOt USGrph VDeg | ||
10-Mar-2018 | usgfidegfi 28030 | In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
USGrph VDeg | ||
10-Mar-2018 | otiunsndisjX 27916 | The union of singletons consisting of ordered triples which have distinct first and third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
Disj | ||
10-Mar-2018 | otiunsndisj 27915 | The union of singletons consisting of ordered triples which have distinct first and third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
Disj | ||
10-Mar-2018 | otsndisj 27914 | The singletons consisting of ordered triples which have distinct third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
Disj | ||
10-Mar-2018 | otthg 27913 | Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
9-Mar-2018 | usg2spot2nb 28108 | The set of paths of length 2 with a given vertex in the middle for a finite graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |
2SPathOnOt USGrph Neighbors Neighbors | ||
9-Mar-2018 | usg2spthonot1 28027 | A simple path of length 2 between two vertices as ordered triple correspons to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |
USGrph 2SPathOnOt | ||
9-Mar-2018 | el2spthonot0 28008 | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |
2SPathOnOt 2SPathOnOt | ||
9-Mar-2018 | isspthonpth 27953 | Properties of a pair of functions to be a simple path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 9-Mar-2018.) |
SPathOn SPaths | ||
9-Mar-2018 | measge0 24483 | A measure is non negative. (Contributed by Thierry Arnoux, 9-Mar-2018.) |
measures | ||
9-Mar-2018 | disjxpin 23948 | Derive a disjunction over a cross product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018.) |
Disj Disj Disj | ||
8-Mar-2018 | usg2spthonot0 28026 | A simple path of length 2 between two vertices as ordered triple correspons to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |
USGrph 2SPathOnOt | ||
8-Mar-2018 | usg2spthonot 28025 | A simple path of length 2 between two vertices as ordered triple correspons to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |
USGrph 2SPathOnOt | ||
8-Mar-2018 | el2wlkonotot1 28011 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |
2WalksOnOt 2WalksOnOt | ||
8-Mar-2018 | ofpreima 24001 | Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
7-Mar-2018 | nbfiusgrafi 27946 | The class of neighbors of a vertex in a finite graph is a finite set. (Contributed by Alexander van der Vekens, 7-Mar-2018.) |
USGrph Neighbors | ||
6-Mar-2018 | frghash2spot 28106 | The number of simple paths of length 2 is n*(n-1) in a friendship graph with vertices. This corresponds to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, the order of vertices is not respected by Huneke, so he only counts half of the paths which are existing when respecting the order as it is the case for simple paths represented by orderes triples. (Contributed by Alexander van der Vekens, 6-Mar-2018.) |
FriendGrph 2SPathOnOt | ||
6-Mar-2018 | usgfiregdegfi 28031 | In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.) |
USGrph VDeg | ||
6-Mar-2018 | a16g 2012 | Generalization of ax16 2092. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) |
6-Mar-2018 | ax10 1991 | Derive set.mm's original ax-10 2188 from others. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) |
6-Mar-2018 | spime 1960 | Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) |
5-Mar-2018 | 2spotiundisj 28105 | All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 5-Mar-2018.) |
Disj 2SPathOnOt | ||
5-Mar-2018 | df-hcmp 24263 | Definition of the Hausdorff completion. In this definition, a structure is a Hausdorff completion of a uniform structure if is a complete uniform space, in which is dense, and which admits the same uniform structure. Theorem 3 of [BourbakiTop1] p. II.21. states the existence and unicity of such a completion. (Contributed by Thierry Arnoux, 5-Mar-2018.) |
HCmp UnifOn CUnifSp UnifSt | ||
4-Mar-2018 | 2spotdisj 28104 | All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018.) |
Disj 2SPathOnOt | ||
4-Mar-2018 | 2spotfi 28029 | In a finite graph, the set of simple paths of length 2 between two vertices (as ordered triples) is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) |
2SPathOnOt | ||
4-Mar-2018 | ismblfin 26113 | Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) |
4-Mar-2018 | sibf0 24571 | The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-Mar-2018.) |
sigaGen RRHomScalar measures sitg | ||
4-Mar-2018 | dral1 2022 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 4-Mar-2018.) |
4-Mar-2018 | dral2 2020 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) (Revised by Wolf Lammen, 4-Mar-2018.) |
4-Mar-2018 | dvelimh 2015 | Version of dvelim 2064 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 4-Mar-2018.) |
3-Mar-2018 | frg2spot1 28101 | In a friendship graph, there is exactly one simple path of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |
FriendGrph 2SPathOnOt | ||
3-Mar-2018 | 2spot2iun2spont 28028 | The set of simple paths of length 2 (in a graph) is the double union of the simple paths of length 2 between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |
2SPathOnOt 2SPathOnOt | ||
3-Mar-2018 | 2spontn0vne 28024 | If the set of simple paths of length 2 between two vertices (in a graph) is not empty, the two vertices must be not equal. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |
2SPathOnOt | ||
3-Mar-2018 | dvelimhw 1872 | Proof of dvelimh 2015 without using ax-12 1946 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) |
3-Mar-2018 | hbnt 1795 | Closed theorem version of bound-variable hypothesis builder hbn 1797. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) |
3-Mar-2018 | 19.9ht 1788 | A closed version of 19.9 1793. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) |
2-Mar-2018 | 2pthwlkonot 28022 | For two different vertices, a walk of length 2 between these vertices as ordered triple is a simple path of length 2 between these vertices as ordered triple in an undirected simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
USGrph 2SPathOnOt 2WalksOnOt | ||
2-Mar-2018 | el2spthonot 28007 | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
2SPathOnOt SPaths | ||
2-Mar-2018 | usgra2wlkspth 27960 | In a undirected simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
USGrph WalkOn SPathOn | ||
2-Mar-2018 | usgra2wlkspthlem2 27959 | Lemma 2 for usgra2wlkspth 27960. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
Word USGrph ..^ | ||
2-Mar-2018 | usgra2wlkspthlem1 27958 | Lemma 1 for usgra2wlkspth 27960. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
Word ..^ | ||
2-Mar-2018 | spthonisspth 27955 | A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
SPathOn SPaths | ||
2-Mar-2018 | f12dfv 27923 | A one-to-one function with a pair as domain in terms of function values. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
2-Mar-2018 | oteqimp 27912 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
1-Mar-2018 | el2spthsoton 28016 | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
2SPathOnOt 2SPathOnOt | ||
1-Mar-2018 | 2spthonot3v 28013 | If an ordered triple represents a simple path of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
2SPathOnOt | ||
1-Mar-2018 | 2spthonot 28003 | The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
2SPathOnOt SPathOn | ||
1-Mar-2018 | is2spthonot 28001 | The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
2SPathOnOt SPathOn | ||
1-Mar-2018 | df-2spthsot 27998 | Define the collection of all simple paths of length 2 as ordered triple. (in a graph) (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
2SPathOnOt 2SPathOnOt | ||
1-Mar-2018 | df-2spthonot 27997 | Define the collection of simple paths of length 2 with particular endpoints as ordered triple (in a graph) . (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
2SPathOnOt SPathOn | ||
1-Mar-2018 | spthonepeq 27956 | The endpoints of a simple path between two vertices are equal if and only if the path is of length 0 (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
SPathOn | ||
1-Mar-2018 | spthonprp 27954 | Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
SPathOn WalkOn SPaths | ||
1-Mar-2018 | isspthon 27952 | Properties of a pair of functions to be a simple path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
SPathOn WalkOn SPaths | ||
1-Mar-2018 | spthon 27951 | The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
SPathOn WalkOn SPaths | ||
1-Mar-2018 | df-spthon 27950 | Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
SPathOn WalkOn SPaths | ||
28-Feb-2018 | el2pthsot 28018 | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.) |
2SPathOnOt SPaths | ||
28-Feb-2018 | 2spthsot 28005 | The set of simple paths of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.) |
2SPathOnOt 2SPathOnOt | ||
28-Feb-2018 | hbn1fw 1715 | Weak version of ax-6 1740 from which we can prove any ax-6 1740 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
28-Feb-2018 | cbvalvw 1711 | Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
27-Feb-2018 | 2wot2wont 28023 | The set of (simple) paths of length 2 (in a graph) is the set of (simple) paths of length 2 between any two different vertices. (Contributed by Alexander van der Vekens, 27-Feb-2018.) |
2WalksOt 2WalksOnOt | ||
27-Feb-2018 | dveeq1 1987 | Quantifier introduction when one pair of variables is distinct. Revised to be independent of dvelimv 2017. (Contributed by NM, 2-Jan-2002.) (Revised by Wolf Lammen, 27-Feb-2018.) |
27-Feb-2018 | spw 1702 | Weak version of specialization scheme sp 1759. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1759 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1759 having no wff metavariables and mutually distinct set variables (see ax11wdemo 1734 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1759 are spfw 1699 (minimal distinct variable requirements), spnfw 1678 (when is not free in ), spvw 1674 (when does not appear in ), sptruw 1679 (when is true), and spfalw 1680 (when is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.) |
26-Feb-2018 | el2wlksotot 28019 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 26-Feb-2018.) |
2WalksOt Walks | ||
26-Feb-2018 | otel3xp 27911 | An ordered triple is an element of a doubled cross product. (Contributed by Alexander van der Vekens, 26-Feb-2018.) |
26-Feb-2018 | ax12b 1697 | Two equivalent ways of expressing ax-12 1946. See the comment for ax-12 1946. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) |
25-Feb-2018 | cnzh 24276 | The -module of is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.) |
Modℂ_{fld} NrmMod | ||
25-Feb-2018 | dvelimv 2017 | Similar to dvelim 2064 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 25-Feb-2018.) |
25-Feb-2018 | a9e 1948 | At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1563 through ax-14 1725 and ax-17 1623, all axioms other than ax9 1949 are believed to be theorems of free logic, although the system without ax9 1949 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 25-Feb-2018.) |
25-Feb-2018 | sbequ2 1657 | An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Feb-2018.) |
24-Feb-2018 | sitgclre 24581 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
sigaGen RRHomScalar measures sitg Ban Scalar ℂ_{fld} ↾_{s} sitg | ||
24-Feb-2018 | sitgclcn 24580 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the complex numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
sigaGen RRHomScalar measures sitg Ban Scalar ℂ_{fld} sitg | ||
24-Feb-2018 | sitgclbn 24579 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces, with additional conditions on its scalar field. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
sigaGen RRHomScalar measures sitg Scalar Ban CUnifSp UnifSt metUnif Mod NrmMod chr sitg | ||
24-Feb-2018 | sitgclg 24578 | Closure of the Bochner integral on a simple functions. This version is very generic, thus the many hypothesis. See sitgclbn 24579 for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
sigaGen RRHomScalar measures sitg Scalar CMnd NrmRing Mod NrmMod chr CUnifSp UnifSt metUnif sitg | ||
24-Feb-2018 | subrgchr 24152 | If is a subring of , then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
SubRing chr ↾_{s} chr | ||
24-Feb-2018 | psmetxrge0 18283 | The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
PsMet | ||
24-Feb-2018 | spimt 1953 | Closed theorem form of spim 1955. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Feb-2018.) |
23-Feb-2018 | spei 1964 | Inference from existential specialization, using implicit substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 19-Aug-1993.) (Revised by Wolf Lammen, 23-Feb-2018.) |
21-Feb-2018 | el2wlksot 28017 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
2WalksOt Walks | ||
21-Feb-2018 | el2wlksoton 28015 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
2WalksOt 2WalksOnOt | ||
21-Feb-2018 | 2wlksot 28004 | The set of walks of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
2WalksOt 2WalksOnOt | ||
21-Feb-2018 | 3xpexg 27902 | The cross product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
21-Feb-2018 | mblfinlem 26112 | Lemma for ismblfin 26113, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) |
20-Feb-2018 | frg2woteqm 28102 | There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 20-Feb-2018.) |
FriendGrph 2WalksOnOt 2WalksOnOt | ||
19-Feb-2018 | frg2wot1 28100 | In a friendship graph, there is exactly one walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |
FriendGrph 2WalksOnOt | ||
19-Feb-2018 | 2wlkonotv 28014 | If an ordered tripple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |
2WalksOnOt | ||
19-Feb-2018 | 2wlkonot3v 28012 | If an ordered triple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |
2WalksOnOt | ||
19-Feb-2018 | sibfima 24575 | Any preimage of a singleton by a simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
sigaGen RRHomScalar measures sitg | ||
19-Feb-2018 | sibfrn 24574 | A simple function has finite range. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
sigaGen RRHomScalar measures sitg | ||
19-Feb-2018 | sibff 24573 | A simple function is a function. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
sigaGen RRHomScalar measures sitg | ||
19-Feb-2018 | sibfmbl 24572 | A simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
sigaGen RRHomScalar measures sitg MblFnM | ||
19-Feb-2018 | issibf 24570 | The predicate " is a simple function" relative to the Bochner integral. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
sigaGen RRHomScalar measures sitg MblFnM | ||
19-Feb-2018 | dmmeas 24477 | The domain of a measure is a sigma algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
measures sigAlgebra | ||
19-Feb-2018 | xrhval 24306 | The value of the embedding from the extended real numbers into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
RRHom RR^{*}Hom RRHom | ||
19-Feb-2018 | df-xrh 24305 | Define an embedding from the extended real number into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
RR^{*}Hom RRHom RRHom RRHom | ||
19-Feb-2018 | spimed 1958 | Deduction version of spime 1960. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) |
18-Feb-2018 | frg2wotn0 28099 | In a friendship graph, there is always a path/walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
FriendGrph 2WalksOnOt | ||
18-Feb-2018 | frg2woteu 28098 | For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
FriendGrph 2WalksOnOt | ||
18-Feb-2018 | frgraeu 28097 | Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
FriendGrph | ||
18-Feb-2018 | usg2wlkonot 28020 | A walk of length 2 between two vertices as ordered triple in an undirected simple graph. This theorem would also hold for undirected multigraphs, but to proof this the cases and/or must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
USGrph 2WalksOnOt | ||
18-Feb-2018 | usg2wlkon 27990 | In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
USGrph WalkOn | ||
18-Feb-2018 | usg2wlk 27989 | In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
USGrph Walks | ||
18-Feb-2018 | usgra2adedgwlkon 27987 | In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
USGrph WalkOn | ||
18-Feb-2018 | usgra2adedgwlk 27986 | In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
USGrph Walks | ||
18-Feb-2018 | 2pthlem2 27977 | Lemma 2 for constr2pth 21521. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by Alexander van der Vekens, 18-Feb-2018.) |
..^ | ||
18-Feb-2018 | 2wlklemC 27972 | Lemma for constr2wlk 27979. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
18-Feb-2018 | 2wlklemB 27971 | Lemma for constr2wlk 27979. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
18-Feb-2018 | 2wlklemA 27970 | Lemma for constr2wlk 27979. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
18-Feb-2018 | uhgraedgrnv 27943 | An edge of an undirected hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
UHGrph | ||
18-Feb-2018 | xrsp1 24126 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | xrsp0 24125 | The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | xrinfm 24041 | The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | infxrmnf 24040 | The infinimum of a set of extended reals containing minus infnity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | xlemnf 24037 | An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | spim 1955 | Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 1955 series of theorems requires that only one direction of the substitution hypothesis hold. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) |
17-Feb-2018 | 0risefac 25274 | The value of the zero rising factorial at natural . (Contributed by Scott Fenton, 17-Feb-2018.) |
RiseFac | ||
17-Feb-2018 | 0fallfac 25273 | The value of the zero falling factorial at natural . (Contributed by Scott Fenton, 17-Feb-2018.) |
FallFac | ||
17-Feb-2018 | clatp1ex 24116 | The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
17-Feb-2018 | clatp0ex 24115 | The poset zero of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
17-Feb-2018 | tosglb 24114 | Same theorem as toslub 24113, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
Toset | ||
17-Feb-2018 | aevlem1 2010 | Lemma for ax10 1991. Change free and bound variables. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) |
17-Feb-2018 | ax10lem2 1989 | Lemma for ax10 1991. Change bound variable. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) |
16-Feb-2018 | usg2wotspth 28021 | A walk of length 2 between two different vertices as ordered triple corresponds to a simple path of length 2 in an undirected simple graph. (Contributed by Alexander van der Vekens, 16-Feb-2018.) |
USGrph 2WalksOnOt SPaths | ||
16-Feb-2018 | is2wlk 27948 | Properties of a pair of functions to be a walk of length 2 (in an undirected graph). (Contributed by Alexander van der Vekens, 16-Feb-2018.) |
Walks ..^ | ||
15-Feb-2018 | el2wlkonotot 28010 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
2WalksOnOt Walks | ||
15-Feb-2018 | el2wlkonotot0 28009 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
2WalksOnOt Walks | ||
15-Feb-2018 | el2wlkonot 28006 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
2WalksOnOt Walks | ||
15-Feb-2018 | 2wlkonot 28002 | The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
2WalksOnOt WalkOn | ||
15-Feb-2018 | is2wlkonot 28000 | The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
2WalksOnOt WalkOn | ||
15-Feb-2018 | el2wlkonotlem 27999 | Lemma for el2wlkonot 28006. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
Walks | ||
15-Feb-2018 | df-2wlksot 27996 | Define the collection of all walks of length 2 as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
2WalksOt 2WalksOnOt | ||
15-Feb-2018 | df-2wlkonot 27995 | Define the collection of walks of length 2 with particular endpoints as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
2WalksOnOt WalkOn | ||
15-Feb-2018 | el2xptp0 27910 | A member of a nested cross product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
15-Feb-2018 | el2xptp 27909 | A member of a nested cross product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
15-Feb-2018 | xrsclat 24124 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
15-Feb-2018 | xrstos 24123 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
Toset | ||
15-Feb-2018 | toslub 24113 | In a toset, the lowest upper bound , defined for partial orders is the supremum, , defined for total orders, if this supremum exists (these are the set.mm definition: lowest upper bound and supremum are normally synonymous) Note that the two definitions do not have the same value when there is no such supremum. In that case, will take the value , but takes the value , therefore, we restrict this theorem only to the case where this supremum exists, which is expressed by the last assumption. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
Toset | ||
14-Feb-2018 | frg2woteq 28103 | There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 14-Feb-2018.) |
FriendGrph 2WalksOnOt 2WalksOnOt | ||
14-Feb-2018 | rezh 24277 | The -module of is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
ℂ_{fld} ↾_{s} Mod NrmMod | ||
14-Feb-2018 | reust 24266 | The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
ℂ_{fld} ↾_{s} UnifSt metUnif | ||
14-Feb-2018 | ofresid 23975 | Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
13-Feb-2018 | df-itgm 24586 |
Define the Bochner integral as the extension by continuity of the
Bochnel integral for simple functions.
Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric sitm. He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 19455. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
itgm measures metUnifsitmCnExtUnifStsitg | ||
13-Feb-2018 | sitmcl 24585 | Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
measures sitg sitg sitm | ||
13-Feb-2018 | sitgf 24582 | The integral for simple functions is itself a function. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
sigaGen RRHomScalar measures sitg sitg sitg sitg | ||
12-Feb-2018 | iprodgam 25241 | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
11-Feb-2018 | iprodefisum 25240 | Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.) |
11-Feb-2018 | iprodefisumlem 25239 | Lemma for iprodefisum 25240. (Contributed by Scott Fenton, 11-Feb-2018.) |
11-Feb-2018 | pstmxmet 24214 | The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
~Met PsMet pstoMet | ||
11-Feb-2018 | pstmfval 24213 | Function value of the metric induced by a pseudometric (Contributed by Thierry Arnoux, 11-Feb-2018.) |
~Met PsMet pstoMet | ||
11-Feb-2018 | metider 24211 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
PsMet ~Met | ||
11-Feb-2018 | tltnle 24112 | In a Toset, less-than is equivalent to not inverse less-than-or-equal see pltnle 14364. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
Toset | ||
11-Feb-2018 | tleile 24111 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
Toset | ||
11-Feb-2018 | adantl6r 23879 | Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
11-Feb-2018 | adantl5r 23878 | Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
11-Feb-2018 | adantl4r 23877 | Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
11-Feb-2018 | adantl3r 23876 | Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
11-Feb-2018 | cfilucfil4 19213 | Given a metric and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
CauFil_{u}metUnif CauFil | ||
11-Feb-2018 | cfilucfil3 19211 | Given a metric and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
CauFil_{u}metUnif CauFil | ||
11-Feb-2018 | metucn 18558 | Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 18512. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
metUnif metUnif PsMet PsMet Cn_{u} | ||
11-Feb-2018 | metuel2 18548 | Elementhood in the uniform structure generated by a metric (Contributed by Thierry Arnoux, 24-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
metUnif PsMet | ||
11-Feb-2018 | metuel 18547 | Elementhood in the uniform structure generated by a metric (Contributed by Thierry Arnoux, 8-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet metUnif | ||
11-Feb-2018 | cfilucfil2 18543 | Given a metric and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 19157. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet CauFil_{u}metUnif | ||
11-Feb-2018 | metuust 18541 | The uniform structure generated by metric is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet metUnif UnifOn | ||
11-Feb-2018 | cfilucfil 18539 | Given a metric and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 19157. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet CauFil_{u} | ||
11-Feb-2018 | metust 18537 | The uniform structure generated by a metric (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet UnifOn | ||
11-Feb-2018 | metustfbas 18535 | The filter base generated by a metric . (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | metustexhalf 18533 | For any element of the filter base generated by the metric , the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | metustsym 18531 | Elements of the filter base generated by the metric are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | metustid 18529 | The identity diagonal is included in all elements of the filter base generated by the metric . (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | metustto 18527 | Any two elements of the filter base generated by the metric can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | metustrel 18525 | Elements of the filter base generated by the metric are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | metustss 18523 | Range of the elements of the filter base generated by the metric . (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | metustel 18521 | Define a filter base generated by a metric . (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | metuval 18519 | Value of the uniform structure generated by metric . (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet metUnif | ||
11-Feb-2018 | blfval 18353 | The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Proof shortened by Thierry Arnoux, 11-Feb-2018.) |
11-Feb-2018 | blfvalps 18352 | The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | psmetres2 18284 | Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
PsMet PsMet | ||
11-Feb-2018 | psmettri 18281 | Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | psmettri2 18279 | Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
PsMet | ||
11-Feb-2018 | df-metu 16643 | Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
metUnif PsMet | ||
11-Feb-2018 | df-bl 16638 | Define the metric space ball function. See blval 18355 for its value. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
9-Feb-2018 | usisuhgra 27944 | An undirected simple graph without loops is an undirected hypergraph. (Contributed by Alexander van der Vekens, 9-Feb-2018.) |
USGrph UHGrph | ||
8-Feb-2018 | euhash1 27942 | The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.) |
8-Feb-2018 | ax12olem4 1975 | Lemma for ax12o 1976. (Contributed by Wolf Lammen, 8-Feb-2018.) |
8-Feb-2018 | ax12olem2 1973 | Lemma for ax12o 1976. (Contributed by Wolf Lammen, 8-Feb-2018.) |
8-Feb-2018 | ax12olem1 1972 | Lemma for ax12o 1976. The proof of ax12o 1976 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Feb-2018.) |
7-Feb-2018 | rexdifpr 27908 | Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.) |
7-Feb-2018 | pstmval 24212 | Value of the metric induced by a pseudometric . (Contributed by Thierry Arnoux, 7-Feb-2018.) |
~Met PsMet pstoMet | ||
7-Feb-2018 | metideq 24210 | Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet ~Met ~Met | ||
7-Feb-2018 | metidv 24209 | and identify by the metric if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet ~Met | ||
7-Feb-2018 | metidss 24208 | As a relation, the metric identification is a subset of a cross product. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet ~Met | ||
7-Feb-2018 | metidval 24207 | Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet ~Met | ||
7-Feb-2018 | df-pstm 24206 | Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
pstoMet PsMet ~Met ~Met | ||
7-Feb-2018 | df-metid 24205 | Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
~Met PsMet | ||
7-Feb-2018 | xmetpsmet 18317 | An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
7-Feb-2018 | psmetge0 18282 | The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
7-Feb-2018 | psmetsym 18280 | The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
7-Feb-2018 | psmet0 18278 | The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
7-Feb-2018 | psmetcl 18277 | Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
7-Feb-2018 | psmetf 18276 | The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
7-Feb-2018 | psmetdmdm 18275 | Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
7-Feb-2018 | ispsmet 18274 | Express the predicate " is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
7-Feb-2018 | df-psmet 16635 | Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
6-Feb-2018 | equsex 1969 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.) |
5-Feb-2018 | constr2wlk 27979 | Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018.) |
Walks | ||
5-Feb-2018 | equsal 1966 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) |
5-Feb-2018 | equs4 1951 | Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) |
5-Feb-2018 | equid 1684 | Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by WolfLammen, 5-Feb-2018.) |
4-Feb-2018 | hashimarni 27939 | If the size of the image of a one-to-one function under the range of a function which is a one-to-one function into the domain of is a nonnegative integer, the size of the function is the same nonnegative integer. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
..^ | ||
4-Feb-2018 | hashimarn 27938 | The size of the image of a one-to-one function under the range of a function which is a one-to-one function into the domain of equals the size of the function . (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
..^ | ||
4-Feb-2018 | hashf1rnN 27937 | TODO: SHOULD REPLACE hashf1rn 11577 IN PROOFS WHICH CAN BE DELETED AFTERWARDS! The size of a one-to-one function is equal to the size of the function's range. Generalisation of hashf1rn 11577. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
4-Feb-2018 | f1o2ndf1 27930 | The (second member of an ordered pair) function restricted to a one-to-one function is a one-to-one function of onto the range of . (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
4-Feb-2018 | fo2ndf 27929 | The (second member of an ordered pair) function restricted to a function is a function of onto the range of . (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
4-Feb-2018 | f2ndf 27928 | The (second member of an ordered pair) function restricted to a function is a function of into the codomain of . (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
4-Feb-2018 | ax9 1949 |
Theorem showing that ax-9 1662 follows from the weaker version ax9v 1663.
(Even though this theorem depends on ax-9 1662,
all references of ax-9 1662
are made via ax9v 1663. An earlier version stated ax9v 1663
as a separate
axiom, but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-9 1662 so that all proofs can be traced back to ax9v 1663. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.) |
3-Feb-2018 | resfnfinfin 27931 | The restriction of a function by a finite set is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.) |
3-Feb-2018 | resisresindm 27919 | The restriction of a relation by a set is identical with the restriction by the intersection of with the domain of the relation. (Contributed by Alexander van der Vekens, 3-Feb-2018.) |
3-Feb-2018 | eximii 1584 | Inference associated with eximi 1582. (Contributed by BJ, 3-Feb-2018.) |
2-Feb-2018 | imarnf1pr 27927 | The image of the range of a function under a function when is a function of a pair into the domain of . (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
2-Feb-2018 | rnfdmpr 27926 | The range of a one-to-one function of an unordered pair into a set is the unordered pair of the function values. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
2-Feb-2018 | iunxprg 27917 | A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
2-Feb-2018 | fprod0diag 25232 | Two ways to express "the product of over the the triangular region , , . Compare fsum0diag 12502. (Contributed by Scott Fenton, 2-Feb-2018.) |
2-Feb-2018 | fprodcom 25231 | Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018.) |
1-Feb-2018 | usgra2adedglem1 27988 | In an undirected simple graph, two adjacent edges are an unordered pair of unordered pairs. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
USGrph | ||
1-Feb-2018 | usgra2adedgspth 27985 | In an undirected simple graph, two adjacent edges form a simple path of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
USGrph SPaths | ||
1-Feb-2018 | usgra2adedgspthlem2 27984 | Lemma for usgra2adedgspth 27985. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
USGrph | ||
1-Feb-2018 | usgra2adedgspthlem1 27983 | Lemma 1 for usgra2adedgspth 27985. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
USGrph | ||
1-Feb-2018 | constr2spth 27981 | A simple path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
SPaths | ||
1-Feb-2018 | constr2trlN 27980 | Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by Alexander van der Vekens, 1-Feb-2018.) |
Trails | ||
1-Feb-2018 | 2wlklem1 27978 | Lemma 1 for constr2wlk 27979. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
1-Feb-2018 | 2trllemG 27974 | TODO: revise wlkntrllem3 21487!) Lemma 7 for constr2trl 21518. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
1-Feb-2018 | 2wlklem 27947 | Lemma for is2wlk 27948 and 2wlklemA 27970. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
1-Feb-2018 | fz0tp 27934 | An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
1-Feb-2018 | tpssi 27907 | A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
1-Feb-2018 | fprodcom2 25230 | Interchange order of multiplication. Note that and are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018.) |
1-Feb-2018 | fprodcnv 25229 | Tra |