![]() |
Metamath
Proof Explorer Theorem List (p. 183 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 | ||
Syntax | chof 18201 | Extend class notation with the Hom functor. |
class HomF | ||
Syntax | cyon 18202 | Extend class notation with the Yoneda embedding. |
class Yon | ||
Definition | df-hof 18203* | Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCatβπΆ) Γ πΆ to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ HomF = (π β Cat β¦ β¨(Homf βπ), β¦(Baseβπ) / πβ¦(π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π))))β©) | ||
Definition | df-yon 18204 | Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ Yon = (π β Cat β¦ (β¨π, (oppCatβπ)β© curryF (HomFβ(oppCatβπ)))) | ||
Theorem | hofval 18205* | Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCatβπΆ) Γ πΆ to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ (π β πΆ β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) β β’ (π β π = β¨(Homf βπΆ), (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β© Β· (2nd βπ¦))π))))β©) | ||
Theorem | hof1fval 18206 | The object part of the Hom functor is the Homf operation, which is just a functionalized version of Hom. That is, it is a two argument function, which maps π, π to the set of morphisms from π to π. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ (π β πΆ β Cat) β β’ (π β (1st βπ) = (Homf βπΆ)) | ||
Theorem | hof1 18207 | The object part of the Hom functor maps π, π to the set of morphisms from π to π. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ (π β πΆ β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π(1st βπ)π) = (ππ»π)) | ||
Theorem | hof2fval 18208* | The morphism part of the Hom functor, for morphisms β¨π, πβ©:β¨π, πβ©βΆβ¨π, πβ© (which since the first argument is contravariant means morphisms π:πβΆπ and π:πβΆπ), yields a function (a morphism of SetCat) mapping β:πβΆπ to π β β β π:πβΆπ. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ (π β πΆ β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ Β· = (compβπΆ) β β’ (π β (β¨π, πβ©(2nd βπ)β¨π, πβ©) = (π β (ππ»π), π β (ππ»π) β¦ (β β (ππ»π) β¦ ((π(β¨π, πβ© Β· π)β)(β¨π, πβ© Β· π)π)))) | ||
Theorem | hof2val 18209* | The morphism part of the Hom functor, for morphisms β¨π, πβ©:β¨π, πβ©βΆβ¨π, πβ© (which since the first argument is contravariant means morphisms π:πβΆπ and π:πβΆπ), yields a function (a morphism of SetCat) mapping β:πβΆπ to π β β β π:πβΆπ. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ (π β πΆ β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ Β· = (compβπΆ) & β’ (π β πΉ β (ππ»π)) & β’ (π β πΊ β (ππ»π)) β β’ (π β (πΉ(β¨π, πβ©(2nd βπ)β¨π, πβ©)πΊ) = (β β (ππ»π) β¦ ((πΊ(β¨π, πβ© Β· π)β)(β¨π, πβ© Β· π)πΉ))) | ||
Theorem | hof2 18210 | The morphism part of the Hom functor, for morphisms β¨π, πβ©:β¨π, πβ©βΆβ¨π, πβ© (which since the first argument is contravariant means morphisms π:πβΆπ and π:πβΆπ), yields a function (a morphism of SetCat) mapping β:πβΆπ to π β β β π:πβΆπ. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ (π β πΆ β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ Β· = (compβπΆ) & β’ (π β πΉ β (ππ»π)) & β’ (π β πΊ β (ππ»π)) & β’ (π β πΎ β (ππ»π)) β β’ (π β ((πΉ(β¨π, πβ©(2nd βπ)β¨π, πβ©)πΊ)βπΎ) = ((πΊ(β¨π, πβ© Β· π)πΎ)(β¨π, πβ© Β· π)πΉ)) | ||
Theorem | hofcllem 18211 | Lemma for hofcl 18212. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ π = (oppCatβπΆ) & β’ π· = (SetCatβπ) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΎ β (ππ»π)) & β’ (π β πΏ β (ππ»π)) & β’ (π β π β (ππ»π)) & β’ (π β π β (ππ»π)) β β’ (π β ((πΎ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(2nd βπ)β¨π, πβ©)(π(β¨π, πβ©(compβπΆ)π)πΏ)) = ((π(β¨π, πβ©(2nd βπ)β¨π, πβ©)π)(β¨(ππ»π), (ππ»π)β©(compβπ·)(ππ»π))(πΎ(β¨π, πβ©(2nd βπ)β¨π, πβ©)πΏ))) | ||
Theorem | hofcl 18212 | Closure of the Hom functor. Note that the codomain is the category SetCatβπ for any universe π which contains each Hom-set. This corresponds to the assertion that πΆ be locally small (with respect to π). (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ π = (oppCatβπΆ) & β’ π· = (SetCatβπ) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) β β’ (π β π β ((π Γc πΆ) Func π·)) | ||
Theorem | oppchofcl 18213 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (HomFβπ) & β’ π· = (SetCatβπ) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) β β’ (π β π β ((πΆ Γc π) Func π·)) | ||
Theorem | yonval 18214 | Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (YonβπΆ) & β’ (π β πΆ β Cat) & β’ π = (oppCatβπΆ) & β’ π = (HomFβπ) β β’ (π β π = (β¨πΆ, πβ© curryF π)) | ||
Theorem | yoncl 18215 | The Yoneda embedding is a functor from the category to the category π of presheaves on πΆ. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (YonβπΆ) & β’ (π β πΆ β Cat) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) β β’ (π β π β (πΆ Func π)) | ||
Theorem | yon1cl 18216 | The Yoneda embedding at an object of πΆ is a presheaf on πΆ, also known as the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) β β’ (π β ((1st βπ)βπ) β (π Func π)) | ||
Theorem | yon11 18217 | Value of the Yoneda embedding at an object. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) β β’ (π β ((1st β((1st βπ)βπ))βπ) = (ππ»π)) | ||
Theorem | yon12 18218 | Value of the Yoneda embedding at a morphism. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ»π)) & β’ (π β πΊ β (ππ»π)) β β’ (π β (((π(2nd β((1st βπ)βπ))π)βπΉ)βπΊ) = (πΊ(β¨π, πβ© Β· π)πΉ)) | ||
Theorem | yon2 18219 | Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ»π)) & β’ (π β πΊ β (ππ»π)) β β’ (π β ((((π(2nd βπ)π)βπΉ)βπ)βπΊ) = (πΉ(β¨π, πβ© Β· π)πΊ)) | ||
Theorem | hofpropd 18220 | If two categories have the same set of objects, morphisms, and compositions, then they have the same Hom functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β (HomFβπΆ) = (HomFβπ·)) | ||
Theorem | yonpropd 18221 | If two categories have the same set of objects, morphisms, and compositions, then they have the same Yoneda functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β (YonβπΆ) = (Yonβπ·)) | ||
Theorem | oppcyon 18222 | Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (Yonβπ) & β’ π = (HomFβπΆ) & β’ (π β πΆ β Cat) β β’ (π β π = (β¨π, πΆβ© curryF π)) | ||
Theorem | oyoncl 18223 | The opposite Yoneda embedding is a functor from oppCatβπΆ to the functor category πΆ β SetCat. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (Yonβπ) & β’ (π β πΆ β Cat) & β’ π = (SetCatβπ) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ π = (πΆ FuncCat π) β β’ (π β π β (π Func π)) | ||
Theorem | oyon1cl 18224 | The opposite Yoneda embedding at an object of πΆ is a functor from πΆ to Set, also known as the covariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (Yonβπ) & β’ (π β πΆ β Cat) & β’ π = (SetCatβπ) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π΅) β β’ (π β ((1st βπ)βπ) β (πΆ Func π)) | ||
Theorem | yonedalem1 18225 | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) β β’ (π β (π β ((π Γc π) Func π) β§ πΈ β ((π Γc π) Func π))) | ||
Theorem | yonedalem21 18226 | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ (π β πΉ β (π Func π)) & β’ (π β π β π΅) β β’ (π β (πΉ(1st βπ)π) = (((1st βπ)βπ)(π Nat π)πΉ)) | ||
Theorem | yonedalem3a 18227* | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ (π β πΉ β (π Func π)) & β’ (π β π β π΅) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) β β’ (π β ((πΉππ) = (π β (((1st βπ)βπ)(π Nat π)πΉ) β¦ ((πβπ)β( 1 βπ))) β§ (πΉππ):(πΉ(1st βπ)π)βΆ(πΉ(1st βπΈ)π))) | ||
Theorem | yonedalem4a 18228* | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ (π β πΉ β (π Func π)) & β’ (π β π β π΅) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’))))) & β’ (π β π΄ β ((1st βπΉ)βπ)) β β’ (π β ((πΉππ)βπ΄) = (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π) β¦ (((π(2nd βπΉ)π¦)βπ)βπ΄)))) | ||
Theorem | yonedalem4b 18229* | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ (π β πΉ β (π Func π)) & β’ (π β π β π΅) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’))))) & β’ (π β π΄ β ((1st βπΉ)βπ)) & β’ (π β π β π΅) & β’ (π β πΊ β (π(Hom βπΆ)π)) β β’ (π β ((((πΉππ)βπ΄)βπ)βπΊ) = (((π(2nd βπΉ)π)βπΊ)βπ΄)) | ||
Theorem | yonedalem4c 18230* | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ (π β πΉ β (π Func π)) & β’ (π β π β π΅) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’))))) & β’ (π β π΄ β ((1st βπΉ)βπ)) β β’ (π β ((πΉππ)βπ΄) β (((1st βπ)βπ)(π Nat π)πΉ)) | ||
Theorem | yonedalem22 18231 | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ (π β πΉ β (π Func π)) & β’ (π β π β π΅) & β’ (π β πΊ β (π Func π)) & β’ (π β π β π΅) & β’ (π β π΄ β (πΉ(π Nat π)πΊ)) & β’ (π β πΎ β (π(Hom βπΆ)π)) β β’ (π β (π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ) = (((π(2nd βπ)π)βπΎ)(β¨((1st βπ)βπ), πΉβ©(2nd βπ»)β¨((1st βπ)βπ), πΊβ©)π΄)) | ||
Theorem | yonedalem3b 18232* | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ (π β πΉ β (π Func π)) & β’ (π β π β π΅) & β’ (π β πΊ β (π Func π)) & β’ (π β π β π΅) & β’ (π β π΄ β (πΉ(π Nat π)πΊ)) & β’ (π β πΎ β (π(Hom βπΆ)π)) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) β β’ (π β ((πΊππ)(β¨(πΉ(1st βπ)π), (πΊ(1st βπ)π)β©(compβπ)(πΊ(1st βπΈ)π))(π΄(β¨πΉ, πβ©(2nd βπ)β¨πΊ, πβ©)πΎ)) = ((π΄(β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)πΎ)(β¨(πΉ(1st βπ)π), (πΉ(1st βπΈ)π)β©(compβπ)(πΊ(1st βπΈ)π))(πΉππ))) | ||
Theorem | yonedalem3 18233* | Lemma for yoneda 18236. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) β β’ (π β π β (π((π Γc π) Nat π)πΈ)) | ||
Theorem | yonedainv 18234* | The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) & β’ πΌ = (Invβπ ) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’))))) β β’ (π β π(ππΌπΈ)π) | ||
Theorem | yonffthlem 18235* | Lemma for yonffth 18237. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) & β’ πΌ = (Invβπ ) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π’ β ((1st βπ)βπ₯) β¦ (π¦ β π΅ β¦ (π β (π¦(Hom βπΆ)π₯) β¦ (((π₯(2nd βπ)π¦)βπ)βπ’))))) β β’ (π β π β ((πΆ Full π) β© (πΆ Faith π))) | ||
Theorem | yoneda 18236* | The Yoneda Lemma. There is a natural isomorphism between the functors π and πΈ, where π(πΉ, π) is the natural transformations from Yon(π) = Hom ( β , π) to πΉ, and πΈ(πΉ, π) = πΉ(π) is the evaluation functor. Here we need two universes to state the claim: the smaller universe π is used for forming the functor category π = πΆ op β SetCat(π), which itself does not (necessarily) live in π but instead is an element of the larger universe π. (If π is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set π = π in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ π» = (HomFβπ) & β’ π = ((π Γc π) FuncCat π) & β’ πΈ = (π evalF π) & β’ π = (π» βfunc ((β¨(1st βπ), tpos (2nd βπ)β© βfunc (π 2ndF π)) β¨,β©F (π 1stF π))) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β (ran (Homf βπ) βͺ π) β π) & β’ π = (π β (π Func π), π₯ β π΅ β¦ (π β (((1st βπ)βπ₯)(π Nat π)π) β¦ ((πβπ₯)β( 1 βπ₯)))) & β’ πΌ = (Isoβπ ) β β’ (π β π β (ππΌπΈ)) | ||
Theorem | yonffth 18237 | The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category πΆ as a full subcategory of the category π of presheaves on πΆ. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π = (π FuncCat π) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) β β’ (π β π β ((πΆ Full π) β© (πΆ Faith π))) | ||
Theorem | yoniso 18238* | If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from πΆ into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π = (oppCatβπΆ) & β’ π = (SetCatβπ) & β’ π· = (CatCatβπ) & β’ π΅ = (Baseβπ·) & β’ πΌ = (Isoβπ·) & β’ π = (π FuncCat π) & β’ πΈ = (π βΎs ran (1st βπ)) & β’ (π β π β π) & β’ (π β πΆ β π΅) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ (π β πΈ β π΅) & β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (πΉβ(π₯(Hom βπΆ)π¦)) = π¦) β β’ (π β π β (πΆπΌπΈ)) | ||
Syntax | codu 18239 | Class function defining dual orders. |
class ODual | ||
Definition | df-odu 18240 |
Define the dual of an ordered structure, which replaces the order
component of the structure with its reverse. See odubas 18244, oduleval 18242,
and oduleg 18243 for its principal properties.
EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18448. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ ODual = (π€ β V β¦ (π€ sSet β¨(leβndx), β‘(leβπ€)β©)) | ||
Theorem | oduval 18241 | Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ β€ = (leβπ) β β’ π· = (π sSet β¨(leβndx), β‘ β€ β©) | ||
Theorem | oduleval 18242 | Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ β€ = (leβπ) β β’ β‘ β€ = (leβπ·) | ||
Theorem | oduleg 18243 | Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ β€ = (leβπ) & β’ πΊ = (leβπ·) β β’ ((π΄ β π β§ π΅ β π) β (π΄πΊπ΅ β π΅ β€ π΄)) | ||
Theorem | odubas 18244 | Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Proof shortened by AV, 12-Nov-2024.) |
β’ π· = (ODualβπ) & β’ π΅ = (Baseβπ) β β’ π΅ = (Baseβπ·) | ||
Theorem | odubasOLD 18245 | Obsolete proof of odubas 18244 as of 12-Nov-2024. Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = (ODualβπ) & β’ π΅ = (Baseβπ) β β’ π΅ = (Baseβπ·) | ||
Syntax | cproset 18246 | Extend class notation with the class of all prosets. |
class Proset | ||
Syntax | cdrs 18247 | Extend class notation with the class of all directed sets. |
class Dirset | ||
Definition | df-proset 18248* |
Define the class of preordered sets, or prosets. A proset is a set
equipped with a preorder, that is, a transitive and reflexive relation.
Preorders are a natural generalization of partial orders which need not be antisymmetric: there may be pairs of elements such that each is "less than or equal to" the other, so that both elements have the same order-theoretic properties (in some sense, there is a "tie" among them). If a preorder is required to be antisymmetric, that is, there is no such "tie", then one obtains a partial order. If a preorder is required to be symmetric, that is, all comparable elements are tied, then one obtains an equivalence relation. Every preorder naturally factors into these two notions: the "tie" relation on a proset is an equivalence relation, and the quotient under that equivalence relation is a partial order. (Contributed by FL, 17-Nov-2014.) (Revised by Stefan O'Rear, 31-Jan-2015.) |
β’ Proset = {π β£ [(Baseβπ) / π][(leβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§))} | ||
Definition | df-drs 18249* |
Define the class of directed sets. A directed set is a nonempty
preordered set where every pair of elements have some upper bound. Note
that it is not required that there exist a least upper bound.
There is no consensus in the literature over whether directed sets are allowed to be empty. It is slightly more convenient for us if they are not. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ Dirset = {π β Proset β£ [(Baseβπ) / π][(leβπ) / π](π β β β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§))} | ||
Theorem | isprs 18250* | Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Proset β (πΎ β V β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) | ||
Theorem | prslem 18251 | Lemma for prsref 18252 and prstr 18253. (Contributed by Mario Carneiro, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Proset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β§ ((π β€ π β§ π β€ π) β π β€ π))) | ||
Theorem | prsref 18252 | "Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Proset β§ π β π΅) β π β€ π) | ||
Theorem | prstr 18253 | "Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Proset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ π β€ π)) β π β€ π) | ||
Theorem | isdrs 18254* | Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Dirset β (πΎ β Proset β§ π΅ β β β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§))) | ||
Theorem | drsdir 18255* | Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Dirset β§ π β π΅ β§ π β π΅) β βπ§ β π΅ (π β€ π§ β§ π β€ π§)) | ||
Theorem | drsprs 18256 | A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (πΎ β Dirset β πΎ β Proset ) | ||
Theorem | drsbn0 18257 | The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) β β’ (πΎ β Dirset β π΅ β β ) | ||
Theorem | drsdirfi 18258* | Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18249 first comes into play; without it we would need an additional constraint that π not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Dirset β§ π β π΅ β§ π β Fin) β βπ¦ β π΅ βπ§ β π π§ β€ π¦) | ||
Theorem | isdrs2 18259* | Directed sets may be defined in terms of finite subsets. Again, without nonemptiness we would need to restrict to nonempty subsets here. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Dirset β (πΎ β Proset β§ βπ₯ β (π« π΅ β© Fin)βπ¦ β π΅ βπ§ β π₯ π§ β€ π¦)) | ||
Syntax | cpo 18260 | Extend class notation with the class of posets. |
class Poset | ||
Syntax | cplt 18261 | Extend class notation with less-than for posets. |
class lt | ||
Syntax | club 18262 | Extend class notation with poset least upper bound. |
class lub | ||
Syntax | cglb 18263 | Extend class notation with poset greatest lower bound. |
class glb | ||
Syntax | cjn 18264 | Extend class notation with poset join. |
class join | ||
Syntax | cmee 18265 | Extend class notation with poset meet. |
class meet | ||
Definition | df-poset 18266* |
Define the class of partially ordered sets (posets). A poset is a set
equipped with a partial order, that is, a binary relation which is
reflexive, antisymmetric, and transitive. Unlike a total order, in a
partial order there may be pairs of elements where neither precedes the
other. Definition of poset in [Crawley] p. 1. Note that
Crawley-Dilworth require that a poset base set be nonempty, but we
follow the convention of most authors who don't make this a requirement.
In our formalism of extensible structures, the base set of a poset π is denoted by (Baseβπ) and its partial order by (leβπ) (for "less than or equal to"). The quantifiers βπβπ provide a notational shorthand to allow to refer to the base and ordering relation as π and π in the definition rather than having to repeat (Baseβπ) and (leβπ) throughout. These quantifiers can be eliminated with ceqsex2v 3531 and related theorems. (Contributed by NM, 18-Oct-2012.) |
β’ Poset = {π β£ βπβπ(π = (Baseβπ) β§ π = (leβπ) β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)))} | ||
Theorem | ispos 18267* | The predicate "is a poset". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Poset β (πΎ β V β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦) β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) | ||
Theorem | ispos2 18268* |
A poset is an antisymmetric proset.
EDITORIAL: could become the definition of poset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Poset β (πΎ β Proset β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦))) | ||
Theorem | posprs 18269 | A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (πΎ β Poset β πΎ β Proset ) | ||
Theorem | posi 18270 | Lemma for poset properties. (Contributed by NM, 11-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β§ ((π β€ π β§ π β€ π) β π = π) β§ ((π β€ π β§ π β€ π) β π β€ π))) | ||
Theorem | posref 18271 | A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Poset β§ π β π΅) β π β€ π) | ||
Theorem | posasymb 18272 | A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β ((π β€ π β§ π β€ π) β π = π)) | ||
Theorem | postr 18273 | A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ π)) | ||
Theorem | 0pos 18274 | Technical lemma to simplify the statement of ipopos 18489. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 17122) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Proof shortened by AV, 13-Oct-2024.) |
β’ β β Poset | ||
Theorem | 0posOLD 18275 | Obsolete proof of 0pos 18274 as of 13-Oct-2024. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β β Poset | ||
Theorem | isposd 18276* | Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by AV, 26-Apr-2024.) |
β’ (π β πΎ β π) & β’ (π β π΅ = (BaseβπΎ)) & β’ (π β β€ = (leβπΎ)) & β’ ((π β§ π₯ β π΅) β π₯ β€ π₯) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β β’ (π β πΎ β Poset) | ||
Theorem | isposi 18277* | Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.) |
β’ πΎ β V & β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ (π₯ β π΅ β π₯ β€ π₯) & β’ ((π₯ β π΅ β§ π¦ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦)) & β’ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β β’ πΎ β Poset | ||
Theorem | isposix 18278* | Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof. (Contributed by NM, 9-Nov-2012.) (Proof shortened by AV, 30-Oct-2024.) |
β’ π΅ β V & β’ β€ β V & β’ πΎ = {β¨(Baseβndx), π΅β©, β¨(leβndx), β€ β©} & β’ (π₯ β π΅ β π₯ β€ π₯) & β’ ((π₯ β π΅ β§ π¦ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦)) & β’ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β β’ πΎ β Poset | ||
Theorem | isposixOLD 18279* | Obsolete proof of isposix 18278 as of 30-Oct-2024. Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof (Remark: That is not true - it becomes true with the new proof!). (Contributed by NM, 9-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ β V & β’ β€ β V & β’ πΎ = {β¨(Baseβndx), π΅β©, β¨(leβndx), β€ β©} & β’ (π₯ β π΅ β π₯ β€ π₯) & β’ ((π₯ β π΅ β§ π¦ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦)) & β’ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β β’ πΎ β Poset | ||
Theorem | pospropd 18280* | Posethood is determined only by structure components and only by the value of the relation within the base set. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β β’ (π β (πΎ β Poset β πΏ β Poset)) | ||
Theorem | odupos 18281 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) β β’ (π β Poset β π· β Poset) | ||
Theorem | oduposb 18282 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) β β’ (π β π β (π β Poset β π· β Poset)) | ||
Definition | df-plt 18283 | Define less-than ordering for posets and related structures. Unlike df-base 17145 and df-ple 17217, this is a derived component extractor and not an extensible structure component extractor that defines the poset. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
β’ lt = (π β V β¦ ((leβπ) β I )) | ||
Theorem | pltfval 18284 | Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ (πΎ β π΄ β < = ( β€ β I )) | ||
Theorem | pltval 18285 | Less-than relation. (df-pss 3968 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β πΆ) β (π < π β (π β€ π β§ π β π))) | ||
Theorem | pltle 18286 | "Less than" implies "less than or equal to". (pssss 4096 analog.) (Contributed by NM, 4-Dec-2011.) |
β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β πΆ) β (π < π β π β€ π)) | ||
Theorem | pltne 18287 | The "less than" relation is not reflexive. (df-pss 3968 analog.) (Contributed by NM, 2-Dec-2011.) |
β’ < = (ltβπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β πΆ) β (π < π β π β π)) | ||
Theorem | pltirr 18288 | The "less than" relation is not reflexive. (pssirr 4101 analog.) (Contributed by NM, 7-Feb-2012.) |
β’ < = (ltβπΎ) β β’ ((πΎ β π΄ β§ π β π΅) β Β¬ π < π) | ||
Theorem | pleval2i 18289 | One direction of pleval2 18290. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((π β π΅ β§ π β π΅) β (π β€ π β (π < π β¨ π = π))) | ||
Theorem | pleval2 18290 | "Less than or equal to" in terms of "less than". (sspss 4100 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β€ π β (π < π β¨ π = π))) | ||
Theorem | pltnle 18291 | "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ π < π) β Β¬ π β€ π) | ||
Theorem | pltval3 18292 | Alternate expression for the "less than" relation. (dfpss3 4087 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π < π β (π β€ π β§ Β¬ π β€ π))) | ||
Theorem | pltnlt 18293 | The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) β β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ π < π) β Β¬ π < π) | ||
Theorem | pltn2lp 18294 | The less-than relation has no 2-cycle loops. (pssn2lp 4102 analog.) (Contributed by NM, 2-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β Β¬ (π < π β§ π < π)) | ||
Theorem | plttr 18295 | The less-than relation is transitive. (psstr 4105 analog.) (Contributed by NM, 2-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β π < π)) | ||
Theorem | pltletr 18296 | Transitive law for chained "less than" and "less than or equal to". (psssstr 4107 analog.) (Contributed by NM, 2-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π β€ π) β π < π)) | ||
Theorem | plelttr 18297 | Transitive law for chained "less than or equal to" and "less than". (sspsstr 4106 analog.) (Contributed by NM, 2-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π < π) β π < π)) | ||
Theorem | pospo 18298 | Write a poset structure in terms of the proper-class poset predicate (strict less than version). (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ (πΎ β π β (πΎ β Poset β ( < Po π΅ β§ ( I βΎ π΅) β β€ ))) | ||
Definition | df-lub 18299* | Define the least upper bound (LUB) of a set of (poset) elements. The domain is restricted to exclude sets π for which the LUB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
β’ lub = (π β V β¦ ((π β π« (Baseβπ) β¦ (β©π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§)))) βΎ {π β£ β!π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§))})) | ||
Definition | df-glb 18300* | Define the greatest lower bound (GLB) of a set of (poset) elements. The domain is restricted to exclude sets π for which the GLB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
β’ glb = (π β V β¦ ((π β π« (Baseβπ) β¦ (β©π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯)))) βΎ {π β£ β!π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯))})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |