Home | Metamath
Proof Explorer Theorem List (p. 163 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imasleval 16201* | The value of the image structure's ordering when the order is compatible with the mapping function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s | ||
Theorem | qusval 16202* | Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s s | ||
Theorem | quslem 16203* | The function in qusval 16202 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s | ||
Theorem | qusin 16204 | Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s s | ||
Theorem | qusbas 16205 | Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s | ||
Theorem | quss 16206 | The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s Scalar Scalar | ||
Theorem | divsfval 16207* | Value of the function in qusval 16202. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
Theorem | ercpbllem 16208* | Lemma for ercpbl 16209. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | ercpbl 16209* | Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
Theorem | erlecpbl 16210* | Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
Theorem | qusaddvallem 16211* | Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s | ||
Theorem | qusaddflem 16212* | The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s | ||
Theorem | qusaddval 16213* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s | ||
Theorem | qusaddf 16214* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s | ||
Theorem | qusmulval 16215* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s | ||
Theorem | qusmulf 16216* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s | ||
Theorem | xpsc 16217 | A short expression for the pair function mapping to and to . (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | xpscg 16218 | A short expression for the pair function mapping to and to . (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | xpscfn 16219 | The pair function is a function on . (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | xpsc0 16220 | The pair function maps to . (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | xpsc1 16221 | The pair function maps to . (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | xpscfv 16222 | The value of the pair function at an element of . (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | xpsfrnel 16223* | Elementhood in the target space of the function appearing in xpsval 16232. (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | xpsfeq 16224 | A function on is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.) |
Theorem | xpsfrnel2 16225* | Elementhood in the target space of the function appearing in xpsval 16232. (Contributed by Mario Carneiro, 15-Aug-2015.) |
Theorem | xpscf 16226 | Equivalent condition for the pair function to be a proper function on . (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xpsfval 16227* | The value of the function appearing in xpsval 16232. (Contributed by Mario Carneiro, 15-Aug-2015.) |
Theorem | xpsff1o 16228* | The function appearing in xpsval 16232 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair . (Contributed by Mario Carneiro, 15-Aug-2015.) |
Theorem | xpsfrn 16229* | A short expression for the indexed cartesian product on two indexes. (Contributed by Mario Carneiro, 15-Aug-2015.) |
Theorem | xpsfrn2 16230* | A short expression for the indexed cartesian product on two indexes. (Contributed by Mario Carneiro, 15-Aug-2015.) |
Theorem | xpsff1o2 16231* | The function appearing in xpsval 16232 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair . (Contributed by Mario Carneiro, 24-Jan-2015.) |
Theorem | xpsval 16232* | Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
s Scalar s s | ||
Theorem | xpslem 16233* | The indexed structure product that appears in xpsval 16232 has the same base as the target of the function . (Contributed by Mario Carneiro, 15-Aug-2015.) |
s Scalar s | ||
Theorem | xpsbas 16234 | The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
s | ||
Theorem | xpsaddlem 16235* | Lemma for xpsadd 16236 and xpsmul 16237. (Contributed by Mario Carneiro, 15-Aug-2015.) |
s Scalars | ||
Theorem | xpsadd 16236 | Value of the addition operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
s | ||
Theorem | xpsmul 16237 | Value of the multiplication operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
s | ||
Theorem | xpssca 16238 | Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015.) |
s Scalar Scalar | ||
Theorem | xpsvsca 16239 | Value of the scalar multiplication function in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
s Scalar | ||
Theorem | xpsless 16240 | Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
s | ||
Theorem | xpsle 16241 | Value of the ordering in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Syntax | cmre 16242 | The class of Moore systems. |
Moore | ||
Syntax | cmrc 16243 | The class function generating Moore closures. |
mrCls | ||
Syntax | cmri 16244 | mrInd is a class function which takes a Moore system to its set of independent sets. |
mrInd | ||
Syntax | cacs 16245 | The class of algebraic closure (Moore) systems. |
ACS | ||
Definition | df-mre 16246* |
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 20882) and vector spaces (lssmre 18966)
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 16250, mresspw 16252, mre1cl 16254 and mreintcl 16255 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 16260); as such the disjoint union of all Moore collections is sometimes considered as Moore, justified by mreunirn 16261. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
Moore | ||
Definition | df-mrc 16247* |
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 20883) and linear span (mrclsp 18989).
A Moore closure operation is (1) extensive, i.e., for all subsets of the base set (mrcssid 16277), (2) isotone, i.e., implies that for all subsets and of the base set (mrcss 16276), and (3) idempotent, i.e., for all subsets of the base set (mrcidm 16279.) 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 | ||
Definition | df-mri 16248* | 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 | ||
Definition | df-acs 16249* | An important subclass of Moore systems are those which can be interpreted as closure under some collection of operators of finite arity (the collection itself is not required to be finite). These are termed algebraic closure systems; similar to definition (A) of an algebraic closure system in [Schechter] p. 84, but to avoid the complexity of an arbitrary mixed collection of functions of various arities (especially if the axiom of infinity omex 8540 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
ACS Moore | ||
Theorem | ismre 16250* | Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore | ||
Theorem | fnmre 16251 | The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 20728 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore | ||
Theorem | mresspw 16252 | A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore | ||
Theorem | mress 16253 | A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
Moore | ||
Theorem | mre1cl 16254 | In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore | ||
Theorem | mreintcl 16255 | A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore | ||
Theorem | mreiincl 16256* | A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Moore | ||
Theorem | mrerintcl 16257 | The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
Moore | ||
Theorem | mreriincl 16258* | The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
Moore | ||
Theorem | mreincl 16259 | Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore | ||
Theorem | mreuni 16260 | Since the entire base set of a Moore collection is the greatest element of it, the base set can be recovered from a Moore collection by set union. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore | ||
Theorem | mreunirn 16261 | Two ways to express the notion of being a Moore collection on an unspecified base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore Moore | ||
Theorem | ismred 16262* | Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore | ||
Theorem | ismred2 16263* | Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
Moore | ||
Theorem | mremre 16264 | The Moore collections of subsets of a space, viewed as a kind of subset of the power set, form a Moore collection in their own right on the power set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Moore Moore | ||
Theorem | submre 16265 | The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
Moore Moore | ||
Theorem | mrcflem 16266* | The domain and range of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
Moore | ||
Theorem | fnmrc 16267 | Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
mrCls Moore | ||
Theorem | mrcfval 16268* | Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcf 16269 | The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcval 16270* | Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Fan Zheng, 6-Jun-2016.) |
mrCls Moore | ||
Theorem | mrccl 16271 | The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcsncl 16272 | The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcid 16273 | The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcssv 16274 | The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcidb 16275 | A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcss 16276 | Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcssid 16277 | The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcidb2 16278 | A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls Moore | ||
Theorem | mrcidm 16279 | The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcsscl 16280 | The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcuni 16281 | Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcun 16282 | Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
mrCls Moore | ||
Theorem | mrcssvd 16283 | The Moore closure of a set is a subset of the base. Deduction form of mrcssv 16274. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
Theorem | mrcssd 16284 | Moore closure preserves subset ordering. Deduction form of mrcss 16276. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
Theorem | mrcssidd 16285 | A set is contained in its Moore closure. Deduction form of mrcssid 16277. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
Theorem | mrcidmd 16286 | Moore closure is idempotent. Deduction form of mrcidm 16279. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
Theorem | mressmrcd 16287 | 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 | ||
Theorem | submrc 16288 | In a closure system which is cut off above some level, closures below that level act as normal. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
mrCls mrCls Moore | ||
Theorem | mrieqvlemd 16289 | 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 16298 and mrieqv2d 16299. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls | ||
Theorem | mrisval 16290* | Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
Theorem | ismri 16291* | Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
Theorem | ismri2 16292* | 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 | ||
Theorem | ismri2d 16293* | 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 | ||
Theorem | ismri2dd 16294* | 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 | ||
Theorem | mriss 16295 | An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017.) |
mrInd Moore | ||
Theorem | mrissd 16296 | 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 | ||
Theorem | ismri2dad 16297 | Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd Moore | ||
Theorem | mrieqvd 16298* | 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 | ||
Theorem | mrieqv2d 16299* | 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 | ||
Theorem | mrissmrcd 16300 | 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 16287, and so are equal by mrieqv2d 16299.) (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |