Metamath Proof Explorer Most Recent Proofs |
||
Mirrors > Home > MPE Home > Th. List > Recent | Other > MM 100 |
Other links Email: Norm Megill. Mailing list: Metamath Google Group Updated 19-May-2017 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (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.
(13-Apr-2017) See equidK for a discussion of the recent theorems in my mathbox. -NM
(24-Mar-2017) Alan Sare updated his completeusersproof program.
(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.
(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).
(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.
(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60.
(28-Dec-2016) David A. Wheeler is putting together a page on Metamath (specifically set.mm) conventions. Comments are welcome on the Google Group thread.
(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph" (symbols: turned F, x, phi) in df-nf to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )". Theorem nf2 shows a version without nested quantifiers.
(22-Dec-2016) Naip Moro has developed a Metamath database for G. Spencer-Brown's Laws of Form. You can follow the Google Group discussion here.
(20-Dec-2016) In metamath program version 0.137, 'verify markup *' now checks that ax-XXX $a matches axXXX $p when the latter exists, per the discussion at https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ.
(24-Nov-2016) Mingl Yuan has kindly provided a mirror site in Beijing, China. He has also provided an rsync server; type "rsync cn.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").
(14-Aug-2016) All HTML pages on this site should now be mobile-friendly and pass the Mobile-Friendly Test. If you find one that does not, let me know.
(14-Aug-2016) Daniel Whalen wrote a paper describing the use of using deep learning to prove 14% of test theorems taken from set.mm: Holophrasm: a neural Automated Theorem Prover for higher-order logic. The associated program is called Holophrasm.
(14-Aug-2016) David A. Wheeler created a video called Metamath Proof Explorer: A Modern Principia Mathematica
(12-Aug-2016) A Gitter chat room has been created for Metamath.
(9-Aug-2016) Mario Carneiro wrote a Metamath proof verifier in the Scala language as part of the ongoing Metamath -> MMT import project
(9-Aug-2016) David A. Wheeler created a GitHub project called metamath-test (last execution run) to check that different verifiers both pass good databases and detect errors in defective ones.
(4-Aug-2016) Mario gave two presentations at CICM 2016.
(17-Jul-2016) Thierry Arnoux has written EMetamath, a Metamath plugin for the Eclipse IDE.
(16-Jul-2016) Mario recovered Chris Capel's collapsible proof demo.
(13-Jul-2016) FL sent me an updated version of PDF (LaTeX source) developed with Lamport's pf2 package. See the 23-Apr-2012 entry below.
(12-Jul-2016) David A. Wheeler produced a new video for mmj2 called "Creating functions in Metamath". It shows a more efficient approach than his previous recent video "Creating functions in Metamath" (old) but it can be of interest to see both approaches.
(10-Jul-2016) Metamath program version 0.132 changes the command 'show restricted' to 'show discouraged' and adds a new command, 'set discouragement'. See the mmnotes.txt entry of 11-May-2016 (updated 10-Jul-2016).
(12-Jun-2016) Dan Getz has written Metamath.jl, a Metamath proof verifier written in the Julia language. Older news...
Color key: | Metamath Proof Explorer | Hilbert Space Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
18-May-2017 | fsnunfv 5619 | Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.) |
5-May-2017 | ballotlemsima 23000 | The image by of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.) |
2-May-2017 | addeq0 22969 | Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.) |
2-May-2017 | fzsplit3 22956 | Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.) |
2-May-2017 | ax12b 1834 | Two equivalent ways of expressing ax-12 1633. See the comment for ax-12 1633. (Contributed by NM, 2-May-2017.) |
1-May-2017 | lvecdim 15837 | The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 15824 and lbsacsbs 15836 to show that being a basis for a vector space is equivalent to being a basis for the associated algebraic closure system, and then using acsexdimd 14213. (Contributed by David Moews, 1-May-2017.) |
LBasis | ||
1-May-2017 | lbsacsbs 15836 | Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 15834. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd LBasis | ||
1-May-2017 | lssacsex 15824 | In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 15651 by lspsolv 15823. (Contributed by David Moews, 1-May-2017.) |
mrCls ACS | ||
1-May-2017 | acsexdimd 14213 | In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 13479 for the finite case and acsinfdimd 14212 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsinfdimd 14212 | In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 14211 twice with acsinfd 14210. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsdomd 14211 | In an algebraic closure system, if and have the same closure and is infinite independent, then dominates . This follows from applying acsinfd 14210 and then applying unirnfdomd 8122 to the map given in acsmap2d 14209. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsinfd 14210 | In an algebraic closure system, if and have the same closure and is infinite independent, then is infinite. This follows from applying unirnffid 7080 to the map given in acsmap2d 14209. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsmap2d 14209 | In an algebraic closure system, if and have the same closure and is independent, then there is a map from into the set of finite subsets of such that equals the union of . This is proven by taking the map from acsmapd 14208 and observing that, since and have the same closure, the closure of must contain . Since is independent, by mrissmrcd 13469, must equal . See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsmapd 14208 | In an algebraic closure system, if is contained in the closure of , there is a map from into the set of finite subsets of such that the closure of contains . This is proven by applying acsficl2d 14206 to each element of . See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
1-May-2017 | acsfiindd 14207 | In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsficl2d 14206 | In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 14201. Deduction form. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
1-May-2017 | acsficld 14205 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 14201. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
1-May-2017 | acsmred 13485 | An algebraic closure system is also a Moore system. Deduction form of acsmre 13481. (Contributed by David Moews, 1-May-2017.) |
ACS Moore | ||
1-May-2017 | mreexfidimd 13479 | In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd 13478 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexdomd 13478 | In a Moore system whose closure operator has the exchange property, if is independent and contained in the closure of , and either or is finite, then dominates . This is an immediate consequence of mreexexd 13477. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexd 13477 | Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if and are disjoint from , is independent, is contained in the closure of , and either or is finite, then there is a subset of equinumerous to such that is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either or is finite. The theorem is proven by induction using mreexexlem3d 13475 for the base case and mreexexlem4d 13476 for the induction step. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexlem4d 13476 | Induction step of the induction in mreexexd 13477. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexlem3d 13475 | Base case of the induction in mreexexd 13477. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexlem2d 13474 | Used in mreexexlem4d 13476 to prove the induction step in mreexexd 13477. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexlemd 13473 | This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 13477. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | mreexmrid 13472 | In a Moore system whose closure operator has the exchange property, if a set is independent and an element is not in its closure, then adding the element to the set gives another independent set. Lemma 4.1.5 in [FaureFrolicher] p. 84. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexd 13471 | In a Moore system, the closure operator is said to have the exchange property if, for all elements and of the base set and subsets of the base set such that is in the closure of but not in the closure of , is in the closure of (Definition 3.1.9 in [FaureFrolicher] p. 57 to 58.) This theorem allows us to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | mrissmrid 13470 | In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mrissmrcd 13469 | In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd 13456, and so are equal by mrieqv2d 13468.) (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mrieqv2d 13468 | In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mrieqvd 13467 | In a Moore system, a set is independent if and only if, for all elements of the set, the closure of the set with the element removed is unequal to the closure of the original set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | ismri2dad 13466 | Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
1-May-2017 | mrissd 13465 | An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017.) |
mrInd Moore | ||
1-May-2017 | mriss 13464 | An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017.) |
mrInd Moore | ||
1-May-2017 | ismri2dd 13463 | Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
1-May-2017 | ismri2d 13462 | Criterion for a subset of the base set in a Moore system to be independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
1-May-2017 | ismri2 13461 | Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
1-May-2017 | ismri 13460 | Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
1-May-2017 | mrisval 13459 | Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
1-May-2017 | mrieqvlemd 13458 | In a Moore system, if is a member of , and have the same closure if and only if is in the closure of . Used in the proof of mrieqvd 13467 and mrieqv2d 13468. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mressmrcd 13456 | In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mrcidmd 13455 | Moore closure is idempotent. Deduction form of mrcidm 13448. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mrcssidd 13454 | A set is contained in its Moore closure. Deduction form of mrcssid 13446. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mrcssd 13453 | Moore closure preserves subset ordering. Deduction form of mrcss 13445. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mrcssvd 13452 | The Moore closure of a set is a subset of the base. Deduction form of mrcssv 13443. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | df-mri 13417 | In a Moore system, a set is independent if no element of the set is in the closure of the set with the element removed (Section 0.6 in [Gratzer] p. 27; Definition 4.1.1 in [FaureFrolicher] p. 83.) mrInd is a class function which takes a Moore system to its set of independent sets. (Contributed by David Moews, 1-May-2017.) |
mrInd Moore mrCls | ||
1-May-2017 | df-mrc 13416 |
Define the Moore closure of a generating set, which is the smallest
closed set containing all generating elements. Definition of Moore
closure in [Schechter] p. 79. This
generalizes topological closure
(mrccls 16743) and linear span (mrclsp 15673).
A Moore closure operation is (1) extensive, i.e., for all subsets of the base set (mrcssid 13446), (2) isotone, i.e., implies that for all subsets and of the base set (mrcss 13445), and (3) idempotent, i.e., for all subsets of the base set (mrcidm 13448.) Operators satisfying these three properties are in bijective correspondence with Moore collections, so these properties may be used to give an alternate characterization of a Moore collection by providing a closure operation on the set of subsets of a given base set which satisfies (1), (2), and (3); the closed sets can be recovered as those sets which equal their closures (Section 4.5 in [Schechter] p. 82.) (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
mrCls Moore | ||
1-May-2017 | df-mre 13415 |
Define a Moore collection, which is a family of subsets of a base set
which preserve arbitrary intersection. Elements of a Moore collection
are termed closed; Moore collections generalize the notion of
closedness from topologies (cldmre 16742) and vector spaces (lssmre 15650)
to the most general setting in which such concepts make sense.
Definition of Moore collection of sets in [Schechter] p. 78. A Moore
collection may also be called a closure system (Section 0.6 in
[Gratzer] p. 23.) The name Moore
collection is after Eliakim Hastings
Moore, who discussed these systems in Part I of [Moore] p. 53 to 76.
See ismre 13419, mresspw 13421, mre1cl 13423 and mreintcl 13424 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 13429); as such the disjoint union of all Moore collections is sometimes considered as Moore, justified by mreunirn 13430. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
Moore | ||
1-May-2017 | unirnfdomd 8122 | The union of the range of a function from a infinite set into the class of finite sets is dominated by its domain. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | infinf 8121 | Equivalence between two infiniteness criteria for sets. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cardidd 8104 | Any set is equinumerous to its cardinal number. Deduction form of cardid 8102. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cardidg 8103 | Any set is equinumerous to its cardinal number. Closed theorem form of cardid 8102. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unirnffid 7080 | The union of the range of a function from a finite set into the class of finite sets is finite. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ensymd 6845 | Symmetry of equinumerosity. Deduction form of ensym 6843. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | elfvexd 5455 | If a function value is nonempty, its argument is a set. Deduction form of elfvex 5454. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ordelinel 4428 | The intersection of two ordinal classes is an element of a third if and only if either one of them is. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ordtri2or3 4427 | A consequence of total ordering for ordinal classes. Similar to ordtri2or2 4426. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssexd 4101 | A subclass of a set is a set. Deduction form of ssexg 4100. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unissd 3792 | Subclass relationship for subclass union. Deduction form of uniss 3789. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unissi 3791 | Subclass relationship for subclass union. Inference form of uniss 3789. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difsnpss 3699 | is a proper subclass of if and only if is a member of . (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difsneq 3698 | equals if and only if is not a member of . Generalization of difsn 3696. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | neldifsnd 3693 | is not in . Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | neldifsn 3692 | is not in . (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | elpwid 3575 | An element of a power class is a subclass. Deduction form of elpwi 3574. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssnelpssd 3460 | Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 3459. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | dfss5 3316 | Another definition of subclasshood. Similar to df-ss 3108, dfss 3109, and dfss1 3315. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unssbd 3295 | If is contained in , so is . One-way deduction form of unss 3291. Partial converse of unssd 3293. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unssad 3294 | If is contained in , so is . One-way deduction form of unss 3291. Partial converse of unssd 3293. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssdif2d 3257 | If is contained in and is contained in , then is contained in . Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssdifssd 3256 | If is contained in , then is also contained in . Deduction form of ssdifss 3249. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | sscond 3255 | If is contained in , then is contained in . Deduction form of sscon 3252. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssdifd 3254 | If is contained in , then is contained in . Deduction form of ssdif 3253. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difss2d 3248 | If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3247. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difss2 3247 | If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difssd 3246 | A difference of two classes is contained in the minuend. Deduction form of difss 3245. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | psssstrd 3227 | Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 3224. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | sspsstrd 3226 | Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 3223. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | psstrd 3225 | Proper subclass inclusion is transitive. Deduction form of psstr 3222. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | pssned 3216 | Proper subclasses are unequal. Deduction form of pssne 3214. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssneldd 3125 | If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssneld 3124 | If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | eldifbd 3107 | If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3104. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | eldifad 3106 | If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3104. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | eldifd 3105 | If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3104. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvrexv2 3090 | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvralv2 3089 | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cla4dv 2817 | Rule of specialization, using implicit substitution. Analogous to rcla4dv 2838. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvrexdva 2723 | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvraldva 2722 | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvrexdva2 2721 | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvraldva2 2720 | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | rexeqbii 2545 | Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | raleqbii 2544 | Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | neleqtrrd 2352 | If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | neleqtrd 2351 | If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | eqneltrrd 2350 | If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | eqneltrd 2349 | If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvexdva 2055 | Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvaldva 2054 | Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
28-Apr-2017 | ballotlemsel1i 22997 | The range is invariant under . (Contributed by Thierry Arnoux, 28-Apr-2017.) |
28-Apr-2017 | ballotlemsgt1 22995 | maps values less than to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.) |
27-Apr-2017 | ballotlemfrceq 23013 | Value of for a reverse counting . (Contributed by Thierry Arnoux, 27-Apr-2017.) |
26-Apr-2017 | ballotlemgun 23009 | A property of the defined operator (Contributed by Thierry Arnoux, 26-Apr-2017.) |
25-Apr-2017 | ballotlemfrcn0 23014 | Value of for a reversed counting , before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017.) |
24-Apr-2017 | funimass4f 22968 | Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.) |
24-Apr-2017 | dfimafnf 22967 | Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.) |
23-Apr-2017 | ax9dgenK 28137 | Degenerate case of ax-9 1684. Uses only Tarski's FOL axiom schemes (see description for equidK 28115). (Contributed by NM, 23-Apr-2017.) |
23-Apr-2017 | f1o3d 22963 | Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.) |
21-Apr-2017 | ballotlemfrci 23012 | Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.) |
21-Apr-2017 | ballotlemfrc 23011 | Express the value of in terms of the newly defined . (Contributed by Thierry Arnoux, 21-Apr-2017.) |
21-Apr-2017 | ballotlemfg 23010 | Express the value of in terms of . (Contributed by Thierry Arnoux, 21-Apr-2017.) |
21-Apr-2017 | ballotlemgval 23008 | Expand the value of . (Contributed by Thierry Arnoux, 21-Apr-2017.) |
21-Apr-2017 | ballotlemscr 23003 | The image of by (Contributed by Thierry Arnoux, 21-Apr-2017.) |
20-Apr-2017 | stowei 27113 | This theorem proves the Stone-Weierstrass theorem for real valued functions: let be a compact topology on , and be the set of real continuous functions on . Assume that is a subalgebra of (closed under addition and multiplication of functions) containing constant functions and discriminating points (if and are distinct points in , then there exists a function in such that h(r) is distinct from h(t) ). Then, for any continuous function and for any positive real , there exists a function in the subalgebra , such that approximates up to ( represents the usual ε value). As a classical example, given any a,b reals, the closed interval could be taken, along with the subalgebra of real polynomials on , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on . The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 27112: often times it will be better to use stoweid 27112 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweid 27112 | This theorem proves the Stone-Weierstrass theorem for real valued functions: let be a compact topology on , and be the set of real continuous functions on . Assume that is a subalgebra of (closed under addition and multiplication of functions) containing constant functions and discriminating points (if and are distinct points in , then there exists a function in such that h(r) is distinct from h(t) ). Then, for any continuous function and for any positive real , there exists a function in the subalgebra , such that approximates up to ( represents the usual ε value). As a classical example, given any a,b reals, the closed interval could be taken, along with the subalgebra of real polynomials on , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on . The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem62 27111 | This theorem proves the Stone Weierstrass theorem for the non trivial case in which T is nonempty. The proof follows [BrosowskiDeutsh] p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem61 27110 | This lemma proves that there exists a function as in the proof in [BrosowskiDeutsh] p. 92: is in the subalgebra, and for all in , abs( f(t) - g(t) ) < 2*ε. Here is used to represent f in the paper, and is used to represent ε. For this lemma there's the further assumption that the function to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem60 27109 | This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all in , there is a such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here is used to represent f in the paper, and is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem59 27108 | This lemma proves that there exists a function as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: x_{j} is in the subalgebra, 0 <= x_{j} <= 1, x_{j} < ε / n on A_{j} (meaning A in the paper), x_{j} > 1 - \epslon / n on B_{j}. Here is used to represent A in the paper (because A is used for the subalgebra of functions), is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem58 27107 | This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem57 27106 | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem56 27105 | This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here is used to represent t_{0} in the paper, is used to represent in the paper, and is used to represent ε (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem55 27104 | This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Here Z is used to represent t_{0} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem54 27103 | There exists a function as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here is used to represent in the paper, because here is used for the subalgebra of functions. is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem53 27102 | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem52 27101 | There exists a neighborood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t_{0} in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem51 27100 | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here is used to represent in the paper, because here is used for the subalgebra of functions. is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem50 27099 | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, contain a finite subcover of T \ U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem49 27098 | There exists a function q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 (at the top of page 91): 0 <= q_{n} <= 1 , q_{n} < ε on , and q_{n} > 1 - ε on . Here y is used to represent the final q_{n} in the paper (the one with n large enough), represents in the paper, represents , represents δ, represents ε, and represents . (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem48 27097 | This lemma is used to prove that built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x < ε on . Here is used to represent in the paper, is used to represent ε in the paper, and is used to represent in the paper (because is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem47 27096 | Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem46 27095 | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem45 27094 | This lemma proves that, given an appropriate (in another theorem we prove such a exists), there exists a function q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= q_{n} <= 1 , q_{n} < ε on T \ U, and q_{n} > 1 - ε on . We use y to represent the final q_{n} in the paper (the one with n large enough), to represent in the paper, to represe |