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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ishlat2 37701* | 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 37702* | 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 37703* | 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 37704 | A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β (πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat)) | ||
Theorem | hloml 37705 | A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OML) | ||
Theorem | hlclat 37706 | A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β CLat) | ||
Theorem | hlcvl 37707 | A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β πΎ β CvLat) | ||
Theorem | hlatl 37708 | A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β AtLat) | ||
Theorem | hlol 37709 | A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OL) | ||
Theorem | hlop 37710 | A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β OP) | ||
Theorem | hllat 37711 | A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β Lat) | ||
Theorem | hllatd 37712 | Deduction form of hllat 37711. A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022.) |
β’ (π β πΎ β HL) β β’ (π β πΎ β Lat) | ||
Theorem | hlomcmat 37713 | A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.) |
β’ (πΎ β HL β (πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat)) | ||
Theorem | hlpos 37714 | A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.) |
β’ (πΎ β HL β πΎ β Poset) | ||
Theorem | hlatjcl 37715 | Closure of join operation. Frequently-used special case of latjcl 18263 for atoms. (Contributed by NM, 15-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β π΅) | ||
Theorem | hlatjcom 37716 | Commutatitivity of join operation. Frequently-used special case of latjcom 18271 for atoms. (Contributed by NM, 15-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) | ||
Theorem | hlatjidm 37717 | Idempotence of join operation. Frequently-used special case of latjcom 18271 for atoms. (Contributed by NM, 15-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) | ||
Theorem | hlatjass 37718 | Lattice join is associative. Frequently-used special case of latjass 18307 for atoms. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = (π β¨ (π β¨ π ))) | ||
Theorem | hlatj12 37719 | Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 18309 for atoms. (Contributed by NM, 4-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π )) = (π β¨ (π β¨ π ))) | ||
Theorem | hlatj32 37720 | Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 18309 for atoms. (Contributed by NM, 21-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = ((π β¨ π ) β¨ π)) | ||
Theorem | hlatjrot 37721 | Rotate lattice join of 3 classes. Frequently-used special case of latjrot 18312 for atoms. (Contributed by NM, 2-Aug-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | hlatj4 37722 | Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 18313 for atoms. (Contributed by NM, 9-Aug-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π ) β¨ (π β¨ π))) | ||
Theorem | hlatlej1 37723 | A join's first argument is less than or equal to the join. Special case of latlej1 18272 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) | ||
Theorem | hlatlej2 37724 | A join's second argument is less than or equal to the join. Special case of latlej2 18273 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) | ||
Theorem | glbconN 37725* | 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 7306. (Revised by SN, 3-Jan-2025.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πΊβπ) = ( β₯ β(πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π}))) | ||
Theorem | glbconNOLD 37726* | Obsolete version of glbconN 37725 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 37727* | De Morgan's law for GLB and LUB. Index-set version of glbconN 37725, where we read π as π(π). (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ πΊ = (glbβπΎ) & β’ β₯ = (ocβπΎ) β β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πΊβ{π₯ β£ βπ β πΌ π₯ = π}) = ( β₯ β(πβ{π₯ β£ βπ β πΌ π₯ = ( β₯ βπ)}))) | ||
Theorem | atnlej1 37728 | 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 37729 | 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 37730* | A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ((π β π β βπ§ β π΄ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π))) β§ βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π)) β π β€ (π§ β¨ π)))) | ||
Theorem | hlexch1 37731 | A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlexch2 37732 | A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlexchb1 37733 | A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlexchb2 37734 | A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlsupr 37735* | 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 37736* | A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β βπ β π΄ (π β¨ π) = (π β¨ π)) | ||
Theorem | hlhgt4 37737* | 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 37738* | 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 37739 | 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 37740 | A Hilbert lattice has the exchange property. (atexch 31109 analog.) (Contributed by NM, 15-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlexch4N 37741 | 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 37742 | A version of hlexchb1 37733 for atoms. (Contributed by NM, 15-Nov-2011.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlatexchb2 37743 | A version of hlexchb2 37734 for atoms. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β (π β¨ π ) = (π β¨ π ))) | ||
Theorem | hlatexch1 37744 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlatexch2 37745 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β π β€ (π β¨ π ))) | ||
Theorem | hlatmstcOLDN 37746* | 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 31090 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πβ{π¦ β π΄ β£ π¦ β€ π}) = π) | ||
Theorem | hlatle 37747* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 31099 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) | ||
Theorem | hlateq 37748* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 31101 analog.) (Contributed by NM, 24-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (βπ β π΄ (π β€ π β π β€ π) β π = π)) | ||
Theorem | hlrelat1 37749* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 31091, with β§ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π < π β βπ β π΄ (Β¬ π β€ π β§ π β€ π))) | ||
Theorem | hlrelat5N 37750* | 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 37751* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 31092 analog.) (Contributed by NM, 4-Feb-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β π΄ (π < (π β¨ π) β§ (π β¨ π) β€ π)) | ||
Theorem | hlrelat2 37752* | A consequence of relative atomicity. (chrelat2i 31093 analog.) (Contributed by NM, 5-Feb-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β βπ β π΄ (π β€ π β§ Β¬ π β€ π))) | ||
Theorem | exatleN 37753 | 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 37754* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β βπ β π΄ βπ β π΄ π β π) | ||
Theorem | atex 37755 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β π΄ β β ) | ||
Theorem | intnatN 37756 | 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 37757 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π)) β (π β¨ π) β (π β¨ π)) | ||
Theorem | 2llnneN 37758 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) β (π β¨ π)) | ||
Theorem | cvr1 37759 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 31083 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) | ||
Theorem | cvr2N 37760 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 31084 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (π < (π β¨ π) β ππΆ(π β¨ π))) | ||
Theorem | hlrelat3 37761* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 37751. (Contributed by NM, 2-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) | ||
Theorem | cvrval3 37762* | Binary relation expressing π covers π. (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆπ β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = π))) | ||
Theorem | cvrval4N 37763* | Binary relation expressing π covers π. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ βπ β π΄ (π β¨ π) = π))) | ||
Theorem | cvrval5 37764* | Binary relation expressing π covers π β§ π. (Contributed by NM, 7-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β βπ β π΄ (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π))) | ||
Theorem | cvrp 37765 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 31103 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β ((π β§ π) = 0 β ππΆ(π β¨ π))) | ||
Theorem | atcvr1 37766 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | atcvr2 37767 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvrexchlem 37768 | Lemma for cvrexch 37769. (cvexchlem 31096 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) | ||
Theorem | cvrexch 37769 | 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 31097 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) | ||
Theorem | cvratlem 37770 | Lemma for cvrat 37771. (atcvatlem 31113 analog.) (Contributed by NM, 22-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β 0 β§ π < (π β¨ π))) β (Β¬ π(leβπΎ)π β π β π΄)) | ||
Theorem | cvrat 37771 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 31114 analog.) (Contributed by NM, 22-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π < (π β¨ π)) β π β π΄)) | ||
Theorem | ltltncvr 37772 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β Β¬ ππΆπ)) | ||
Theorem | ltcvrntr 37773 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ ππΆπ) β Β¬ ππΆπ)) | ||
Theorem | cvrntr 37774 | The covers relation is not transitive. (cvntr 31020 analog.) (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ππΆπ β§ ππΆπ) β Β¬ ππΆπ)) | ||
Theorem | atcvr0eq 37775 | The covers relation is not transitive. (atcv0eq 31107 analog.) (Contributed by NM, 29-Nov-2011.) |
β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( 0 πΆ(π β¨ π) β π = π)) | ||
Theorem | lnnat 37776 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β Β¬ (π β¨ π) β π΄)) | ||
Theorem | atcvrj0 37777 | Two atoms covering the zero subspace are equal. (atcv1 31108 analog.) (Contributed by NM, 29-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄) β§ ππΆ(π β¨ π)) β (π = 0 β π = π)) | ||
Theorem | cvrat2 37778 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 31115 analog.) (Contributed by NM, 30-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ ππΆ(π β¨ π))) β π β π΄) | ||
Theorem | atcvrneN 37779 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ππΆ(π β¨ π )) β π β π ) | ||
Theorem | atcvrj1 37780 | 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 37781 | 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 37782 | 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 37783 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β€ (π β¨ π ))) β π β π ) | ||
Theorem | atltcvr 37784 | An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012.) |
β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π < (π β¨ π ) β ππΆ(π β¨ π ))) | ||
Theorem | atle 37785* | Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β 0 ) β βπ β π΄ π β€ π) | ||
Theorem | atlt 37786 | 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 37787 | Transfer less-than relation from one atom to another. (Contributed by NM, 7-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π < π) | ||
Theorem | 2atlt 37788* | 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 37789 | Atom exchange property. Version of hlatexch2 37745 with covers relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (ππΆ(π β¨ π ) β ππΆ(π β¨ π ))) | ||
Theorem | atexchltN 37790 | Atom exchange property. Version of hlatexch2 37745 with less-than ordering. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π < (π β¨ π ) β π < (π β¨ π ))) | ||
Theorem | cvrat3 37791 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 31124 analog.) (Contributed by NM, 30-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β (π β§ (π β¨ π)) β π΄)) | ||
Theorem | cvrat4 37792* | A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in [PtakPulmannova] p. 68. Also Lemma 9.2(delta) in [MaedaMaeda] p. 41. (atcvat4i 31125 analog.) (Contributed by NM, 30-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) | ||
Theorem | cvrat42 37793* | Commuted version of cvrat4 37792. (Contributed by NM, 28-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) | ||
Theorem | 2atjm 37794 | The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π)) β ((π β¨ π) β§ π) = π) | ||
Theorem | atbtwn 37795 | Property of a 3rd atom π on a line π β¨ π intersecting element π at π. (Contributed by NM, 30-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) β (π β π β Β¬ π β€ π)) | ||
Theorem | atbtwnexOLDN 37796* | There exists a 3rd atom π on a line π β¨ π intersecting element π at π, such that π is different from π and not in π. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β€ π β§ Β¬ π β€ π)) β βπ β π΄ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) | ||
Theorem | atbtwnex 37797* | Given atoms π in π and π not in π, there exists an atom π not in π such that the line π β¨ π intersects π at π. (Contributed by NM, 1-Aug-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β€ π β§ Β¬ π β€ π)) β βπ β π΄ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) | ||
Theorem | 3noncolr2 37798 | Two ways to express 3 non-colinear atoms (rotated right 2 places). (Contributed by NM, 12-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π ))) | ||
Theorem | 3noncolr1N 37799 | Two ways to express 3 non-colinear atoms (rotated right 1 place). (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π))) | ||
Theorem | hlatcon3 37800 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |