Home | Metamath
Proof Explorer Theorem List (p. 171 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 | joinfval 17001* | Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 17002 first to reduce net proof size (existence part)? |
Theorem | joinfval2 17002* | Value of join function for a poset-type structure. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
Theorem | joindm 17003* | Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.) |
Theorem | joindef 17004 | Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.) |
Theorem | joinval 17005 | Join value. Since both sides evaluate to when they don't exist, for convenience we drop the requirement. (Contributed by NM, 9-Sep-2018.) |
Theorem | joincl 17006 | Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
Theorem | joindmss 17007 | Subset property of domain of join. (Contributed by NM, 12-Sep-2018.) |
Theorem | joinval2lem 17008* | Lemma for joinval2 17009 and joineu 17010. (Contributed by NM, 12-Sep-2018.) TODO: combine this through joineu into joinlem? |
Theorem | joinval2 17009* | Value of join for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 11-Sep-2018.) |
Theorem | joineu 17010* | Uniqueness of join of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
Theorem | joinlem 17011* | Lemma for join properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
Theorem | lejoin1 17012 | A join's first argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011.) |
Theorem | lejoin2 17013 | A join's second argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011.) |
Theorem | joinle 17014 | A join is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.) |
Theorem | meetfval 17015* | Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove meetfval2 17016 first to reduce net proof size (existence part)? |
Theorem | meetfval2 17016* | Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
Theorem | meetdm 17017* | Domain of meet function for a poset-type structure. (Contributed by NM, 16-Sep-2018.) |
Theorem | meetdef 17018 | Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018.) |
Theorem | meetval 17019 | Meet value. Since both sides evaluate to when they don't exist, for convenience we drop the requirement. (Contributed by NM, 9-Sep-2018.) |
Theorem | meetcl 17020 | Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
Theorem | meetdmss 17021 | Subset property of domain of meet. (Contributed by NM, 12-Sep-2018.) |
Theorem | meetval2lem 17022* | Lemma for meetval2 17023 and meeteu 17024. (Contributed by NM, 12-Sep-2018.) TODO: combine this through meeteu into meetlem? |
Theorem | meetval2 17023* | Value of meet for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 11-Sep-2018.) |
Theorem | meeteu 17024* | Uniqueness of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
Theorem | meetlem 17025* | Lemma for meet properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
Theorem | lemeet1 17026 | A meet's first argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
Theorem | lemeet2 17027 | A meet's second argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
Theorem | meetle 17028 | A meet is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
Theorem | joincomALT 17029 | The join of a poset commutes. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 16-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | joincom 17030 | The join of a poset commutes. (The antecedent i.e. "the joins exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
Theorem | meetcomALT 17031 | The meet of a poset commutes. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 17-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | meetcom 17032 | The meet of a poset commutes. (The antecedent i.e. "the meets exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 17-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
Syntax | ctos 17033 | Extend class notation with the class of all tosets. |
Toset | ||
Definition | df-toset 17034* | Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014.) |
Toset | ||
Theorem | istos 17035* | The predicate "is a toset." (Contributed by FL, 17-Nov-2014.) |
Toset | ||
Theorem | tosso 17036 | Write the totally ordered set structure predicate in terms of the proper class strict order predicate. (Contributed by Mario Carneiro, 8-Feb-2015.) |
Toset | ||
Syntax | cp0 17037 | Extend class notation with poset zero. |
Syntax | cp1 17038 | Extend class notation with poset unit. |
Definition | df-p0 17039 | Define poset zero. (Contributed by NM, 12-Oct-2011.) |
Definition | df-p1 17040 | Define poset unit. (Contributed by NM, 22-Oct-2011.) |
Theorem | p0val 17041 | Value of poset zero. (Contributed by NM, 12-Oct-2011.) |
Theorem | p1val 17042 | Value of poset zero. (Contributed by NM, 22-Oct-2011.) |
Theorem | p0le 17043 | Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011.) (Revised by NM, 13-Sep-2018.) |
Theorem | ple1 17044 | Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011.) (Revised by NM, 13-Sep-2018.) |
Syntax | clat 17045 | Extend class notation with the class of all lattices. |
Definition | df-lat 17046 | Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
Theorem | islat 17047 | The predicate "is a lattice." (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
Theorem | latcl2 17048 | The join and meet of any two elements exist. (Contributed by NM, 14-Sep-2018.) |
Theorem | latlem 17049 | Lemma for lattice properties. (Contributed by NM, 14-Sep-2011.) |
Theorem | latpos 17050 | A lattice is a poset. (Contributed by NM, 17-Sep-2011.) |
Theorem | latjcl 17051 | Closure of join operation in a lattice. (chjcom 28365 analog.) (Contributed by NM, 14-Sep-2011.) |
Theorem | latmcl 17052 | Closure of meet operation in a lattice. (incom 3805 analog.) (Contributed by NM, 14-Sep-2011.) |
Theorem | latref 17053 | A lattice ordering is reflexive. (ssid 3624 analog.) (Contributed by NM, 8-Oct-2011.) |
Theorem | latasymb 17054 | A lattice ordering is asymmetric. (eqss 3618 analog.) (Contributed by NM, 22-Oct-2011.) |
Theorem | latasym 17055 | A lattice ordering is asymmetric. (eqss 3618 analog.) (Contributed by NM, 8-Oct-2011.) |
Theorem | lattr 17056 | A lattice ordering is transitive. (sstr 3611 analog.) (Contributed by NM, 17-Nov-2011.) |
Theorem | latasymd 17057 | Deduce equality from lattice ordering. (eqssd 3620 analog.) (Contributed by NM, 18-Nov-2011.) |
Theorem | lattrd 17058 | A lattice ordering is transitive. Deduction version of lattr 17056. (Contributed by NM, 3-Sep-2012.) |
Theorem | latjcom 17059 | The join of a lattice commutes. (chjcom 28365 analog.) (Contributed by NM, 16-Sep-2011.) |
Theorem | latlej1 17060 | A join's first argument is less than or equal to the join. (chub1 28366 analog.) (Contributed by NM, 17-Sep-2011.) |
Theorem | latlej2 17061 | A join's second argument is less than or equal to the join. (chub2 28367 analog.) (Contributed by NM, 17-Sep-2011.) |
Theorem | latjle12 17062 | A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 28368 analog.) (Contributed by NM, 17-Sep-2011.) |
Theorem | latleeqj1 17063 | Less-than-or-equal-to in terms of join. (chlejb1 28371 analog.) (Contributed by NM, 21-Oct-2011.) |
Theorem | latleeqj2 17064 | Less-than-or-equal-to in terms of join. (chlejb2 28372 analog.) (Contributed by NM, 14-Nov-2011.) |
Theorem | latjlej1 17065 | Add join to both sides of a lattice ordering. (chlej1i 28332 analog.) (Contributed by NM, 8-Nov-2011.) |
Theorem | latjlej2 17066 | Add join to both sides of a lattice ordering. (chlej2i 28333 analog.) (Contributed by NM, 8-Nov-2011.) |
Theorem | latjlej12 17067 | Add join to both sides of a lattice ordering. (chlej12i 28334 analog.) (Contributed by NM, 8-Nov-2011.) |
Theorem | latnlej 17068 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 28-May-2012.) |
Theorem | latnlej1l 17069 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
Theorem | latnlej1r 17070 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
Theorem | latnlej2 17071 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 10-Jul-2012.) |
Theorem | latnlej2l 17072 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
Theorem | latnlej2r 17073 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
Theorem | latjidm 17074 | Lattice join is idempotent. (Contributed by NM, 8-Oct-2011.) |
Theorem | latmcom 17075 | The join of a lattice commutes. (Contributed by NM, 6-Nov-2011.) |
Theorem | latmle1 17076 | A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.) |
Theorem | latmle2 17077 | A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.) |
Theorem | latlem12 17078 | An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011.) |
Theorem | latleeqm1 17079 | Less-than-or-equal-to in terms of meet. (Contributed by NM, 7-Nov-2011.) |
Theorem | latleeqm2 17080 | Less-than-or-equal-to in terms of meet. (Contributed by NM, 7-Nov-2011.) |
Theorem | latmlem1 17081 | Add meet to both sides of a lattice ordering. (Contributed by NM, 10-Nov-2011.) |
Theorem | latmlem2 17082 | Add meet to both sides of a lattice ordering. (sslin 3839 analog.) (Contributed by NM, 10-Nov-2011.) |
Theorem | latmlem12 17083 | Add join to both sides of a lattice ordering. (ss2in 3840 analog.) (Contributed by NM, 10-Nov-2011.) |
Theorem | latnlemlt 17084 | Negation of less-than-or-equal-to expressed in terms of meet and less-than. (nssinpss 3856 analog.) (Contributed by NM, 5-Feb-2012.) |
Theorem | latnle 17085 | Equivalent expressions for "not less than" in a lattice. (chnle 28373 analog.) (Contributed by NM, 16-Nov-2011.) |
Theorem | latmidm 17086 | Lattice join is idempotent. (inidm 3822 analog.) (Contributed by NM, 8-Nov-2011.) |
Theorem | latabs1 17087 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs1 28375 analog.) (Contributed by NM, 8-Nov-2011.) |
Theorem | latabs2 17088 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs2 28376 analog.) (Contributed by NM, 8-Nov-2011.) |
Theorem | latledi 17089 | An ortholattice is distributive in one ordering direction. (ledi 28399 analog.) (Contributed by NM, 7-Nov-2011.) |
Theorem | latmlej11 17090 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
Theorem | latmlej12 17091 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
Theorem | latmlej21 17092 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
Theorem | latmlej22 17093 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
Theorem | lubsn 17094 | The least upper bound of a singleton. (chsupsn 28272 analog.) (Contributed by NM, 20-Oct-2011.) |
Theorem | latjass 17095 | Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (chjass 28392 analog.) (Contributed by NM, 17-Sep-2011.) |
Theorem | latj12 17096 | Swap 1st and 2nd members of lattice join. (chj12 28393 analog.) (Contributed by NM, 4-Jun-2012.) |
Theorem | latj32 17097 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 2-Dec-2011.) |
Theorem | latj13 17098 | Swap 1st and 3rd members of lattice join. (Contributed by NM, 4-Jun-2012.) |
Theorem | latj31 17099 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 23-Jun-2012.) |
Theorem | latjrot 17100 | Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |