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