![]() |
Metamath
Proof Explorer Theorem List (p. 184 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-join 18301* | Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.) |
β’ join = (π β V β¦ {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦} (lubβπ)π§}) | ||
Definition | df-meet 18302* | Define poset meet. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.) |
β’ meet = (π β V β¦ {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦} (glbβπ)π§}) | ||
Theorem | lubfval 18303* | Value of the least upper bound function of a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) & β’ (π β πΎ β π) β β’ (π β π = ((π β π« π΅ β¦ (β©π₯ β π΅ π)) βΎ {π β£ β!π₯ β π΅ π})) | ||
Theorem | lubdm 18304* | Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) & β’ (π β πΎ β π) β β’ (π β dom π = {π β π« π΅ β£ β!π₯ β π΅ π}) | ||
Theorem | lubfun 18305 | The LUB is a function. (Contributed by NM, 9-Sep-2018.) |
β’ π = (lubβπΎ) β β’ Fun π | ||
Theorem | lubeldm 18306* | Member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) & β’ (π β πΎ β π) β β’ (π β (π β dom π β (π β π΅ β§ β!π₯ β π΅ π))) | ||
Theorem | lubelss 18307 | A member of the domain of the least upper bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β πΎ β π) & β’ (π β π β dom π) β β’ (π β π β π΅) | ||
Theorem | lubeu 18308* | Unique existence proper of a member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) & β’ (π β πΎ β π) & β’ (π β π β dom π) β β’ (π β β!π₯ β π΅ π) | ||
Theorem | lubval 18309* | Value of the least upper bound function of a poset. Out-of-domain arguments (those not satisfying π β dom π) are allowed for convenience, evaluating to the empty set. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) & β’ (π β πΎ β π) & β’ (π β π β π΅) β β’ (π β (πβπ) = (β©π₯ β π΅ π)) | ||
Theorem | lubcl 18310 | The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ (π β πΎ β π) & β’ (π β π β dom π) β β’ (π β (πβπ) β π΅) | ||
Theorem | lubprop 18311* | Properties of greatest lower bound of a poset. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β πΎ β π) & β’ (π β π β dom π) β β’ (π β (βπ¦ β π π¦ β€ (πβπ) β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§))) | ||
Theorem | luble 18312 | The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β πΎ β π) & β’ (π β π β dom π) & β’ (π β π β π) β β’ (π β π β€ (πβπ)) | ||
Theorem | lublecllem 18313* | Lemma for lublecl 18314 and lubid 18315. (Contributed by NM, 8-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β πΎ β Poset) & β’ (π β π β π΅) β β’ ((π β§ π₯ β π΅) β ((βπ§ β {π¦ β π΅ β£ π¦ β€ π}π§ β€ π₯ β§ βπ€ β π΅ (βπ§ β {π¦ β π΅ β£ π¦ β€ π}π§ β€ π€ β π₯ β€ π€)) β π₯ = π)) | ||
Theorem | lublecl 18314* | The set of all elements less than a given element has an LUB. (Contributed by NM, 8-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β πΎ β Poset) & β’ (π β π β π΅) β β’ (π β {π¦ β π΅ β£ π¦ β€ π} β dom π) | ||
Theorem | lubid 18315* | The LUB of elements less than or equal to a fixed value equals that value. (Contributed by NM, 19-Oct-2011.) (Revised by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ (π β πΎ β Poset) & β’ (π β π β π΅) β β’ (π β (πβ{π¦ β π΅ β£ π¦ β€ π}) = π) | ||
Theorem | glbfval 18316* | Value of the greatest lower function of a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) & β’ (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) & β’ (π β πΎ β π) β β’ (π β πΊ = ((π β π« π΅ β¦ (β©π₯ β π΅ π)) βΎ {π β£ β!π₯ β π΅ π})) | ||
Theorem | glbdm 18317* | Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) & β’ (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) & β’ (π β πΎ β π) β β’ (π β dom πΊ = {π β π« π΅ β£ β!π₯ β π΅ π}) | ||
Theorem | glbfun 18318 | The GLB is a function. (Contributed by NM, 9-Sep-2018.) |
β’ πΊ = (glbβπΎ) β β’ Fun πΊ | ||
Theorem | glbeldm 18319* | Member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) & β’ (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) & β’ (π β πΎ β π) β β’ (π β (π β dom πΊ β (π β π΅ β§ β!π₯ β π΅ π))) | ||
Theorem | glbelss 18320 | A member of the domain of the greatest lower bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) & β’ (π β πΎ β π) & β’ (π β π β dom πΊ) β β’ (π β π β π΅) | ||
Theorem | glbeu 18321* | Unique existence proper of a member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) & β’ (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) & β’ (π β πΎ β π) & β’ (π β π β dom πΊ) β β’ (π β β!π₯ β π΅ π) | ||
Theorem | glbval 18322* | Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying π β dom π) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΊ = (glbβπΎ) & β’ (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) & β’ (π β πΎ β π) & β’ (π β π β π΅) β β’ (π β (πΊβπ) = (β©π₯ β π΅ π)) | ||
Theorem | glbcl 18323 | The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ (π β πΎ β π) & β’ (π β π β dom πΊ) β β’ (π β (πΊβπ) β π΅) | ||
Theorem | glbprop 18324* | Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (glbβπΎ) & β’ (π β πΎ β π) & β’ (π β π β dom π) β β’ (π β (βπ¦ β π (πβπ) β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ (πβπ)))) | ||
Theorem | glble 18325 | The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (glbβπΎ) & β’ (π β πΎ β π) & β’ (π β π β dom π) & β’ (π β π β π) β β’ (π β (πβπ) β€ π) | ||
Theorem | joinfval 18326* | Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 18327 first to reduce net proof size (existence part)? |
β’ π = (lubβπΎ) & β’ β¨ = (joinβπΎ) β β’ (πΎ β π β β¨ = {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§}) | ||
Theorem | joinfval2 18327* | Value of join function for a poset-type structure. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
β’ π = (lubβπΎ) & β’ β¨ = (joinβπΎ) β β’ (πΎ β π β β¨ = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}) | ||
Theorem | joindm 18328* | Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.) |
β’ π = (lubβπΎ) & β’ β¨ = (joinβπΎ) β β’ (πΎ β π β dom β¨ = {β¨π₯, π¦β© β£ {π₯, π¦} β dom π}) | ||
Theorem | joindef 18329 | Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.) |
β’ π = (lubβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (β¨π, πβ© β dom β¨ β {π, π} β dom π)) | ||
Theorem | joinval 18330 | Join value. Since both sides evaluate to β when they don't exist, for convenience we drop the {π, π} β dom π requirement. (Contributed by NM, 9-Sep-2018.) |
β’ π = (lubβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β¨ π) = (πβ{π, π})) | ||
Theorem | joincl 18331 | Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β¨ ) β β’ (π β (π β¨ π) β π΅) | ||
Theorem | joindmss 18332 | Subset property of domain of join. (Contributed by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) β β’ (π β dom β¨ β (π΅ Γ π΅)) | ||
Theorem | joinval2lem 18333* | Lemma for joinval2 18334 and joineu 18335. (Contributed by NM, 12-Sep-2018.) TODO: combine this through joineu 18335 into joinlem 18336? |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ ((π β π΅ β§ π β π΅) β ((βπ¦ β {π, π}π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β {π, π}π¦ β€ π§ β π₯ β€ π§)) β ((π β€ π₯ β§ π β€ π₯) β§ βπ§ β π΅ ((π β€ π§ β§ π β€ π§) β π₯ β€ π§)))) | ||
Theorem | joinval2 18334* | Value of join for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 11-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β¨ π) = (β©π₯ β π΅ ((π β€ π₯ β§ π β€ π₯) β§ βπ§ β π΅ ((π β€ π§ β§ π β€ π§) β π₯ β€ π§)))) | ||
Theorem | joineu 18335* | Uniqueness of join of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β¨ ) β β’ (π β β!π₯ β π΅ ((π β€ π₯ β§ π β€ π₯) β§ βπ§ β π΅ ((π β€ π§ β§ π β€ π§) β π₯ β€ π§))) | ||
Theorem | joinlem 18336* | Lemma for join properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β¨ ) β β’ (π β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ βπ§ β π΅ ((π β€ π§ β§ π β€ π§) β (π β¨ π) β€ π§))) | ||
Theorem | lejoin1 18337 | A join's first argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β¨ ) β β’ (π β π β€ (π β¨ π)) | ||
Theorem | lejoin2 18338 | A join's second argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β¨ ) β β’ (π β π β€ (π β¨ π)) | ||
Theorem | joinle 18339 | A join is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ (π β πΎ β Poset) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β¨ ) β β’ (π β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) | ||
Theorem | meetfval 18340* | Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove meetfval2 18341 first to reduce net proof size (existence part)? |
β’ πΊ = (glbβπΎ) & β’ β§ = (meetβπΎ) β β’ (πΎ β π β β§ = {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}πΊπ§}) | ||
Theorem | meetfval2 18341* | Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
β’ πΊ = (glbβπΎ) & β’ β§ = (meetβπΎ) β β’ (πΎ β π β β§ = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}) | ||
Theorem | meetdm 18342* | Domain of meet function for a poset-type structure. (Contributed by NM, 16-Sep-2018.) |
β’ πΊ = (glbβπΎ) & β’ β§ = (meetβπΎ) β β’ (πΎ β π β dom β§ = {β¨π₯, π¦β© β£ {π₯, π¦} β dom πΊ}) | ||
Theorem | meetdef 18343 | Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018.) |
β’ πΊ = (glbβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (β¨π, πβ© β dom β§ β {π, π} β dom πΊ)) | ||
Theorem | meetval 18344 | Meet value. Since both sides evaluate to β when they don't exist, for convenience we drop the {π, π} β dom πΊ requirement. (Contributed by NM, 9-Sep-2018.) |
β’ πΊ = (glbβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β§ π) = (πΊβ{π, π})) | ||
Theorem | meetcl 18345 | Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β§ ) β β’ (π β (π β§ π) β π΅) | ||
Theorem | meetdmss 18346 | Subset property of domain of meet. (Contributed by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) β β’ (π β dom β§ β (π΅ Γ π΅)) | ||
Theorem | meetval2lem 18347* | Lemma for meetval2 18348 and meeteu 18349. (Contributed by NM, 12-Sep-2018.) TODO: combine this through meeteu 18349 into meetlem 18350? |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ ((π β π΅ β§ π β π΅) β ((βπ¦ β {π, π}π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β {π, π}π§ β€ π¦ β π§ β€ π₯)) β ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)))) | ||
Theorem | meetval2 18348* | Value of meet for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 11-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β§ π) = (β©π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)))) | ||
Theorem | meeteu 18349* | Uniqueness of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β§ ) β β’ (π β β!π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯))) | ||
Theorem | meetlem 18350* | Lemma for meet properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β§ ) β β’ (π β (((π β§ π) β€ π β§ (π β§ π) β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π)))) | ||
Theorem | lemeet1 18351 | A meet's first argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β§ ) β β’ (π β (π β§ π) β€ π) | ||
Theorem | lemeet2 18352 | A meet's second argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β§ ) β β’ (π β (π β§ π) β€ π) | ||
Theorem | meetle 18353 | A meet is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β Poset) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β β¨π, πβ© β dom β§ ) β β’ (π β ((π β€ π β§ π β€ π) β π β€ (π β§ π))) | ||
Theorem | joincomALT 18354 | The join of a poset is commutative. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 16-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β π β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) | ||
Theorem | joincom 18355 | The join of a poset is commutative. (The antecedent β¨π, πβ© β dom β¨ β§ β¨π, πβ© β dom β¨ i.e., "the joins exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ (β¨π, πβ© β dom β¨ β§ β¨π, πβ© β dom β¨ )) β (π β¨ π) = (π β¨ π)) | ||
Theorem | meetcomALT 18356 | The meet of a poset is commutative. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 17-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β π β§ π β π΅ β§ π β π΅) β (π β§ π) = (π β§ π)) | ||
Theorem | meetcom 18357 | The meet of a poset is commutative. (The antecedent β¨π, πβ© β dom β§ β§ β¨π, πβ© β dom β§ i.e., "the meets exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 17-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ (β¨π, πβ© β dom β§ β§ β¨π, πβ© β dom β§ )) β (π β§ π) = (π β§ π)) | ||
Theorem | join0 18358 | Lemma for odumeet 18363. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ (joinββ ) = β | ||
Theorem | meet0 18359 | Lemma for odujoin 18361. (Contributed by Stefan O'Rear, 29-Jan-2015.) TODO (df-riota 7365 update): This proof increased from 152 bytes to 547 bytes after the df-riota 7365 change. Any way to shorten it? join0 18358 also. |
β’ (meetββ ) = β | ||
Theorem | odulub 18360 | Least upper bounds in a dual order are greatest lower bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ πΏ = (glbβπ) β β’ (π β π β πΏ = (lubβπ·)) | ||
Theorem | odujoin 18361 | Joins in a dual order are meets in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ β§ = (meetβπ) β β’ β§ = (joinβπ·) | ||
Theorem | oduglb 18362 | Greatest lower bounds in a dual order are least upper bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ π = (lubβπ) β β’ (π β π β π = (glbβπ·)) | ||
Theorem | odumeet 18363 | Meets in a dual order are joins in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ β¨ = (joinβπ) β β’ β¨ = (meetβπ·) | ||
Theorem | poslubmo 18364* | Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.) |
β’ β€ = (leβπΎ) & β’ π΅ = (BaseβπΎ) β β’ ((πΎ β Poset β§ π β π΅) β β*π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) | ||
Theorem | posglbmo 18365* | Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018.) |
β’ β€ = (leβπΎ) & β’ π΅ = (BaseβπΎ) β β’ ((πΎ β Poset β§ π β π΅) β β*π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) | ||
Theorem | poslubd 18366* | Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ β€ = (leβπΎ) & β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ (π β πΎ β Poset) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ ((π β§ π₯ β π) β π₯ β€ π) & β’ ((π β§ π¦ β π΅ β§ βπ₯ β π π₯ β€ π¦) β π β€ π¦) β β’ (π β (πβπ) = π) | ||
Theorem | poslubdg 18367* | Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ β€ = (leβπΎ) & β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π = (lubβπΎ)) & β’ (π β πΎ β Poset) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ ((π β§ π₯ β π) β π₯ β€ π) & β’ ((π β§ π¦ β π΅ β§ βπ₯ β π π₯ β€ π¦) β π β€ π¦) β β’ (π β (πβπ) = π) | ||
Theorem | posglbdg 18368* | Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ β€ = (leβπΎ) & β’ (π β π΅ = (BaseβπΎ)) & β’ (π β πΊ = (glbβπΎ)) & β’ (π β πΎ β Poset) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ ((π β§ π₯ β π) β π β€ π₯) & β’ ((π β§ π¦ β π΅ β§ βπ₯ β π π¦ β€ π₯) β π¦ β€ π) β β’ (π β (πΊβπ) = π) | ||
Syntax | ctos 18369 | Extend class notation with the class of all tosets. |
class Toset | ||
Definition | df-toset 18370* | Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014.) |
β’ Toset = {π β Poset β£ [(Baseβπ) / π][(leβπ) / π]βπ₯ β π βπ¦ β π (π₯ππ¦ β¨ π¦ππ₯)} | ||
Theorem | istos 18371* | The predicate "is a toset". (Contributed by FL, 17-Nov-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Toset β (πΎ β Poset β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β¨ π¦ β€ π₯))) | ||
Theorem | tosso 18372 | Write the totally ordered set structure predicate in terms of the proper class strict order predicate. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ (πΎ β π β (πΎ β Toset β ( < Or π΅ β§ ( I βΎ π΅) β β€ ))) | ||
Theorem | tospos 18373 | A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ (πΉ β Toset β πΉ β Poset) | ||
Theorem | tleile 18374 | In a Toset, any two elements are comparable. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π β€ π β¨ π β€ π)) | ||
Theorem | tltnle 18375 | In a Toset, "less than" is equivalent to the negation of the converse of "less than or equal to", see pltnle 18291. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π < π β Β¬ π β€ π)) | ||
Syntax | cp0 18376 | Extend class notation with poset zero. |
class 0. | ||
Syntax | cp1 18377 | Extend class notation with poset unit. |
class 1. | ||
Definition | df-p0 18378 | Define poset zero. (Contributed by NM, 12-Oct-2011.) |
β’ 0. = (π β V β¦ ((glbβπ)β(Baseβπ))) | ||
Definition | df-p1 18379 | Define poset unit. (Contributed by NM, 22-Oct-2011.) |
β’ 1. = (π β V β¦ ((lubβπ)β(Baseβπ))) | ||
Theorem | p0val 18380 | Value of poset zero. (Contributed by NM, 12-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ 0 = (0.βπΎ) β β’ (πΎ β π β 0 = (πΊβπ΅)) | ||
Theorem | p1val 18381 | Value of poset zero. (Contributed by NM, 22-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ 1 = (1.βπΎ) β β’ (πΎ β π β 1 = (πβπ΅)) | ||
Theorem | p0le 18382 | Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011.) (Revised by NM, 13-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π΅ β dom πΊ) β β’ (π β 0 β€ π) | ||
Theorem | ple1 18383 | Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011.) (Revised by NM, 13-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ β€ = (leβπΎ) & β’ 1 = (1.βπΎ) & β’ (π β πΎ β π) & β’ (π β π β π΅) & β’ (π β π΅ β dom π) β β’ (π β π β€ 1 ) | ||
Syntax | clat 18384 | Extend class notation with the class of all lattices. |
class Lat | ||
Definition | df-lat 18385 | Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
β’ Lat = {π β Poset β£ (dom (joinβπ) = ((Baseβπ) Γ (Baseβπ)) β§ dom (meetβπ) = ((Baseβπ) Γ (Baseβπ)))} | ||
Theorem | islat 18386 | The predicate "is a lattice". (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ (πΎ β Lat β (πΎ β Poset β§ (dom β¨ = (π΅ Γ π΅) β§ dom β§ = (π΅ Γ π΅)))) | ||
Theorem | odulatb 18387 | Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) β β’ (π β π β (π β Lat β π· β Lat)) | ||
Theorem | odulat 18388 | Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) β β’ (π β Lat β π· β Lat) | ||
Theorem | latcl2 18389 | The join and meet of any two elements exist. (Contributed by NM, 14-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ (π β πΎ β Lat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (β¨π, πβ© β dom β¨ β§ β¨π, πβ© β dom β§ )) | ||
Theorem | latlem 18390 | Lemma for lattice properties. (Contributed by NM, 14-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β ((π β¨ π) β π΅ β§ (π β§ π) β π΅)) | ||
Theorem | latpos 18391 | A lattice is a poset. (Contributed by NM, 17-Sep-2011.) |
β’ (πΎ β Lat β πΎ β Poset) | ||
Theorem | latjcl 18392 | Closure of join operation in a lattice. (chjcom 30759 analog.) (Contributed by NM, 14-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) | ||
Theorem | latmcl 18393 | Closure of meet operation in a lattice. (incom 4202 analog.) (Contributed by NM, 14-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) | ||
Theorem | latref 18394 | A lattice ordering is reflexive. (ssid 4005 analog.) (Contributed by NM, 8-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Lat β§ π β π΅) β π β€ π) | ||
Theorem | latasymb 18395 | A lattice ordering is asymmetric. (eqss 3998 analog.) (Contributed by NM, 22-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β ((π β€ π β§ π β€ π) β π = π)) | ||
Theorem | latasym 18396 | A lattice ordering is asymmetric. (eqss 3998 analog.) (Contributed by NM, 8-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β ((π β€ π β§ π β€ π) β π = π)) | ||
Theorem | lattr 18397 | A lattice ordering is transitive. (sstr 3991 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ π)) | ||
Theorem | latasymd 18398 | Deduce equality from lattice ordering. (eqssd 4000 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ (π β πΎ β Lat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β€ π) & β’ (π β π β€ π) β β’ (π β π = π) | ||
Theorem | lattrd 18399 | A lattice ordering is transitive. Deduction version of lattr 18397. (Contributed by NM, 3-Sep-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ (π β πΎ β Lat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β€ π) & β’ (π β π β€ π) β β’ (π β π β€ π) | ||
Theorem | latjcom 18400 | The join of a lattice commutes. (chjcom 30759 analog.) (Contributed by NM, 16-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |