HomeTheorem List (p. 185 of 479)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 185 of 479) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30171) |
Hilbert Space Explorer
(30172-31694) |
Users' Mathboxes
(31695-47852) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | latlej1 18401 | A join's first argument is less than or equal to the join. (chub1 30760 analog.) (Contributed by NM, 17-Sep-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β€ (π β¨ π)) | ||
| Theorem | latlej2 18402 | A join's second argument is less than or equal to the join. (chub2 30761 analog.) (Contributed by NM, 17-Sep-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β€ (π β¨ π)) | ||
| Theorem | latjle12 18403 | A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 30762 analog.) (Contributed by NM, 17-Sep-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) | ||
| Theorem | latleeqj1 18404 | "Less than or equal to" in terms of join. (chlejb1 30765 analog.) (Contributed by NM, 21-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β€ π β (π β¨ π) = π)) | ||
| Theorem | latleeqj2 18405 | "Less than or equal to" in terms of join. (chlejb2 30766 analog.) (Contributed by NM, 14-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β€ π β (π β¨ π) = π)) | ||
| Theorem | latjlej1 18406 | Add join to both sides of a lattice ordering. (chlej1i 30726 analog.) (Contributed by NM, 8-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β (π β¨ π) β€ (π β¨ π))) | ||
| Theorem | latjlej2 18407 | Add join to both sides of a lattice ordering. (chlej2i 30727 analog.) (Contributed by NM, 8-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β (π β¨ π) β€ (π β¨ π))) | ||
| Theorem | latjlej12 18408 | Add join to both sides of a lattice ordering. (chlej12i 30728 analog.) (Contributed by NM, 8-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ (π β¨ π))) | ||
| Theorem | latnlej 18409 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 28-May-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ (π β¨ π)) β (π β π β§ π β π)) | ||
| Theorem | latnlej1l 18410 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ (π β¨ π)) β π β π) | ||
| Theorem | latnlej1r 18411 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ (π β¨ π)) β π β π) | ||
| Theorem | latnlej2 18412 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 10-Jul-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ (π β¨ π)) β (Β¬ π β€ π β§ Β¬ π β€ π)) | ||
| Theorem | latnlej2l 18413 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ (π β¨ π)) β Β¬ π β€ π) | ||
| Theorem | latnlej2r 18414 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ (π β¨ π)) β Β¬ π β€ π) | ||
| Theorem | latjidm 18415 | Lattice join is idempotent. Analogue of unidm 4153. (Contributed by NM, 8-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ π β π΅) β (π β¨ π) = π) | ||
| Theorem | latmcom 18416 | The join of a lattice commutes. (Contributed by NM, 6-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) = (π β§ π)) | ||
| Theorem | latmle1 18417 | A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β€ π) | ||
| Theorem | latmle2 18418 | A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β€ π) | ||
| Theorem | latlem12 18419 | 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.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ (π β§ π))) | ||
| Theorem | latleeqm1 18420 | "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β€ π β (π β§ π) = π)) | ||
| Theorem | latleeqm2 18421 | "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β€ π β (π β§ π) = π)) | ||
| Theorem | latmlem1 18422 | Add meet to both sides of a lattice ordering. (Contributed by NM, 10-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β (π β§ π) β€ (π β§ π))) | ||
| Theorem | latmlem2 18423 | Add meet to both sides of a lattice ordering. (sslin 4235 analog.) (Contributed by NM, 10-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β (π β§ π) β€ (π β§ π))) | ||
| Theorem | latmlem12 18424 | Add join to both sides of a lattice ordering. (ss2in 4237 analog.) (Contributed by NM, 10-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β (π β§ π) β€ (π β§ π))) | ||
| Theorem | latnlemlt 18425 | Negation of "less than or equal to" expressed in terms of meet and less-than. (nssinpss 4257 analog.) (Contributed by NM, 5-Feb-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β (π β§ π) < π)) | ||
| Theorem | latnle 18426 | Equivalent expressions for "not less than" in a lattice. (chnle 30767 analog.) (Contributed by NM, 16-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β π < (π β¨ π))) | ||
| Theorem | latmidm 18427 | Lattice meet is idempotent. Analogue of inidm 4219. (Contributed by NM, 8-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅) β (π β§ π) = π) | ||
| Theorem | latabs1 18428 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs1 30769 analog.) (Contributed by NM, 8-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ (π β§ π)) = π) | ||
| Theorem | latabs2 18429 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs2 30770 analog.) (Contributed by NM, 8-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ (π β¨ π)) = π) | ||
| Theorem | latledi 18430 | An ortholattice is distributive in one ordering direction. (ledi 30793 analog.) (Contributed by NM, 7-Nov-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β¨ (π β§ π)) β€ (π β§ (π β¨ π))) | ||
| Theorem | latmlej11 18431 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ π) β€ (π β¨ π)) | ||
| Theorem | latmlej12 18432 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ π) β€ (π β¨ π)) | ||
| Theorem | latmlej21 18433 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ π) β€ (π β¨ π)) | ||
| Theorem | latmlej22 18434 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ π) β€ (π β¨ π)) | ||
| Theorem | lubsn 18435 | The least upper bound of a singleton. (chsupsn 30666 analog.) (Contributed by NM, 20-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β Lat β§ π β π΅) β (πβ{π}) = π) | ||
| Theorem | latjass 18436 | Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (chjass 30786 analog.) (Contributed by NM, 17-Sep-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π) = (π β¨ (π β¨ π))) | ||
| Theorem | latj12 18437 | Swap 1st and 2nd members of lattice join. (chj12 30787 analog.) (Contributed by NM, 4-Jun-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ (π β¨ π)) = (π β¨ (π β¨ π))) | ||
| Theorem | latj32 18438 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 2-Dec-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π) = ((π β¨ π) β¨ π)) | ||
| Theorem | latj13 18439 | Swap 1st and 3rd members of lattice join. (Contributed by NM, 4-Jun-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ (π β¨ π)) = (π β¨ (π β¨ π))) | ||
| Theorem | latj31 18440 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 23-Jun-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π) = ((π β¨ π) β¨ π)) | ||
| Theorem | latjrot 18441 | Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π) = ((π β¨ π) β¨ π)) | ||
| Theorem | latj4 18442 | Rearrangement of lattice join of 4 classes. (chj4 30788 analog.) (Contributed by NM, 14-Jun-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π))) | ||
| Theorem | latj4rot 18443 | Rotate lattice join of 4 classes. (Contributed by NM, 11-Jul-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π))) | ||
| Theorem | latjjdi 18444 | Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π))) | ||
| Theorem | latjjdir 18445 | Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π) = ((π β¨ π) β¨ (π β¨ π))) | ||
| Theorem | mod1ile 18446 | The weak direction of the modular law (e.g., pmod1i 38719, atmod1i1 38728) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β (π β¨ (π β§ π)) β€ ((π β¨ π) β§ π))) | ||
| Theorem | mod2ile 18447 | The weak direction of the modular law (e.g., pmod2iN 38720) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β ((π β§ π) β¨ π) β€ (π β§ (π β¨ π)))) | ||
| Theorem | latmass 18448 | Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = (π β§ (π β§ π))) | ||
| Theorem | latdisdlem 18449* | Lemma for latdisd 18450. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ (πΎ β Lat β (βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) | ||
| Theorem | latdisd 18450* | 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.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ (πΎ β Lat β (βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β¨ (π¦ β§ π§)) = ((π₯ β¨ π¦) β§ (π₯ β¨ π§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) | ||
| Syntax | ccla 18451 | Extend class notation with complete lattices. |
| class CLat | ||
| Definition | df-clat 18452 | 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.) |
| β’ CLat = {π β Poset β£ (dom (lubβπ) = π« (Baseβπ) β§ dom (glbβπ) = π« (Baseβπ))} | ||
| Theorem | isclat 18453 | The predicate "is a complete lattice". (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
| β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) β β’ (πΎ β CLat β (πΎ β Poset β§ (dom π = π« π΅ β§ dom πΊ = π« π΅))) | ||
| Theorem | clatpos 18454 | A complete lattice is a poset. (Contributed by NM, 8-Sep-2018.) |
| β’ (πΎ β CLat β πΎ β Poset) | ||
| Theorem | clatlem 18455 | Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β ((πβπ) β π΅ β§ (πΊβπ) β π΅)) | ||
| Theorem | clatlubcl 18456 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β (πβπ) β π΅) | ||
| Theorem | clatlubcl2 18457 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 13-Sep-2018.) |
| β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β π β dom π) | ||
| Theorem | clatglbcl 18458 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β (πΊβπ) β π΅) | ||
| Theorem | clatglbcl2 18459 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018.) |
| β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β π β dom πΊ) | ||
| Theorem | oduclatb 18460 | Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| β’ π· = (ODualβπ) β β’ (π β CLat β π· β CLat) | ||
| Theorem | clatl 18461 | A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5796 to shorten proof and eliminate joindmss 18332 and meetdmss 18346? |
| β’ (πΎ β CLat β πΎ β Lat) | ||
| Theorem | isglbd 18462* | Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) & β’ ((π β§ π¦ β π) β π» β€ π¦) & β’ ((π β§ π₯ β π΅ β§ βπ¦ β π π₯ β€ π¦) β π₯ β€ π») & β’ (π β πΎ β CLat) & β’ (π β π β π΅) & β’ (π β π» β π΅) β β’ (π β (πΊβπ) = π») | ||
| Theorem | lublem 18463* | Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β (βπ¦ β π π¦ β€ (πβπ) β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§))) | ||
| Theorem | lubub 18464 | The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β π β€ (πβπ)) | ||
| Theorem | lubl 18465* | The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π΅) β (βπ¦ β π π¦ β€ π β (πβπ) β€ π)) | ||
| Theorem | lubss 18466 | Subset law for least upper bounds. (chsupss 30595 analog.) (Contributed by NM, 20-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β (πβπ) β€ (πβπ)) | ||
| Theorem | lubel 18467 | An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π β§ π β π΅) β π β€ (πβπ)) | ||
| Theorem | lubun 18468 | The LUB of a union. (Contributed by NM, 5-Mar-2012.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π΅) β (πβ(π βͺ π)) = ((πβπ) β¨ (πβπ))) | ||
| Theorem | clatglb 18469* | Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β (βπ¦ β π (πΊβπ) β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ (πΊβπ)))) | ||
| Theorem | clatglble 18470 | The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β (πΊβπ) β€ π) | ||
| Theorem | clatleglb 18471* | Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π΅) β (π β€ (πΊβπ) β βπ¦ β π π β€ π¦)) | ||
| Theorem | clatglbss 18472 | Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β (πΊβπ) β€ (πΊβπ)) | ||
| Syntax | cdlat 18473 | The class of distributive lattices. |
| class DLat | ||
| Definition | df-dlat 18474* | A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 18450) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ DLat = {π β Lat β£ [(Baseβπ) / π][(joinβπ) / π][(meetβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§))} | ||
| Theorem | isdlat 18475* | Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ (πΎ β DLat β (πΎ β Lat β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) | ||
| Theorem | dlatmjdi 18476 | In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β DLat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π))) | ||
| Theorem | dlatl 18477 | A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ (πΎ β DLat β πΎ β Lat) | ||
| Theorem | odudlatb 18478 | 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 18479 | In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β DLat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ (π β§ π)) = ((π β¨ π) β§ (π β¨ π))) | ||
| Syntax | cipo 18480 | Class function defining inclusion posets. |
| class toInc | ||
| Definition | df-ipo 18481* |
For any family of sets, define the poset of that family ordered by
inclusion. See ipobas 18484, ipolerval 18485, and ipole 18487 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 = (π β V β¦ β¦{β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} / πβ¦({β¨(Baseβndx), πβ©, β¨(TopSetβndx), (ordTopβπ)β©} βͺ {β¨(leβndx), πβ©, β¨(ocβndx), (π₯ β π β¦ βͺ {π¦ β π β£ (π¦ β© π₯) = β })β©})) | ||
| Theorem | ipostr 18482 | The structure of df-ipo 18481 is a structure defining indices up to 11. (Contributed by Mario Carneiro, 25-Oct-2015.) |
| β’ ({β¨(Baseβndx), π΅β©, β¨(TopSetβndx), π½β©} βͺ {β¨(leβndx), β€ β©, β¨(ocβndx), β₯ β©}) Struct β¨1, ;11β© | ||
| Theorem | ipoval 18483* | Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ πΌ = (toIncβπΉ) & β’ β€ = {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β β’ (πΉ β π β πΌ = ({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx), (ordTopβ β€ )β©} βͺ {β¨(leβndx), β€ β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β })β©})) | ||
| Theorem | ipobas 18484 | Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by Mario Carneiro, 25-Oct-2015.) |
| β’ πΌ = (toIncβπΉ) β β’ (πΉ β π β πΉ = (BaseβπΌ)) | ||
| Theorem | ipolerval 18485* | Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ πΌ = (toIncβπΉ) β β’ (πΉ β π β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} = (leβπΌ)) | ||
| Theorem | ipotset 18486 | Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.) |
| β’ πΌ = (toIncβπΉ) & β’ β€ = (leβπΌ) β β’ (πΉ β π β (ordTopβ β€ ) = (TopSetβπΌ)) | ||
| Theorem | ipole 18487 | Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ πΌ = (toIncβπΉ) & β’ β€ = (leβπΌ) β β’ ((πΉ β π β§ π β πΉ β§ π β πΉ) β (π β€ π β π β π)) | ||
| Theorem | ipolt 18488 | Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ πΌ = (toIncβπΉ) & β’ < = (ltβπΌ) β β’ ((πΉ β π β§ π β πΉ β§ π β πΉ) β (π < π β π β π)) | ||
| Theorem | ipopos 18489 | The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| β’ πΌ = (toIncβπΉ) β β’ πΌ β Poset | ||
| Theorem | isipodrs 18490* | Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| β’ ((toIncβπ΄) β Dirset β (π΄ β V β§ π΄ β β β§ βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ βͺ π¦) β π§)) | ||
| Theorem | ipodrscl 18491 | Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| β’ ((toIncβπ΄) β Dirset β π΄ β V) | ||
| Theorem | ipodrsfi 18492* | Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| β’ (((toIncβπ΄) β Dirset β§ π β π΄ β§ π β Fin) β βπ§ β π΄ βͺ π β π§) | ||
| Theorem | fpwipodrs 18493 | The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| β’ (π΄ β π β (toIncβ(π« π΄ β© Fin)) β Dirset) | ||
| Theorem | ipodrsima 18494* | The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| β’ (π β πΉ Fn π« π΄) & β’ ((π β§ (π’ β π£ β§ π£ β π΄)) β (πΉβπ’) β (πΉβπ£)) & β’ (π β (toIncβπ΅) β Dirset) & β’ (π β π΅ β π« π΄) & β’ (π β (πΉ β π΅) β π) β β’ (π β (toIncβ(πΉ β π΅)) β Dirset) | ||
| Theorem | isacs3lem 18495* | An algebraic closure system satisfies isacs3 18503. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π β πΆ))) | ||
| Theorem | acsdrsel 18496 | An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| β’ ((πΆ β (ACSβπ) β§ π β πΆ β§ (toIncβπ) β Dirset) β βͺ π β πΆ) | ||
| Theorem | isacs4lem 18497* | 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 18498* | 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βπ) β§ βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin)))) | ||
| Theorem | acsdrscl 18499 | In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (ACSβπ) β§ π β π« π β§ (toIncβπ) β Dirset) β (πΉββͺ π) = βͺ (πΉ β π)) | ||
| Theorem | acsficl 18500 | 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βπ) β§ π β π) β (πΉβπ) = βͺ (πΉ β (π« π β© Fin))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |