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 17-Jun-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 | ||
17-Jun-2017 | idomsubgmo 26867 | The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.) |
mulGrp ↾_{s} Unit IDomn SubGrp | ||
17-Jun-2017 | hilbert1.2 24139 | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.) |
LinesEE | ||
17-Jun-2017 | cvmliftmo 23173 | A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
CovMap 𝑛Locally | ||
17-Jun-2017 | ply1divmo 19469 | Uniqueness of a quotient in a polynomial division. For polynomials such that and the leading coefficient of is not a zero divisor, there is at most one polynomial which satisfies where the degree of is less than the degree of . (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
Poly_{1} deg_{1} coe_{1} RLReg | ||
17-Jun-2017 | 2ndcdisj2 17131 | Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
17-Jun-2017 | 2ndcdisj 17130 | Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
17-Jun-2017 | lspextmo 15761 | A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
LMHom | ||
17-Jun-2017 | mgmidmo 14318 | A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.) |
17-Jun-2017 | sqrmo 11688 | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
17-Jun-2017 | rmorabex 4191 | Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | dfdisj2 3955 | Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.) |
Disj | ||
17-Jun-2017 | rmo2i 3038 | Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | rmo2 3037 | Alternate definition of restricted "at most one." Note that is not equivalent to (in analogy to reu6 2922); to see this, let be the empty set. However, one direction of this pattern holds; see rmo2i 3038. (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | nrexrmo 2727 | Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | nfrmod 2686 | Deduction version of nfrmo 2688. (Contributed by NM, 17-Jun-2017.) |
16-Jun-2017 | spwmo 14283 | A poset has at most one supremum. (Contributed by NM, 13-May-2008.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | poslubmo 14198 | Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | brdom7disj 8110 | An equivalence to a dominance relation for disjoint sets. (Contributed by NM, 29-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | brdom4 8109 | An equivalence to a dominance relation. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | iunmapdisj 7604 | The union is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | moriotass 6288 | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | dffun9 5207 | Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | reuxfr2 4516 | Transfer existential uniqueness from a variable to another variable contained in expression . (Contributed by NM, 14-Nov-2004.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | reuxfr2d 4515 | Transfer existential uniqueness from a variable to another variable contained in expression . (Contributed by NM, 16-Jan-2012.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | somo 4306 | A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | df-disj 3954 | A collection of classes is disjoint when for each element , it is in for at most one . (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.) |
Disj | ||
16-Jun-2017 | rmoi 3041 | Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | rmob 3040 | Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | rmo3 3039 | Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | 2reuswap 2933 | A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | imrmo 2932 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmoan 2931 | Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmo4 2926 | Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | cbvrmo 2733 | Change the bound variable of restricted "at most one" using implicit substitution. (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmo5 2726 | Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | reurmo 2725 | Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | reu5 2723 | Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | mormo 2722 | Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobii 2704 | Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobiia 2703 | Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobidv 2702 | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobidva 2701 | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobida 2700 | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | nfrmo 2688 | Bound-variable hypothesis builder for restricted uniqueness. (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | nfrmo1 2684 | is not free in . (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | df-rmo 2524 | Define restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
18-May-2017 | fsnunfv 5640 | 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 23021 | The image by of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.) |
2-May-2017 | addeq0 22990 | Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.) |
2-May-2017 | fzsplit3 22977 | 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 15858 | The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 15845 and lbsacsbs 15857 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 14234. (Contributed by David Moews, 1-May-2017.) |
LBasis | ||
1-May-2017 | lbsacsbs 15857 | Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 15855. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd LBasis | ||
1-May-2017 | lssacsex 15845 | In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 15672 by lspsolv 15844. (Contributed by David Moews, 1-May-2017.) |
mrCls ACS | ||
1-May-2017 | acsexdimd 14234 | In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 13500 for the finite case and acsinfdimd 14233 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 14233 | 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 14232 twice with acsinfd 14231. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsdomd 14232 | In an algebraic closure system, if and have the same closure and is infinite independent, then dominates . This follows from applying acsinfd 14231 and then applying unirnfdomd 8143 to the map given in acsmap2d 14230. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsinfd 14231 | In an algebraic closure system, if and have the same closure and is infinite independent, then is infinite. This follows from applying unirnffid 7101 to the map given in acsmap2d 14230. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsmap2d 14230 | 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 14229 and observing that, since and have the same closure, the closure of must contain . Since is independent, by mrissmrcd 13490, 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 14229 | 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 14227 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 14228 | 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 14227 | 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 14222. Deduction form. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
1-May-2017 | acsficld 14226 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 14222. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
1-May-2017 | acsmred 13506 | An algebraic closure system is also a Moore system. Deduction form of acsmre 13502. (Contributed by David Moews, 1-May-2017.) |
ACS Moore | ||
1-May-2017 | mreexfidimd 13500 | 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 13499 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 13499 | 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 13498. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexd 13498 | 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 13496 for the base case and mreexexlem4d 13497 for the induction step. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexlem4d 13497 | Induction step of the induction in mreexexd 13498. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexlem3d 13496 | Base case of the induction in mreexexd 13498. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexlem2d 13495 | Used in mreexexlem4d 13497 to prove the induction step in mreexexd 13498. 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 13494 | This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 13498. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | mreexmrid 13493 | 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 13492 | 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 13491 | In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mrissmrcd 13490 | 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 13477, and so are equal by mrieqv2d 13489.) (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mrieqv2d 13489 | 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 13488 | 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 13487 | 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 13486 | 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 13485 | 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 13484 | 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 13483 | 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 13482 | 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 13481 | 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 13480 | 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 13479 | 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 13488 and mrieqv2d 13489. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mressmrcd 13477 | 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 13476 | Moore closure is idempotent. Deduction form of mrcidm 13469. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mrcssidd 13475 | A set is contained in its Moore closure. Deduction form of mrcssid 13467. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mrcssd 13474 | Moore closure preserves subset ordering. Deduction form of mrcss 13466. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | mrcssvd 13473 | The Moore closure of a set is a subset of the base. Deduction form of mrcssv 13464. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
1-May-2017 | df-mri 13438 | 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 13437 |
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 16764) and linear span (mrclsp 15694).
A Moore closure operation is (1) extensive, i.e., for all subsets of the base set (mrcssid 13467), (2) isotone, i.e., implies that for all subsets and of the base set (mrcss 13466), and (3) idempotent, i.e., for all subsets of the base set (mrcidm 13469.) 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 13436 |
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 16763) and vector spaces (lssmre 15671)
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 13440, mresspw 13442, mre1cl 13444 and mreintcl 13445 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 13450); as such the disjoint union of all Moore collections is sometimes considered as Moore, justified by mreunirn 13451. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
Moore | ||
1-May-2017 | unirnfdomd 8143 | 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 8142 | Equivalence between two infiniteness criteria for sets. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cardidd 8125 | Any set is equinumerous to its cardinal number. Deduction form of cardid 8123. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cardidg 8124 | Any set is equinumerous to its cardinal number. Closed theorem form of cardid 8123. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unirnffid 7101 | 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 6866 | Symmetry of equinumerosity. Deduction form of ensym 6864. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | elfvexd 5476 | If a function value is nonempty, its argument is a set. Deduction form of elfvex 5475. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ordelinel 4449 | 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 4448 | A consequence of total ordering for ordinal classes. Similar to ordtri2or2 4447. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssexd 4121 | A subclass of a set is a set. Deduction form of ssexg 4120. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unissd 3811 | Subclass relationship for subclass union. Deduction form of uniss 3808. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unissi 3810 | Subclass relationship for subclass union. Inference form of uniss 3808. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difsnpss 3718 | is a proper subclass of if and only if is a member of . (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difsneq 3717 | equals if and only if is not a member of . Generalization of difsn 3715. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | neldifsnd 3712 | is not in . Deduction form. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | neldifsn 3711 | is not in . (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | elpwid 3594 | An element of a power class is a subclass. Deduction form of elpwi 3593. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssnelpssd 3479 | Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 3478. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | dfss5 3335 | Another definition of subclasshood. Similar to df-ss 3127, dfss 3128, and dfss1 3334. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unssbd 3314 | If is contained in , so is . One-way deduction form of unss 3310. Partial converse of unssd 3312. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | unssad 3313 | If is contained in , so is . One-way deduction form of unss 3310. Partial converse of unssd 3312. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssdif2d 3276 | 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 3275 | If is contained in , then is also contained in . Deduction form of ssdifss 3268. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | sscond 3274 | If is contained in , then is contained in . Deduction form of sscon 3271. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssdifd 3273 | If is contained in , then is contained in . Deduction form of ssdif 3272. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difss2d 3267 | If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3266. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | difss2 3266 | 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 3265 | A difference of two classes is contained in the minuend. Deduction form of difss 3264. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | psssstrd 3246 | Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 3243. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | sspsstrd 3245 | Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 3242. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | psstrd 3244 | Proper subclass inclusion is transitive. Deduction form of psstr 3241. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | pssned 3235 | Proper subclasses are unequal. Deduction form of pssne 3233. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | ssneldd 3144 | 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 3143 | 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 3126 | If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3123. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | eldifad 3125 | If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3123. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | eldifd 3124 | If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3123. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvrexv2 3109 | 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 3108 | 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 2834 | Rule of specialization, using implicit substitution. Analogous to rcla4dv 2855. (Contributed by David Moews, 1-May-2017.) |
1-May-2017 | cbvrexdva 2740 | 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 2739 | 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 2738 | 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 2737 | 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 2547 | 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 2546 | 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 23018 | The range is invariant under . (Contributed by Thierry Arnoux, 28-Apr-2017.) |
28-Apr-2017 | ballotlemsgt1 23016 | maps values less than to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.) |
27-Apr-2017 | ballotlemfrceq 23034 | Value of for a reverse counting . (Contributed by Thierry Arnoux, 27-Apr-2017.) |
26-Apr-2017 | ballotlemgun 23030 | A property of the defined operator (Contributed by Thierry Arnoux, 26-Apr-2017.) |
25-Apr-2017 | ballotlemfrcn0 23035 | Value of for a reversed counting , before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017.) |
24-Apr-2017 | funimass4f 22989 | Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.) |
24-Apr-2017 | dfimafnf 22988 | 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 28158 | Degenerate case of ax-9 1684. Uses only Tarski's FOL axiom schemes (see description for equidK 28136). (Contributed by NM, 23-Apr-2017.) |
23-Apr-2017 | f1o3d 22984 | Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.) |
21-Apr-2017 | ballotlemfrci 23033 | Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.) |
21-Apr-2017 | ballotlemfrc 23032 | Express the value of in terms of the newly defined . (Contributed by Thierry Arnoux, 21-Apr-2017.) |
21-Apr-2017 | ballotlemfg 23031 | Express the value of in terms of . (Contributed by Thierry Arnoux, 21-Apr-2017.) |
21-Apr-2017 | ballotlemgval 23029 | Expand the value of . (Contributed by Thierry Arnoux, 21-Apr-2017.) |
21-Apr-2017 | ballotlemscr 23024 | The image of by (Contributed by Thierry Arnoux, 21-Apr-2017.) |
20-Apr-2017 | stowei 27134 | 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 27133: often times it will be better to use stoweid 27133 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 27133 | 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 27132 | 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 27131 | 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 27130 | 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 27129 | 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 27128 | 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 27127 | 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 27126 | 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 27125 | 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 27124 | 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 27123 | 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 27122 | 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.) |