Home | Metamath
Proof Explorer Theorem List (p. 378 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cvlsupr3 37701 | Two equivalent ways of expressing that π is a superposition of π and π, which can replace the superposition part of ishlat1 37709, (π₯ β π¦ β βπ§ β π΄(π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦)) ), with the simpler βπ§ β π΄(π₯ β¨ π§) = (π¦ β¨ π§) as shown in ishlat3N 37711. (Contributed by NM, 5-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π ) = (π β¨ π ) β (π β π β (π β π β§ π β π β§ π β€ (π β¨ π))))) | ||
Theorem | cvlsupr4 37702 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β€ (π β¨ π)) | ||
Theorem | cvlsupr5 37703 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β π) | ||
Theorem | cvlsupr6 37704 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 9-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β π β π) | ||
Theorem | cvlsupr7 37705 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 24-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cvlsupr8 37706 | Consequence of superposition condition (π β¨ π ) = (π β¨ π ). (Contributed by NM, 24-Nov-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π ) = (π β¨ π ))) β (π β¨ π) = (π β¨ π )) | ||
Syntax | chlt 37707 | Extend class notation with Hilbert lattices. |
class HL | ||
Definition | df-hlat 37708* | Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012.) |
β’ HL = {π β ((OML β© CLat) β© CvLat) β£ (βπ β (Atomsβπ)βπ β (Atomsβπ)(π β π β βπ β (Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π))) β§ βπ β (Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ))))} | ||
Theorem | ishlat1 37709* | The predicate "is a Hilbert lattice", which is: is orthomodular (πΎ β OML), complete (πΎ β CLat), atomic and satisfies the exchange (or covering) property (πΎ β CvLat), satisfies the superposition principle, and has a minimum height of 4 (witnessed here by 0, x, y, z, 1). (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) | ||
Theorem | ishlat2 37710* | The predicate "is a Hilbert lattice". Here we replace πΎ β CvLat with the weaker πΎ β AtLat and show the exchange property explicitly. (Contributed by NM, 5-Nov-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ (βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) | ||
Theorem | ishlat3N 37711* | The predicate "is a Hilbert lattice". Note that the superposition principle is expressed in the compact form βπ§ β π΄(π₯ β¨ π§) = (π¦ β¨ π§). The exchange property and atomicity are provided by πΎ β CvLat, and "minimum height 4" is shown explicitly. (Contributed by NM, 8-Nov-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ β¨ π§) = (π¦ β¨ π§) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) | ||
Theorem | ishlatiN 37712* | Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.) |
β’ πΎ β OML & β’ πΎ β CLat & β’ πΎ β AtLat & β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯))) & β’ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )) β β’ πΎ β HL | ||
Theorem | hlomcmcv 37713 | A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β (πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat)) | ||
Theorem | hloml 37714 | A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OML) | ||
Theorem | hlclat 37715 | A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β CLat) | ||
Theorem | hlcvl 37716 | A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β πΎ β CvLat) | ||
Theorem | hlatl 37717 | A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β AtLat) | ||
Theorem | hlol 37718 | A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OL) | ||
Theorem | hlop 37719 | A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OP) | ||
Theorem | hllat 37720 | A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β Lat) | ||
Theorem | hllatd 37721 | Deduction form of hllat 37720. A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022.) |
β’ (π β πΎ β HL) β β’ (π β πΎ β Lat) | ||
Theorem | hlomcmat 37722 | A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β (πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat)) | ||
Theorem | hlpos 37723 | A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β Poset) | ||
Theorem | hlatjcl 37724 | Closure of join operation. Frequently-used special case of latjcl 18262 for atoms. (Contributed by NM, 15-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β π΅) | ||
Theorem | hlatjcom 37725 | Commutatitivity of join operation. Frequently-used special case of latjcom 18270 for atoms. (Contributed by NM, 15-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) | ||
Theorem | hlatjidm 37726 | Idempotence of join operation. Frequently-used special case of latjcom 18270 for atoms. (Contributed by NM, 15-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) | ||
Theorem | hlatjass 37727 | Lattice join is associative. Frequently-used special case of latjass 18306 for atoms. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = (π β¨ (π β¨ π ))) | ||
Theorem | hlatj12 37728 | Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 18308 for atoms. (Contributed by NM, 4-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π )) = (π β¨ (π β¨ π ))) | ||
Theorem | hlatj32 37729 | Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 18308 for atoms. (Contributed by NM, 21-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = ((π β¨ π ) β¨ π)) | ||
Theorem | hlatjrot 37730 | Rotate lattice join of 3 classes. Frequently-used special case of latjrot 18311 for atoms. (Contributed by NM, 2-Aug-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | hlatj4 37731 | Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 18312 for atoms. (Contributed by NM, 9-Aug-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π ) β¨ (π β¨ π))) | ||
Theorem | hlatlej1 37732 | A join's first argument is less than or equal to the join. Special case of latlej1 18271 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) | ||
Theorem | hlatlej2 37733 | A join's second argument is less than or equal to the join. Special case of latlej2 18272 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) | ||
Theorem | glbconN 37734* | De Morgan's law for GLB and LUB. This holds in any complete ortholattice, although we assume HL for convenience. (Contributed by NM, 17-Jan-2012.) New df-riota 7305. (Revised by SN, 3-Jan-2025.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πΊβπ) = ( β₯ β(πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π}))) | ||
Theorem | glbconNOLD 37735* | Obsolete version of glbconN 37734 as of 3-Jan-2025. (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πΊβπ) = ( β₯ β(πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π}))) | ||
Theorem | glbconxN 37736* | De Morgan's law for GLB and LUB. Index-set version of glbconN 37734, where we read π as π(π). (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πΊβ{π₯ β£ βπ β πΌ π₯ = π}) = ( β₯ β(πβ{π₯ β£ βπ β πΌ π₯ = ( β₯ βπ)}))) | ||
Theorem | atnlej1 37737 | If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π )) β π β π) | ||
Theorem | atnlej2 37738 | If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π )) β π β π ) | ||
Theorem | hlsuprexch 37739* | A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ((π β π β βπ§ β π΄ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π))) β§ βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π)) β π β€ (π§ β¨ π)))) | ||
Theorem | hlexch1 37740 | A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlexch2 37741 | A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlexchb1 37742 | A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlexchb2 37743 | A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlsupr 37744* | A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β βπ β π΄ (π β π β§ π β π β§ π β€ (π β¨ π))) | ||
Theorem | hlsupr2 37745* | A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β βπ β π΄ (π β¨ π) = (π β¨ π)) | ||
Theorem | hlhgt4 37746* | A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) β β’ (πΎ β HL β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))) | ||
Theorem | hlhgt2 37747* | A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) β β’ (πΎ β HL β βπ₯ β π΅ ( 0 < π₯ β§ π₯ < 1 )) | ||
Theorem | hl0lt1N 37748 | Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011.) (New usage is discouraged.) |
β’ < = (ltβπΎ) & β’ 0 = (0.βπΎ) & β’ 1 = (1.βπΎ) β β’ (πΎ β HL β 0 < 1 ) | ||
Theorem | hlexch3 37749 | A Hilbert lattice has the exchange property. (atexch 31121 analog.) (Contributed by NM, 15-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlexch4N 37750 | A Hilbert lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 15-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlatexchb1 37751 | A version of hlexchb1 37742 for atoms. (Contributed by NM, 15-Nov-2011.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlatexchb2 37752 | A version of hlexchb2 37743 for atoms. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β (π β¨ π ) = (π β¨ π ))) | ||
Theorem | hlatexch1 37753 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlatexch2 37754 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β π β€ (π β¨ π ))) | ||
Theorem | hlatmstcOLDN 37755* | An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in [Kalmbach] p. 140; also remark in [BeltramettiCassinelli] p. 98. (hatomistici 31102 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πβ{π¦ β π΄ β£ π¦ β€ π}) = π) | ||
Theorem | hlatle 37756* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 31111 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) | ||
Theorem | hlateq 37757* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 31113 analog.) (Contributed by NM, 24-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (βπ β π΄ (π β€ π β π β€ π) β π = π)) | ||
Theorem | hlrelat1 37758* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 31103, with β§ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π < π β βπ β π΄ (Β¬ π β€ π β§ π β€ π))) | ||
Theorem | hlrelat5N 37759* | An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of [Kalmbach] p. 149. (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β π΄ (π < (π β¨ π) β§ π β€ π)) | ||
Theorem | hlrelat 37760* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 31104 analog.) (Contributed by NM, 4-Feb-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β π΄ (π < (π β¨ π) β§ (π β¨ π) β€ π)) | ||
Theorem | hlrelat2 37761* | A consequence of relative atomicity. (chrelat2i 31105 analog.) (Contributed by NM, 5-Feb-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β βπ β π΄ (π β€ π β§ Β¬ π β€ π))) | ||
Theorem | exatleN 37762 | A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) β (π β€ π β π = π)) | ||
Theorem | hl2at 37763* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β βπ β π΄ βπ β π΄ π β π) | ||
Theorem | atex 37764 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β π΄ β β ) | ||
Theorem | intnatN 37765 | If the intersection with a non-majorizing element is an atom, the intersecting element is not an atom. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ (π β§ π) β π΄)) β Β¬ π β π΄) | ||
Theorem | 2llnne2N 37766 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π)) β (π β¨ π) β (π β¨ π)) | ||
Theorem | 2llnneN 37767 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) β (π β¨ π)) | ||
Theorem | cvr1 37768 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 31095 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) | ||
Theorem | cvr2N 37769 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 31096 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (π < (π β¨ π) β ππΆ(π β¨ π))) | ||
Theorem | hlrelat3 37770* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 37760. (Contributed by NM, 2-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) | ||
Theorem | cvrval3 37771* | Binary relation expressing π covers π. (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆπ β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = π))) | ||
Theorem | cvrval4N 37772* | Binary relation expressing π covers π. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ βπ β π΄ (π β¨ π) = π))) | ||
Theorem | cvrval5 37773* | Binary relation expressing π covers π β§ π. (Contributed by NM, 7-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β βπ β π΄ (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π))) | ||
Theorem | cvrp 37774 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 31115 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β ((π β§ π) = 0 β ππΆ(π β¨ π))) | ||
Theorem | atcvr1 37775 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | atcvr2 37776 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvrexchlem 37777 | Lemma for cvrexch 37778. (cvexchlem 31108 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) | ||
Theorem | cvrexch 37778 | A Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (cvexchi 31109 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) | ||
Theorem | cvratlem 37779 | Lemma for cvrat 37780. (atcvatlem 31125 analog.) (Contributed by NM, 22-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β 0 β§ π < (π β¨ π))) β (Β¬ π(leβπΎ)π β π β π΄)) | ||
Theorem | cvrat 37780 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 31126 analog.) (Contributed by NM, 22-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π < (π β¨ π)) β π β π΄)) | ||
Theorem | ltltncvr 37781 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β Β¬ ππΆπ)) | ||
Theorem | ltcvrntr 37782 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ ππΆπ) β Β¬ ππΆπ)) | ||
Theorem | cvrntr 37783 | The covers relation is not transitive. (cvntr 31032 analog.) (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ππΆπ β§ ππΆπ) β Β¬ ππΆπ)) | ||
Theorem | atcvr0eq 37784 | The covers relation is not transitive. (atcv0eq 31119 analog.) (Contributed by NM, 29-Nov-2011.) |
β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( 0 πΆ(π β¨ π) β π = π)) | ||
Theorem | lnnat 37785 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β Β¬ (π β¨ π) β π΄)) | ||
Theorem | atcvrj0 37786 | Two atoms covering the zero subspace are equal. (atcv1 31120 analog.) (Contributed by NM, 29-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄) β§ ππΆ(π β¨ π)) β (π = 0 β π = π)) | ||
Theorem | cvrat2 37787 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 31127 analog.) (Contributed by NM, 30-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ ππΆ(π β¨ π))) β π β π΄) | ||
Theorem | atcvrneN 37788 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ππΆ(π β¨ π )) β π β π ) | ||
Theorem | atcvrj1 37789 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β€ (π β¨ π ))) β ππΆ(π β¨ π )) | ||
Theorem | atcvrj2b 37790 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β π β§ π β€ (π β¨ π )) β ππΆ(π β¨ π ))) | ||
Theorem | atcvrj2 37791 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β€ (π β¨ π ))) β ππΆ(π β¨ π )) | ||
Theorem | atleneN 37792 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β€ (π β¨ π ))) β π β π ) | ||
Theorem | atltcvr 37793 | An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012.) |
β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π < (π β¨ π ) β ππΆ(π β¨ π ))) | ||
Theorem | atle 37794* | Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β 0 ) β βπ β π΄ π β€ π) | ||
Theorem | atlt 37795 | Two atoms are unequal iff their join is greater than one of them. (Contributed by NM, 6-May-2012.) |
β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π < (π β¨ π) β π β π)) | ||
Theorem | atlelt 37796 | Transfer less-than relation from one atom to another. (Contributed by NM, 7-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π < π) | ||
Theorem | 2atlt 37797* | Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΅) β§ π < π) β βπ β π΄ (π β π β§ π < π)) | ||
Theorem | atexchcvrN 37798 | Atom exchange property. Version of hlatexch2 37754 with covers relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (ππΆ(π β¨ π ) β ππΆ(π β¨ π ))) | ||
Theorem | atexchltN 37799 | Atom exchange property. Version of hlatexch2 37754 with less-than ordering. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π < (π β¨ π ) β π < (π β¨ π ))) | ||
Theorem | cvrat3 37800 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 31136 analog.) (Contributed by NM, 30-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β (π β§ (π β¨ π)) β π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |