![]() |
Metamath
Proof Explorer Theorem List (p. 186 of 484) | < 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: | ![]() (1-30772) |
![]() (30773-32295) |
![]() (32296-48350) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lublem 18501* | Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β (βπ¦ β π π¦ β€ (πβπ) β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§))) | ||
Theorem | lubub 18502 | The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β π β€ (πβπ)) | ||
Theorem | lubl 18503* | The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π΅) β (βπ¦ β π π¦ β€ π β (πβπ) β€ π)) | ||
Theorem | lubss 18504 | Subset law for least upper bounds. (chsupss 31196 analog.) (Contributed by NM, 20-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β (πβπ) β€ (πβπ)) | ||
Theorem | lubel 18505 | 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 18506 | The LUB of a union. (Contributed by NM, 5-Mar-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π = (lubβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π΅) β (πβ(π βͺ π)) = ((πβπ) β¨ (πβπ))) | ||
Theorem | clatglb 18507* | Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅) β (βπ¦ β π (πΊβπ) β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ (πΊβπ)))) | ||
Theorem | clatglble 18508 | The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β (πΊβπ) β€ π) | ||
Theorem | clatleglb 18509* | 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 18510 | Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) β β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β (πΊβπ) β€ (πΊβπ)) | ||
Syntax | cdlat 18511 | The class of distributive lattices. |
class DLat | ||
Definition | df-dlat 18512* | A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 18488) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ DLat = {π β Lat β£ [(Baseβπ) / π][(joinβπ) / π][(meetβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§))} | ||
Theorem | isdlat 18513* | Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ (πΎ β DLat β (πΎ β Lat β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) | ||
Theorem | dlatmjdi 18514 | In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β DLat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π))) | ||
Theorem | dlatl 18515 | A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ (πΎ β DLat β πΎ β Lat) | ||
Theorem | odudlatb 18516 | 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 18517 | In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β DLat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ (π β§ π)) = ((π β¨ π) β§ (π β¨ π))) | ||
Syntax | cipo 18518 | Class function defining inclusion posets. |
class toInc | ||
Definition | df-ipo 18519* |
For any family of sets, define the poset of that family ordered by
inclusion. See ipobas 18522, ipolerval 18523, and ipole 18525 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 18520 | The structure of df-ipo 18519 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 18521* | 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 18522 | 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 18523* | Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ πΌ = (toIncβπΉ) β β’ (πΉ β π β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} = (leβπΌ)) | ||
Theorem | ipotset 18524 | Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.) |
β’ πΌ = (toIncβπΉ) & β’ β€ = (leβπΌ) β β’ (πΉ β π β (ordTopβ β€ ) = (TopSetβπΌ)) | ||
Theorem | ipole 18525 | Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ πΌ = (toIncβπΉ) & β’ β€ = (leβπΌ) β β’ ((πΉ β π β§ π β πΉ β§ π β πΉ) β (π β€ π β π β π)) | ||
Theorem | ipolt 18526 | Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ πΌ = (toIncβπΉ) & β’ < = (ltβπΌ) β β’ ((πΉ β π β§ π β πΉ β§ π β πΉ) β (π < π β π β π)) | ||
Theorem | ipopos 18527 | The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ πΌ = (toIncβπΉ) β β’ πΌ β Poset | ||
Theorem | isipodrs 18528* | Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ ((toIncβπ΄) β Dirset β (π΄ β V β§ π΄ β β β§ βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ βͺ π¦) β π§)) | ||
Theorem | ipodrscl 18529 | Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ ((toIncβπ΄) β Dirset β π΄ β V) | ||
Theorem | ipodrsfi 18530* | Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (((toIncβπ΄) β Dirset β§ π β π΄ β§ π β Fin) β βπ§ β π΄ βͺ π β π§) | ||
Theorem | fpwipodrs 18531 | The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (π΄ β π β (toIncβ(π« π΄ β© Fin)) β Dirset) | ||
Theorem | ipodrsima 18532* | The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (π β πΉ Fn π« π΄) & β’ ((π β§ (π’ β π£ β§ π£ β π΄)) β (πΉβπ’) β (πΉβπ£)) & β’ (π β (toIncβπ΅) β Dirset) & β’ (π β π΅ β π« π΄) & β’ (π β (πΉ β π΅) β π) β β’ (π β (toIncβ(πΉ β π΅)) β Dirset) | ||
Theorem | isacs3lem 18533* | An algebraic closure system satisfies isacs3 18541. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π β πΆ))) | ||
Theorem | acsdrsel 18534 | An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ ((πΆ β (ACSβπ) β§ π β πΆ β§ (toIncβπ) β Dirset) β βͺ π β πΆ) | ||
Theorem | isacs4lem 18535* | 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 18536* | 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 18537 | In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (ACSβπ) β§ π β π« π β§ (toIncβπ) β Dirset) β (πΉββͺ π) = βͺ (πΉ β π)) | ||
Theorem | acsficl 18538 | 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 18539* | 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)))) | ||
Theorem | isacs4 18540* | A closure system is algebraic iff closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« π« π((toIncβπ ) β Dirset β (πΉββͺ π ) = βͺ (πΉ β π )))) | ||
Theorem | isacs3 18541* | A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π β πΆ))) | ||
Theorem | acsficld 18542 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 18538. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) β β’ (π β (πβπ) = βͺ (π β (π« π β© Fin))) | ||
Theorem | acsficl2d 18543* | In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 18538. Deduction form. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) β β’ (π β (π β (πβπ) β βπ₯ β (π« π β© Fin)π β (πβπ₯))) | ||
Theorem | acsfiindd 18544 | In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β π) β β’ (π β (π β πΌ β (π« π β© Fin) β πΌ)) | ||
Theorem | acsmapd 18545* | In an algebraic closure system, if π is contained in the closure of π, there is a map π from π into the set of finite subsets of π such that the closure of βͺ ran π contains π. This is proven by applying acsficl2d 18543 to each element of π. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) & β’ (π β π β (πβπ)) β β’ (π β βπ(π:πβΆ(π« π β© Fin) β§ π β (πββͺ ran π))) | ||
Theorem | acsmap2d 18546* | In an algebraic closure system, if π and π have the same closure and π is independent, then there is a map π from π into the set of finite subsets of π such that π equals the union of ran π. This is proven by taking the map π from acsmapd 18545 and observing that, since π and π have the same closure, the closure of βͺ ran π must contain π. Since π is independent, by mrissmrcd 17619, βͺ ran π must equal π. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ (π β (πβπ) = (πβπ)) β β’ (π β βπ(π:πβΆ(π« π β© Fin) β§ π = βͺ ran π)) | ||
Theorem | acsinfd 18547 | In an algebraic closure system, if π and π have the same closure and π is infinite independent, then π is infinite. This follows from applying unirnffid 9368 to the map given in acsmap2d 18546. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ (π β (πβπ) = (πβπ)) & β’ (π β Β¬ π β Fin) β β’ (π β Β¬ π β Fin) | ||
Theorem | acsdomd 18548 | In an algebraic closure system, if π and π have the same closure and π is infinite independent, then π dominates π. This follows from applying acsinfd 18547 and then applying unirnfdomd 10590 to the map given in acsmap2d 18546. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ (π β (πβπ) = (πβπ)) & β’ (π β Β¬ π β Fin) β β’ (π β π βΌ π) | ||
Theorem | acsinfdimd 18549 | In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 18548 twice with acsinfd 18547. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β πΌ) & β’ (π β π β πΌ) & β’ (π β (πβπ) = (πβπ)) & β’ (π β Β¬ π β Fin) β β’ (π β π β π) | ||
Theorem | acsexdimd 18550* | In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 17629 for the finite case and acsinfdimd 18549 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β βπ β π« πβπ¦ β π βπ§ β ((πβ(π βͺ {π¦})) β (πβπ ))π¦ β (πβ(π βͺ {π§}))) & β’ (π β π β πΌ) & β’ (π β π β πΌ) & β’ (π β (πβπ) = (πβπ)) β β’ (π β π β π) | ||
Theorem | mrelatglb 18551 | Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatglbALT 48119 for an alternate proof. |
β’ πΌ = (toIncβπΆ) & β’ πΊ = (glbβπΌ) β β’ ((πΆ β (Mooreβπ) β§ π β πΆ β§ π β β ) β (πΊβπ) = β© π) | ||
Theorem | mrelatglb0 18552 | The empty intersection in a Moore space is realized by the base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΌ = (toIncβπΆ) & β’ πΊ = (glbβπΌ) β β’ (πΆ β (Mooreβπ) β (πΊββ ) = π) | ||
Theorem | mrelatlub 18553 | Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatlubALT 48118 for an alternate proof. |
β’ πΌ = (toIncβπΆ) & β’ πΉ = (mrClsβπΆ) & β’ πΏ = (lubβπΌ) β β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (πΏβπ) = (πΉββͺ π)) | ||
Theorem | mreclatBAD 18554* | A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7372 update): Reprove using isclat 18491 instead of the isclatBAD. hypothesis. See commented-out mreclat above. See mreclat 48120 for a good version. |
β’ πΌ = (toIncβπΆ) & β’ (πΌ β CLat β (πΌ β Poset β§ βπ₯(π₯ β (BaseβπΌ) β (((lubβπΌ)βπ₯) β (BaseβπΌ) β§ ((glbβπΌ)βπ₯) β (BaseβπΌ))))) β β’ (πΆ β (Mooreβπ) β πΌ β CLat) | ||
See commented-out notes for lattices as relations. | ||
Syntax | cps 18555 | Extend class notation with the class of all posets. |
class PosetRel | ||
Syntax | ctsr 18556 | Extend class notation with the class of all totally ordered sets. |
class TosetRel | ||
Definition | df-ps 18557 | Define the class of all posets (partially ordered sets) with weak ordering (e.g., "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.) |
β’ PosetRel = {π β£ (Rel π β§ (π β π) β π β§ (π β© β‘π) = ( I βΎ βͺ βͺ π))} | ||
Definition | df-tsr 18558 | Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.) |
β’ TosetRel = {π β PosetRel β£ (dom π Γ dom π) β (π βͺ β‘π)} | ||
Theorem | isps 18559 | The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.) |
β’ (π β π΄ β (π β PosetRel β (Rel π β§ (π β π ) β π β§ (π β© β‘π ) = ( I βΎ βͺ βͺ π )))) | ||
Theorem | psrel 18560 | A poset is a relation. (Contributed by NM, 12-May-2008.) |
β’ (π΄ β PosetRel β Rel π΄) | ||
Theorem | psref2 18561 | A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.) |
β’ (π β PosetRel β (π β© β‘π ) = ( I βΎ βͺ βͺ π )) | ||
Theorem | pstr2 18562 | A poset is transitive. (Contributed by FL, 3-Aug-2009.) |
β’ (π β PosetRel β (π β π ) β π ) | ||
Theorem | pslem 18563 | Lemma for psref 18565 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ (π β PosetRel β (((π΄π π΅ β§ π΅π πΆ) β π΄π πΆ) β§ (π΄ β βͺ βͺ π β π΄π π΄) β§ ((π΄π π΅ β§ π΅π π΄) β π΄ = π΅))) | ||
Theorem | psdmrn 18564 | The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.) |
β’ (π β PosetRel β (dom π = βͺ βͺ π β§ ran π = βͺ βͺ π )) | ||
Theorem | psref 18565 | A poset is reflexive. (Contributed by NM, 13-May-2008.) |
β’ π = dom π β β’ ((π β PosetRel β§ π΄ β π) β π΄π π΄) | ||
Theorem | psrn 18566 | The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.) |
β’ π = dom π β β’ (π β PosetRel β π = ran π ) | ||
Theorem | psasym 18567 | A poset is antisymmetric. (Contributed by NM, 12-May-2008.) |
β’ ((π β PosetRel β§ π΄π π΅ β§ π΅π π΄) β π΄ = π΅) | ||
Theorem | pstr 18568 | A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ ((π β PosetRel β§ π΄π π΅ β§ π΅π πΆ) β π΄π πΆ) | ||
Theorem | cnvps 18569 | The converse of a poset is a poset. In the general case (β‘π β PosetRel β π β PosetRel) is not true. See cnvpsb 18570 for a special case where the property holds. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 3-Sep-2015.) |
β’ (π β PosetRel β β‘π β PosetRel) | ||
Theorem | cnvpsb 18570 | The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.) |
β’ (Rel π β (π β PosetRel β β‘π β PosetRel)) | ||
Theorem | psss 18571 | Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.) |
β’ (π β PosetRel β (π β© (π΄ Γ π΄)) β PosetRel) | ||
Theorem | psssdm2 18572 | Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π β β’ (π β PosetRel β dom (π β© (π΄ Γ π΄)) = (π β© π΄)) | ||
Theorem | psssdm 18573 | Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π β β’ ((π β PosetRel β§ π΄ β π) β dom (π β© (π΄ Γ π΄)) = π΄) | ||
Theorem | istsr 18574 | The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π = dom π β β’ (π β TosetRel β (π β PosetRel β§ (π Γ π) β (π βͺ β‘π ))) | ||
Theorem | istsr2 18575* | The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π = dom π β β’ (π β TosetRel β (π β PosetRel β§ βπ₯ β π βπ¦ β π (π₯π π¦ β¨ π¦π π₯))) | ||
Theorem | tsrlin 18576 | A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π β β’ ((π β TosetRel β§ π΄ β π β§ π΅ β π) β (π΄π π΅ β¨ π΅π π΄)) | ||
Theorem | tsrlemax 18577 | Two ways of saying a number is less than or equal to the maximum of two others. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π β β’ ((π β TosetRel β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π if(π΅π πΆ, πΆ, π΅) β (π΄π π΅ β¨ π΄π πΆ))) | ||
Theorem | tsrps 18578 | A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ (π β TosetRel β π β PosetRel) | ||
Theorem | cnvtsr 18579 | The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β TosetRel β β‘π β TosetRel ) | ||
Theorem | tsrss 18580 | Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Nov-2013.) |
β’ (π β TosetRel β (π β© (π΄ Γ π΄)) β TosetRel ) | ||
Theorem | ledm 18581 | The domain of β€ is β*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.) |
β’ β* = dom β€ | ||
Theorem | lern 18582 | The range of β€ is β*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ β* = ran β€ | ||
Theorem | lefld 18583 | The field of the 'less or equal to' relationship on the extended real. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.) |
β’ β* = βͺ βͺ β€ | ||
Theorem | letsr 18584 | The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ β€ β TosetRel | ||
Syntax | cdir 18585 | Extend class notation with the class of directed sets. |
class DirRel | ||
Syntax | ctail 18586 | Extend class notation with the tail function for directed sets. |
class tail | ||
Definition | df-dir 18587 | Define the class of directed sets (the order relation itself is sometimes called a direction, and a directed set is a set equipped with a direction). (Contributed by Jeff Hankins, 25-Nov-2009.) |
β’ DirRel = {π β£ ((Rel π β§ ( I βΎ βͺ βͺ π) β π) β§ ((π β π) β π β§ (βͺ βͺ π Γ βͺ βͺ π) β (β‘π β π)))} | ||
Definition | df-tail 18588* | Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.) |
β’ tail = (π β DirRel β¦ (π₯ β βͺ βͺ π β¦ (π β {π₯}))) | ||
Theorem | isdir 18589 | A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π΄ = βͺ βͺ π β β’ (π β π β (π β DirRel β ((Rel π β§ ( I βΎ π΄) β π ) β§ ((π β π ) β π β§ (π΄ Γ π΄) β (β‘π β π ))))) | ||
Theorem | reldir 18590 | A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ (π β DirRel β Rel π ) | ||
Theorem | dirdm 18591 | A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ (π β DirRel β dom π = βͺ βͺ π ) | ||
Theorem | dirref 18592 | A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π = dom π β β’ ((π β DirRel β§ π΄ β π) β π΄π π΄) | ||
Theorem | dirtr 18593 | A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ (((π β DirRel β§ πΆ β π) β§ (π΄π π΅ β§ π΅π πΆ)) β π΄π πΆ) | ||
Theorem | dirge 18594* | For any two elements of a directed set, there exists a third element greater than or equal to both. Note that this does not say that the two elements have a least upper bound. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π = dom π β β’ ((π β DirRel β§ π΄ β π β§ π΅ β π) β βπ₯ β π (π΄π π₯ β§ π΅π π₯)) | ||
Theorem | tsrdir 18595 | A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ (π΄ β TosetRel β π΄ β DirRel) | ||
According to Wikipedia ("Magma (algebra)", 08-Jan-2020, https://en.wikipedia.org/wiki/magma_(algebra)) "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.". Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following: With df-mpo 7421, binary operations are defined by a rule, and with df-ov 7419, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation 7419 (19-Jan-2020), "... a binary operation on a set π is a mapping of the elements of the Cartesian product π Γ π to S: π:π Γ πβΆπ. Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, binary operations mapping the elements of the Cartesian product π Γ π are more precisely called internal binary operations. If, in addition, the result is also contained in the set π, the operation should be called closed internal binary operation. Therefore, a "binary operation on a set π" according to Wikipedia is a "closed internal binary operation" in a more precise terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations 7419). The definition of magmas (Mgm, see df-mgm 18599) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible. | ||
Syntax | cplusf 18596 | Extend class notation with group addition as a function. |
class +π | ||
Syntax | cmgm 18597 | Extend class notation with class of all magmas. |
class Mgm | ||
Definition | df-plusf 18598* | Define group addition function. Usually we will use +g directly instead of +π, and they have the same behavior in most cases. The main advantage of +π for any magma is that it is a guaranteed function (mgmplusf 18609), while +g only has closure (mgmcl 18602). (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ +π = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(+gβπ)π¦))) | ||
Definition | df-mgm 18599* | A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ Mgm = {π β£ [(Baseβπ) / π][(+gβπ) / π]βπ₯ β π βπ¦ β π (π₯ππ¦) β π} | ||
Theorem | ismgm 18600* | The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β π β (π β Mgm β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |