Home | Metamath
Proof Explorer Theorem List (p. 172 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 | latj4 17101 | Rearrangement of lattice join of 4 classes. (chj4 28394 analog.) (Contributed by NM, 14-Jun-2012.) |
Theorem | latj4rot 17102 | Rotate lattice join of 4 classes. (Contributed by NM, 11-Jul-2012.) |
Theorem | latjjdi 17103 | Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012.) |
Theorem | latjjdir 17104 | Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012.) |
Theorem | mod1ile 17105 | The weak direction of the modular law (e.g., pmod1i 35134, atmod1i1 35143) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
Theorem | mod2ile 17106 | The weak direction of the modular law (e.g., pmod2iN 35135) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
Syntax | ccla 17107 | Extend class notation with complete lattices. |
Definition | df-clat 17108 | Define the class of all complete lattices, where every subset of the base set has an LUB and a GLB. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
Theorem | isclat 17109 | The predicate "is a complete lattice." (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
Theorem | clatpos 17110 | A complete lattice is a poset. (Contributed by NM, 8-Sep-2018.) |
Theorem | clatlem 17111 | Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011.) |
Theorem | clatlubcl 17112 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
Theorem | clatlubcl2 17113 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 13-Sep-2018.) |
Theorem | clatglbcl 17114 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
Theorem | clatglbcl2 17115 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018.) |
Theorem | clatl 17116 | A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5219 to shorten proof and eliminate joindmss 17007 and meetdmss 17021? |
Theorem | isglbd 17117* | Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.) |
Theorem | lublem 17118* | Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.) |
Theorem | lubub 17119 | The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.) |
Theorem | lubl 17120* | The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.) |
Theorem | lubss 17121 | Subset law for least upper bounds. (chsupss 28201 analog.) (Contributed by NM, 20-Oct-2011.) |
Theorem | lubel 17122 | An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011.) |
Theorem | lubun 17123 | The LUB of a union. (Contributed by NM, 5-Mar-2012.) |
Theorem | clatglb 17124* | Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.) |
Theorem | clatglble 17125 | The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.) |
Theorem | clatleglb 17126* | Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011.) |
Theorem | clatglbss 17127 | Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.) |
Syntax | codu 17128 | Class function defining dual orders. |
ODual | ||
Definition | df-odu 17129 |
Define the dual of an ordered structure, which replaces the order
component of the structure with its reverse. See odubas 17133, oduleval 17131,
and oduleg 17132 for its principal properties.
EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 17188. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual sSet | ||
Theorem | oduval 17130 | Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual sSet | ||
Theorem | oduleval 17131 | Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | oduleg 17132 | Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | odubas 17133 | Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | pospropd 17134* | Posethood is determined only by structure components and only by the value of the relation within the base set. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
Theorem | odupos 17135 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | oduposb 17136 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | meet0 17137 | Lemma for odujoin 17142. (Contributed by Stefan O'Rear, 29-Jan-2015.) TODO (df-riota 6611 update): This proof increased from 152 bytes to 547 bytes after the df-riota 6611 change. Any way to shorten it? join0 17138 also. |
Theorem | join0 17138 | Lemma for odumeet 17140. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
Theorem | oduglb 17139 | Greatest lower bounds in a dual order are least upper bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | odumeet 17140 | Meets in a dual order are joins in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | odulub 17141 | Least upper bounds in a dual order are greatest lower bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | odujoin 17142 | Joins in a dual order are meets in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | odulatb 17143 | Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | oduclatb 17144 | Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | odulat 17145 | Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
ODual | ||
Theorem | poslubmo 17146* | 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.) |
Theorem | posglbmo 17147* | Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018.) |
Theorem | poslubd 17148* | Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
Theorem | poslubdg 17149* | Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
Theorem | posglbd 17150* | Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
Syntax | cipo 17151 | Class function defining inclusion posets. |
toInc | ||
Definition | df-ipo 17152* |
For any family of sets, define the poset of that family ordered by
inclusion. See ipobas 17155, ipolerval 17156, and ipole 17158 for its contract.
EDITORIAL: I'm not thrilled with the name. Any suggestions? (Contributed by Stefan O'Rear, 30-Jan-2015.) (New usage is discouraged.) |
toInc TopSet ordTop | ||
Theorem | ipostr 17153 | The structure of df-ipo 17152 is a structure defining indexes up to 11. (Contributed by Mario Carneiro, 25-Oct-2015.) |
TopSet Struct ; | ||
Theorem | ipoval 17154* | Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
toInc TopSet ordTop | ||
Theorem | ipobas 17155 | Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by Mario Carneiro, 25-Oct-2015.) |
toInc | ||
Theorem | ipolerval 17156* | Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
toInc | ||
Theorem | ipotset 17157 | Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.) |
toInc ordTop TopSet | ||
Theorem | ipole 17158 | Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
toInc | ||
Theorem | ipolt 17159 | Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
toInc | ||
Theorem | ipopos 17160 | The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
toInc | ||
Theorem | isipodrs 17161* | Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
toInc Dirset | ||
Theorem | ipodrscl 17162 | Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
toInc Dirset | ||
Theorem | ipodrsfi 17163* | Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
toInc Dirset | ||
Theorem | fpwipodrs 17164 | The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
toInc Dirset | ||
Theorem | ipodrsima 17165* | The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
toInc Dirset toInc Dirset | ||
Theorem | isacs3lem 17166* | An algebraic closure system satisfies isacs3 17174. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
ACS Moore toInc Dirset | ||
Theorem | acsdrsel 17167 | An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
ACS toInc Dirset | ||
Theorem | isacs4lem 17168* | In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls Moore toInc Dirset Moore toInc Dirset | ||
Theorem | isacs5lem 17169* | If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls Moore toInc Dirset Moore | ||
Theorem | acsdrscl 17170 | In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls ACS toInc Dirset | ||
Theorem | acsficl 17171 | A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls ACS | ||
Theorem | isacs5 17172* | A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls ACS Moore | ||
Theorem | isacs4 17173* | A closure system is algebraic iff closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls ACS Moore toInc Dirset | ||
Theorem | isacs3 17174* | A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
ACS Moore toInc Dirset | ||
Theorem | acsficld 17175 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 17171. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
Theorem | acsficl2d 17176* | 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 17171. Deduction form. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
Theorem | acsfiindd 17177 | 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 | ||
Theorem | acsmapd 17178* | 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 17176 to each element of . See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
Theorem | acsmap2d 17179* | 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 17178 and observing that, since and have the same closure, the closure of must contain . Since is independent, by mrissmrcd 16300, must equal . See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
Theorem | acsinfd 17180 | In an algebraic closure system, if and have the same closure and is infinite independent, then is infinite. This follows from applying unirnffid 8258 to the map given in acsmap2d 17179. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
Theorem | acsdomd 17181 | In an algebraic closure system, if and have the same closure and is infinite independent, then dominates . This follows from applying acsinfd 17180 and then applying unirnfdomd 9389 to the map given in acsmap2d 17179. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
Theorem | acsinfdimd 17182 | 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 17181 twice with acsinfd 17180. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
Theorem | acsexdimd 17183* | In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 16311 for the finite case and acsinfdimd 17182 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 | ||
Theorem | mrelatglb 17184 | Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
toInc Moore | ||
Theorem | mrelatglb0 17185 | The empty intersection in a Moore space is realized by the base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
toInc Moore | ||
Theorem | mrelatlub 17186 | Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
toInc mrCls Moore | ||
Theorem | mreclatBAD 17187* | A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 6611 update): Reprove using isclat 17109 instead of the isclatBAD. hypothesis. See commented-out mreclat above. |
toInc Moore | ||
Theorem | latmass 17188 | Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Theorem | latdisdlem 17189* | Lemma for latdisd 17190. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
Theorem | latdisd 17190* | In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
Syntax | cdlat 17191 | The class of distributive lattices. |
DLat | ||
Definition | df-dlat 17192* | A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 17190) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
DLat | ||
Theorem | isdlat 17193* | Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
DLat | ||
Theorem | dlatmjdi 17194 | In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
DLat | ||
Theorem | dlatl 17195 | A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
DLat | ||
Theorem | odudlatb 17196 | The dual of a distributive lattice is a distributive lattice and conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
ODual DLat DLat | ||
Theorem | dlatjmdi 17197 | In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
DLat | ||
Syntax | cps 17198 | Extend class notation with the class of all posets. |
Syntax | ctsr 17199 | Extend class notation with the class of all totally ordered sets. |
Definition | df-ps 17200 | Define the class of all posets (partially ordered sets) with weak ordering (e.g., "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |