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-Apr-2018 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (11-Apr-2018) Benoît Jubin solved an open problem about the "Axiom of Twoness", showing that it is necessary for completeness. See item 14 on the "Open problems and miscellany" page.
(30-Mar-2018) Filip Cernatescu's Milpgame has been updated to version 0.6, which reduces the set.mm load time to about 40 seconds. A new how-to has also been added to its web page.
(25-Mar-2018) Giovanni Mascellani has announced mmpp, a new proof editing environment for the Metamath language.
(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 | ||
15-Apr-2018 | equveli 2042 | A variable elimination law for equality with no distinct variable requirements. (Compare equvini 2040.) (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Apr-2018.) |
7-Apr-2018 | swrd0swrd0 28014 | A prefix of a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018.) |
Word substr substr substr | ||
7-Apr-2018 | 2elfz3nn0 27984 | If there are two elements in a finite set of sequential integers from 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018.) |
7-Apr-2018 | equvini 2040 | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require to be distinct from and (making the proof longer). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2018.) |
6-Apr-2018 | swrdswrd0 28013 | A subword of a prefix. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
Word substr substr substr | ||
6-Apr-2018 | 0elfz 27983 | 0 is an element of a finite set of sequential integers from 0 to a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
6-Apr-2018 | nn0resubcl 27975 | Closure law for subtraction of reals, restricted to nonnnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
6-Apr-2018 | nn0readdcl 27974 | Closure law for addition of reals, restricted to nonnnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
6-Apr-2018 | ltsubnn0 27973 | Subtracting a nonnegative integer from a nonnegative integer which is greater than the first one results in a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
6-Apr-2018 | lesubnn0 27972 | Subtracting a nonnegative integer from a nonnegative integer which is greater than or equal to the first one results in a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
5-Apr-2018 | swrdccatin12c 28028 | The subword of a concatenation of two words within both of the concatenated words. REMARK: Maybe this can be proven directly, without using swrdccatin12 28026 (this would be a special case of the current theorem) and swrdccatin12b 28027 (this would be obsolete then). (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
Word Word concat substr substr concat substr | ||
5-Apr-2018 | swrdccatin12b 28027 | The subword of a concatenation of two words within both of the concatenated words. REMARK: If swrdccatin12c 28028 is proven directly, this theorem would be obsolete then). (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
Word Word concat substr substr concat substr | ||
5-Apr-2018 | swrd0swrdid 28012 | A prefix of a prefix with the same length is the prefix. (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
Word substr substr substr | ||
5-Apr-2018 | swrdrlen 28003 | Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
Word substr | ||
4-Apr-2018 | swrdswrd 28011 | A subword of a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
Word substr substr substr | ||
4-Apr-2018 | swrdswrdlem 28010 | Lemma for swrdswrd 28011. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
Word Word | ||
4-Apr-2018 | cnambfre 26154 | A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.) |
↾_{t} MblFn | ||
3-Apr-2018 | elfzelfzelfz 27981 | En element of a finite set of sequential integers is an element of a finite set of sequential integers with the upper bound being an element of the finite set of sequential integers with the same lower bound as for the first interval and the element under consideration as upper bound. (Contributed by Alexander van der Vekens, 3-Apr-2018.) |
3-Apr-2018 | zletr 27980 | Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.) |
3-Apr-2018 | itgaddnclem2 26163 | Lemma for itgaddnc 26164; cf. itgaddlem2 19668. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.) |
MblFn | ||
2-Apr-2018 | swrd0swrd 28009 | A prefix of a subword. (Contributed by Alexander van der Vekens, 2-Apr-2018.) |
Word substr substr substr | ||
2-Apr-2018 | nn0fz0 27979 | Nonnegative integers expressed in terms of finite sets of sequential integers with lower bound 0. (Contributed by Alexander van der Vekens, 2-Apr-2018.) |
2-Apr-2018 | mbfposadd 26153 | If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018.) |
MblFn MblFn MblFn MblFn | ||
1-Apr-2018 | lenrevcctswrd 28005 | The length of two reversely concatenated parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.) |
Word substr concat substr | ||
1-Apr-2018 | addlenrevswrd 28004 | The sum of the lengths of two parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.) |
Word substr substr | ||
31-Mar-2018 | swrdccat3b 28031 | A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) |
Word Word concat substr substr substr concat | ||
31-Mar-2018 | swrdccat3a 28030 | A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) |
Word Word concat substr substr concat substr | ||
31-Mar-2018 | swrd0 28002 | A subword of an empty set is always the empty set. REMARK: The antecedent should not be necessary! (Contributed by Alexander van der Vekens, 31-Mar-2018.) |
substr | ||
31-Mar-2018 | mbfresfi 26152 | Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.) |
MblFn MblFn | ||
30-Mar-2018 | swrdccat3 28029 | The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
Word Word concat substr substr substr substr concat substr | ||
30-Mar-2018 | swrdccatin12 28026 | The subword of a concatenation of two words within both of the concatenated words. REMARK: If swrdccatin12c 28028 is proven directly, this theorem would be special case of swrdccatin12c 28028). (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
Word Word ..^ concat substr substr concat substr | ||
30-Mar-2018 | swrdccatin12lem4 28025 | Lemma 4 for swrdccatin12 28026. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
Word Word ..^ ..^ ..^ concat substr substr | ||
30-Mar-2018 | swrdccatin12lem3 28024 | Lemma 3 for swrdccatin12 28026. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
Word Word ..^ ..^ ..^ concat substr substr substr | ||
30-Mar-2018 | swrdccatin12lem3c 28023 | Lemma for swrdccatin12lem3 28024 and swrdccatin12lem4 28025. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
Word Word ..^ concat Word concat | ||
30-Mar-2018 | swrdccatin12lem3b 28022 | Lemma 2 for swrdccatin12lem3 28024. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
..^ ..^ ..^ ..^ | ||
30-Mar-2018 | swrdccatin12lem3a 28021 | Lemma 1 for swrdccatin12lem3 28024. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
..^ ..^ ..^ ..^ | ||
30-Mar-2018 | swrdccatin12lem2 28020 | Lemma 2 for swrdccatin12 28026. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
..^ ..^ ..^ | ||
30-Mar-2018 | ccatvalfn 28008 | The concatenation of two words is a function over the half-open interval of integers having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
Word Word concat ..^ | ||
30-Mar-2018 | elfzonelfzo 27992 | If an element of a half-open range of integers is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
..^ ..^ ..^ | ||
30-Mar-2018 | elfzomelpfzo 27989 | An integer increased by another interger is an element of a half-open range of integers if and only if the integer is contained in the half-open range of integers with bounds decreased by the other integer. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
..^ ..^ | ||
29-Mar-2018 | swrdccatin2lem1 28017 | Lemma for swrdccatin2 28018. (Contributed by Alexander van der Vekens, 29-Mar-2018.) |
..^ ..^ | ||
29-Mar-2018 | elfzmlbp 27978 | Subtracting the lower bound of a finite sets of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) |
29-Mar-2018 | elfzmlbm 27977 | Subtracting the left border of a finite sets of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) |
28-Mar-2018 | swrdccatin12lem1 28019 | Lemma 1 for swrdccatin12 28026. (Contributed by Alexander van der Vekens, 28-Mar-2018.) |
Word Word ..^ Word | ||
28-Mar-2018 | swrdccatin2 28018 | The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) |
Word Word concat substr substr | ||
28-Mar-2018 | swrdccatin1 28016 | The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) |
Word Word concat substr substr | ||
28-Mar-2018 | swrdvalfn 28007 | Value of the subword extractor as function with domain. (Contributed by Alexander van der Vekens, 28-Mar-2018.) |
Word substr ..^ | ||
28-Mar-2018 | elfzelfzccat 28006 | An element of a finite set of sequential integers up to the length of a word is an element of an extended finite set of sequential integers up to the length of a concatenation of this word with another word. (Contributed by Alexander van der Vekens, 28-Mar-2018.) |
Word Word concat | ||
28-Mar-2018 | elfzelfzadd 27982 | An element of a finite set of sequential integers is an element of an extended finite set of sequential integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.) |
28-Mar-2018 | 0mbf 26151 | The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.) |
MblFn | ||
28-Mar-2018 | ismblfin 26146 | Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.) |
28-Mar-2018 | mblfinlem3 26145 | Backward direction of ismblfin 26146. (Contributed by Brendan Leahy, 28-Mar-2018.) |
27-Mar-2018 | swrdccat3a0 28015 | The subword of a concatenation of an empty word with another word is the subword of the second concatenated word. (Contributed by Alexander van der Vekens, 27-Mar-2018.) |
Word concat substr substr | ||
27-Mar-2018 | 2if2 27941 | Resolve two nested conditionals. (Contributed by Alexander van der Vekens, 27-Mar-2018.) |
25-Mar-2018 | fseq0hash 27993 | The value of the size function on a finite 0-based sequence. (Contributed by Alexander van der Vekens, 25-Mar-2018.) |
..^ | ||
25-Mar-2018 | mblfinlem2 26144 | The difference between two sets measurable by the criterion in ismblfin 26146 is itself measurable by the same. Proposition 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) |
23-Mar-2018 | fzosplitsnm1 27991 | Removing a singleton from a half-open range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
..^ ..^ | ||
23-Mar-2018 | ubmelm1fzo 27987 | If an integer between 0 and an upper bound of a half open interval of integers minus 1 is subtracted from this upper bound, the result is contained in this half open interval. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
..^ ..^ | ||
22-Mar-2018 | axbnd 2384 |
Axiom of Bundling (intuitionistic logic axiom ax-bnd).
In classical logic, this and axi12 2383 are fairly straightforward consequences of ax12o 1976. But in intuitionistic logic, it is not easy to add the extra to axi12 2383 and so we treat the two as separate axioms. (Contributed by Jim Kingdon, 22-Mar-2018.) |
21-Mar-2018 | fzo1fzo0n0 27988 | An integer between 1 and an upper bound of a half open interval of integers is not 0 and between 0 and the upper bound of a half open interval of integers. (Contributed by Alexander van der Vekens, 21-Mar-2018.) |
..^ ..^ | ||
20-Mar-2018 | usgranloop 21352 | In an undirected simple graph without loops, there is no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) |
USGrph | ||
20-Mar-2018 | usisuslgra 21340 | An undirected simple graph without loops is an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) |
USGrph USLGrph | ||
20-Mar-2018 | eqlei2 9140 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
20-Mar-2018 | eqlei 9139 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
19-Mar-2018 | 0mnnnnn0 27971 | The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.) |
18-Mar-2018 | ubmelfzo 27986 | If an integer between 0 and an upper bound of a half open interval of integers is subtracted from this upper bound, the result is contained in this half open interval. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
..^ ..^ | ||
18-Mar-2018 | fzo0ss1 27985 | Subset relationship for half-open sequences of integers with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
..^ ..^ | ||
18-Mar-2018 | leaddsuble 27970 | Addition and subtraction on one side of 'less or equal'. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
18-Mar-2018 | cnm1cn 27968 | A complex number minus 1 is a complex number. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
16-Mar-2018 | swrdnd 28001 | The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
Word substr | ||
16-Mar-2018 | swrdltnd 28000 | The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
Word substr | ||
16-Mar-2018 | ssfzo12 27990 | Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
..^ ..^ | ||
16-Mar-2018 | ssfz12 27976 | Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
16-Mar-2018 | binomrisefac 25309 | 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 27997 | 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 | itg2addnc 26158 | Alternate proof of itg2add 19604 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 19553, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 8271, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.) |
MblFn | ||
13-Mar-2018 | binomfallfac 25308 | 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 25307 | Lemma for binomfallfac 25308. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.) |
FallFac FallFac FallFac FallFac FallFac FallFac | ||
13-Mar-2018 | binomfallfaclem1 25306 | Lemma for binomfallfac 25308. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.) |
FallFac FallFac | ||
12-Mar-2018 | sibfof 24607 | 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 28173 | 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 28172 | 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 28171 | 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 28167 | 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 27969 | 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 27967 | The cross product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
11-Mar-2018 | itg2addnclem3 26157 | Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 26158. (Contributed by Brendan Leahy, 11-Mar-2018.) |
MblFn | ||
11-Mar-2018 | cnflduss 19263 | 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 18567 | 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 18566 | 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 18559 | 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 18558 | 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 18409 | 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 18407 | 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 18405 | 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 18402 | 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 18399 | 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 18395 | 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 18393 | 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 18391 | 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 18389 | 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 18386 | 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 18384 | 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 18387 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 18378 | 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 18376 | 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 18372 | Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
11-Mar-2018 | elblps 18370 | 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 18368 | 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 18299 | 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 28170 | 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 28169 | 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 28090 | 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 27955 | 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 27954 | 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 27953 | 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 27952 | Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
10-Mar-2018 | itg2addnclem 26155 | An alternate expression for the integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.) |
9-Mar-2018 | usg2spot2nb 28168 | 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 28087 | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |
USGrph 2SPathOnOt | ||
9-Mar-2018 | el2spthonot0 28068 | 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 | measge0 24514 | A measure is non negative. (Contributed by Thierry Arnoux, 9-Mar-2018.) |
measures | ||
9-Mar-2018 | disjxpin 23981 | 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 | ||
9-Mar-2018 | isspthonpth 21537 | 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 | ||
8-Mar-2018 | usg2spthonot0 28086 | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |
USGrph 2SPathOnOt | ||
8-Mar-2018 | usg2spthonot 28085 | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |
USGrph 2SPathOnOt | ||
8-Mar-2018 | el2wlkonotot1 28071 | 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 24034 | Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
7-Mar-2018 | nbfiusgrafi 28034 | 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 28166 | 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 28091 | 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 | ax10 1991 | Derive set.mm's original ax-10 2190 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 28165 | 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 24294 | 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 28164 | 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 28089 | 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 | sibf0 24602 | 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 2066 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 4-Mar-2018.) |
3-Mar-2018 | frg2spot1 28161 | 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 28088 | 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 28084 | 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 28082 | 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 28067 | 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 28038 | 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 28037 | Lemma 2 for usgra2wlkspth 28038. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
Word USGrph ..^ | ||
2-Mar-2018 | usgra2wlkspthlem1 28036 | Lemma 1 for usgra2wlkspth 28038. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
Word ..^ | ||
2-Mar-2018 | f12dfv 27961 | 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 27951 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
2-Mar-2018 | spthonisspth 21539 | A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
SPathOn SPaths | ||
1-Mar-2018 | el2spthsoton 28076 | 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 28073 | 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 28063 | 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 28061 | 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 28058 | 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 28057 | 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 21540 | 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 21538 | Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
SPathOn WalkOn SPaths | ||
1-Mar-2018 | isspthon 21536 | 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 21535 | 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 21478 | 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 28078 | 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 28065 | 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 28083 | 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 28079 | 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 27950 | 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 24307 | 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 2066 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 ax-9 1662 are believed to be theorems of free logic, although the system without ax-9 1662 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 24612 | 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 24611 | 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 24610 | 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 24609 | Closure of the Bochner integral on a simple functions. This version is very generic, thus the many hypothesis. See sitgclbn 24610 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 24183 | 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 18297 | 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 28077 | 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 28075 | 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 28064 | 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 27942 | The cross product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
21-Feb-2018 | mblfinlem 26143 | Lemma for ismblfin 26146, 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 28162 | 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 28160 | 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 28074 | 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 28072 | 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 24606 | 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 24605 | A simple function has finite range. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
sigaGen RRHomScalar measures sitg | ||
19-Feb-2018 | sibff 24604 | A simple function is a function. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
sigaGen RRHomScalar measures sitg | ||
19-Feb-2018 | sibfmbl 24603 | A simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
sigaGen RRHomScalar measures sitg MblFnM | ||
19-Feb-2018 | issibf 24601 | 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 24508 | The domain of a measure is a sigma algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
measures sigAlgebra | ||
19-Feb-2018 | xrhval 24337 | 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 24336 | 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 28159 | 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 28158 | 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 28157 | 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 28080 | 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 28050 | 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 28049 | 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 28047 | 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 28046 | 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 | uhgraedgrnv 28032 | An edge of an undirected hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
UHGrph | ||
18-Feb-2018 | xrsp1 24157 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | xrsp0 24156 | The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | xrinfm 24074 | The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | infxrmnf 24073 | 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 24070 | An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
18-Feb-2018 | 2pthlem2 21549 | Lemma 2 for constr2pth 21554. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by Alexander van der Vekens, 18-Feb-2018.) |
..^ | ||
18-Feb-2018 | 2wlklemC 21509 | Lemma for constr2wlk 21551. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
18-Feb-2018 | 2wlklemB 21508 | Lemma for constr2wlk 21551. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
18-Feb-2018 | 2wlklemA 21507 | Lemma for constr2wlk 21551. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
18-Feb-2018 | a16g 2012 | Generalization of ax16 2094. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 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 25305 | The value of the zero rising factorial at natural . (Contributed by Scott Fenton, 17-Feb-2018.) |
RiseFac | ||
17-Feb-2018 | 0fallfac 25304 | The value of the zero falling factorial at natural . (Contributed by Scott Fenton, 17-Feb-2018.) |
FallFac | ||
17-Feb-2018 | clatp1ex 24147 | The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
17-Feb-2018 | clatp0ex 24146 | The poset zero of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
17-Feb-2018 | tosglb 24145 | Same theorem as toslub 24144, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
Toset | ||
17-Feb-2018 | aevlem1 2010 | Lemma for aev 2011 and a16g 2012. 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 28081 | 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 21518 | 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 28070 | 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 28069 | 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 28066 | 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 28062 | 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 28060 | 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 28059 | Lemma for el2wlkonot 28066. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
Walks | ||
15-Feb-2018 | df-2wlksot 28056 | 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 28055 | 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 27949 | A member of a nested cross product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
15-Feb-2018 | el2xptp 27948 | A member of a nested cross product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
15-Feb-2018 | xrsclat 24155 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
15-Feb-2018 | xrstos 24154 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
Toset | ||
15-Feb-2018 | toslub 24144 | 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 28163 | 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 24308 | The -module of is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
ℂ_{fld} ↾_{s} Mod NrmMod | ||
14-Feb-2018 | reust 24297 | The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
ℂ_{fld} ↾_{s} UnifSt metUnif | ||
14-Feb-2018 | ofresid 24008 | 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 24617 |
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 19469. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
itgm measures metUnifsitmCnExtUnifStsitg | ||
13-Feb-2018 | sitmcl 24616 | 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 24613 | 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 25272 | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
11-Feb-2018 | iprodefisum 25271 | Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.) |
11-Feb-2018 | iprodefisumlem 25270 | Lemma for iprodefisum 25271. (Contributed by Scott Fenton, 11-Feb-2018.) |
11-Feb-2018 | pstmxmet 24245 | 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 24244 | Function value of the metric induced by a pseudometric (Contributed by Thierry Arnoux, 11-Feb-2018.) |
~Met PsMet pstoMet | ||
11-Feb-2018 | metider 24242 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
PsMet ~Met | ||
11-Feb-2018 | tltnle 24143 | In a Toset, less-than is equivalent to not inverse less-than-or-equal see pltnle 14378. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
Toset |