![]() |
Metamath
Proof Explorer Theorem List (p. 183 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | diag12 18201 | Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΄ = (BaseβπΆ) & β’ (π β π β π΄) & β’ πΎ = ((1st βπΏ)βπ) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΅) & β’ π½ = (Hom βπ·) & β’ 1 = (IdβπΆ) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ½π)) β β’ (π β ((π(2nd βπΎ)π)βπΉ) = ( 1 βπ)) | ||
Theorem | diag2 18202 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ π΄ = (BaseβπΆ) & β’ π΅ = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β πΉ β (ππ»π)) β β’ (π β ((π(2nd βπΏ)π)βπΉ) = (π΅ Γ {πΉ})) | ||
Theorem | diag2cl 18203 | The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ π΄ = (BaseβπΆ) & β’ π΅ = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β πΉ β (ππ»π)) & β’ π = (π· Nat πΆ) β β’ (π β (π΅ Γ {πΉ}) β (((1st βπΏ)βπ)π((1st βπΏ)βπ))) | ||
Theorem | curf2ndf 18204 | As shown in diagval 18197, the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is π₯ β πΆ β¦ (π¦ β π· β¦ π¦), which is a constant functor of the identity functor at π·. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (π· FuncCat π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β (β¨πΆ, π·β© curryF (πΆ 2ndF π·)) = ((1st β(πΞfuncπΆ))β(idfuncβπ·))) | ||
Syntax | chof 18205 | Extend class notation with the Hom functor. |
class HomF | ||
Syntax | cyon 18206 | Extend class notation with the Yoneda embedding. |
class Yon | ||
Definition | df-hof 18207* | 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 18208 | 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 18209* | 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 18210 | 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 18211 | 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 18212* | 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 18213* | 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 18214 | 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 18215 | Lemma for hofcl 18216. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (HomFβπΆ) & β’ π = (oppCatβπΆ) & β’ π· = (SetCatβπ) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΎ β (ππ»π)) & β’ (π β πΏ β (ππ»π)) & β’ (π β π β (ππ»π)) & β’ (π β π β (ππ»π)) β β’ (π β ((πΎ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(2nd βπ)β¨π, πβ©)(π(β¨π, πβ©(compβπΆ)π)πΏ)) = ((π(β¨π, πβ©(2nd βπ)β¨π, πβ©)π)(β¨(ππ»π), (ππ»π)β©(compβπ·)(ππ»π))(πΎ(β¨π, πβ©(2nd βπ)β¨π, πβ©)πΏ))) | ||
Theorem | hofcl 18216 | 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 18217 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (HomFβπ) & β’ π· = (SetCatβπ) & β’ (π β πΆ β Cat) & β’ (π β π β π) & β’ (π β ran (Homf βπΆ) β π) β β’ (π β π β ((πΆ Γc π) Func π·)) | ||
Theorem | yonval 18218 | Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (YonβπΆ) & β’ (π β πΆ β Cat) & β’ π = (oppCatβπΆ) & β’ π = (HomFβπ) β β’ (π β π = (β¨πΆ, πβ© curryF π)) | ||
Theorem | yoncl 18219 | 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 18220 | 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 18221 | 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 18222 | 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 18223 | Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ π = (YonβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ π» = (Hom βπΆ) & β’ (π β π β π΅) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ»π)) & β’ (π β πΊ β (ππ»π)) β β’ (π β ((((π(2nd βπ)π)βπΉ)βπ)βπΊ) = (πΉ(β¨π, πβ© Β· π)πΊ)) | ||
Theorem | hofpropd 18224 | 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 18225 | 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 18226 | Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (Yonβπ) & β’ π = (HomFβπΆ) & β’ (π β πΆ β Cat) β β’ (π β π = (β¨π, πΆβ© curryF π)) | ||
Theorem | oyoncl 18227 | 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 18228 | 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 18229 | Lemma for yoneda 18240. (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 18230 | Lemma for yoneda 18240. (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 18231* | Lemma for yoneda 18240. (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 18232* | Lemma for yoneda 18240. (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 18233* | Lemma for yoneda 18240. (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 18234* | Lemma for yoneda 18240. (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 18235 | Lemma for yoneda 18240. (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 18236* | Lemma for yoneda 18240. (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 18237* | Lemma for yoneda 18240. (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 18238* | 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 18239* | Lemma for yonffth 18241. (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 18240* | 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 18241 | 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 18242* | 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 18243 | Class function defining dual orders. |
class ODual | ||
Definition | df-odu 18244 |
Define the dual of an ordered structure, which replaces the order
component of the structure with its reverse. See odubas 18248, oduleval 18246,
and oduleg 18247 for its principal properties.
EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18452. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ ODual = (π€ β V β¦ (π€ sSet β¨(leβndx), β‘(leβπ€)β©)) | ||
Theorem | oduval 18245 | Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ β€ = (leβπ) β β’ π· = (π sSet β¨(leβndx), β‘ β€ β©) | ||
Theorem | oduleval 18246 | Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ β€ = (leβπ) β β’ β‘ β€ = (leβπ·) | ||
Theorem | oduleg 18247 | Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) & β’ β€ = (leβπ) & β’ πΊ = (leβπ·) β β’ ((π΄ β π β§ π΅ β π) β (π΄πΊπ΅ β π΅ β€ π΄)) | ||
Theorem | odubas 18248 | 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 18249 | Obsolete proof of odubas 18248 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 18250 | Extend class notation with the class of all prosets. |
class Proset | ||
Syntax | cdrs 18251 | Extend class notation with the class of all directed sets. |
class Dirset | ||
Definition | df-proset 18252* |
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 18253* |
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 18254* | Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Proset β (πΎ β V β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) | ||
Theorem | prslem 18255 | Lemma for prsref 18256 and prstr 18257. (Contributed by Mario Carneiro, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Proset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β§ ((π β€ π β§ π β€ π) β π β€ π))) | ||
Theorem | prsref 18256 | "Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Proset β§ π β π΅) β π β€ π) | ||
Theorem | prstr 18257 | "Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Proset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ π β€ π)) β π β€ π) | ||
Theorem | isdrs 18258* | Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Dirset β (πΎ β Proset β§ π΅ β β β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§))) | ||
Theorem | drsdir 18259* | Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Dirset β§ π β π΅ β§ π β π΅) β βπ§ β π΅ (π β€ π§ β§ π β€ π§)) | ||
Theorem | drsprs 18260 | A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (πΎ β Dirset β πΎ β Proset ) | ||
Theorem | drsbn0 18261 | The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ π΅ = (BaseβπΎ) β β’ (πΎ β Dirset β π΅ β β ) | ||
Theorem | drsdirfi 18262* | Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18253 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 18263* | 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 18264 | Extend class notation with the class of posets. |
class Poset | ||
Syntax | cplt 18265 | Extend class notation with less-than for posets. |
class lt | ||
Syntax | club 18266 | Extend class notation with poset least upper bound. |
class lub | ||
Syntax | cglb 18267 | Extend class notation with poset greatest lower bound. |
class glb | ||
Syntax | cjn 18268 | Extend class notation with poset join. |
class join | ||
Syntax | cmee 18269 | Extend class notation with poset meet. |
class meet | ||
Definition | df-poset 18270* |
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 3529 and related theorems. (Contributed by NM, 18-Oct-2012.) |
β’ Poset = {π β£ βπβπ(π = (Baseβπ) β§ π = (leβπ) β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)))} | ||
Theorem | ispos 18271* | The predicate "is a poset". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ (πΎ β Poset β (πΎ β V β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦) β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) | ||
Theorem | ispos2 18272* |
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 18273 | A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (πΎ β Poset β πΎ β Proset ) | ||
Theorem | posi 18274 | Lemma for poset properties. (Contributed by NM, 11-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β§ ((π β€ π β§ π β€ π) β π = π) β§ ((π β€ π β§ π β€ π) β π β€ π))) | ||
Theorem | posref 18275 | A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Poset β§ π β π΅) β π β€ π) | ||
Theorem | posasymb 18276 | A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β ((π β€ π β§ π β€ π) β π = π)) | ||
Theorem | postr 18277 | A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ π)) | ||
Theorem | 0pos 18278 | Technical lemma to simplify the statement of ipopos 18493. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 17126) 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 18279 | Obsolete proof of 0pos 18278 as of 13-Oct-2024. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β β Poset | ||
Theorem | isposd 18280* | 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 18281* | Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.) |
β’ πΎ β V & β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ (π₯ β π΅ β π₯ β€ π₯) & β’ ((π₯ β π΅ β§ π¦ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦)) & β’ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β β’ πΎ β Poset | ||
Theorem | isposix 18282* | 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 18283* | Obsolete proof of isposix 18282 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 18284* | 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 18285 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) β β’ (π β Poset β π· β Poset) | ||
Theorem | oduposb 18286 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
β’ π· = (ODualβπ) β β’ (π β π β (π β Poset β π· β Poset)) | ||
Definition | df-plt 18287 | Define less-than ordering for posets and related structures. Unlike df-base 17149 and df-ple 17221, 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 18288 | Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ (πΎ β π΄ β < = ( β€ β I )) | ||
Theorem | pltval 18289 | Less-than relation. (df-pss 3966 analog.) (Contributed by NM, 12-Oct-2011.) |
β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β πΆ) β (π < π β (π β€ π β§ π β π))) | ||
Theorem | pltle 18290 | "Less than" implies "less than or equal to". (pssss 4094 analog.) (Contributed by NM, 4-Dec-2011.) |
β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β πΆ) β (π < π β π β€ π)) | ||
Theorem | pltne 18291 | The "less than" relation is not reflexive. (df-pss 3966 analog.) (Contributed by NM, 2-Dec-2011.) |
β’ < = (ltβπΎ) β β’ ((πΎ β π΄ β§ π β π΅ β§ π β πΆ) β (π < π β π β π)) | ||
Theorem | pltirr 18292 | The "less than" relation is not reflexive. (pssirr 4099 analog.) (Contributed by NM, 7-Feb-2012.) |
β’ < = (ltβπΎ) β β’ ((πΎ β π΄ β§ π β π΅) β Β¬ π < π) | ||
Theorem | pleval2i 18293 | One direction of pleval2 18294. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((π β π΅ β§ π β π΅) β (π β€ π β (π < π β¨ π = π))) | ||
Theorem | pleval2 18294 | "Less than or equal to" in terms of "less than". (sspss 4098 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β€ π β (π < π β¨ π = π))) | ||
Theorem | pltnle 18295 | "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ π < π) β Β¬ π β€ π) | ||
Theorem | pltval3 18296 | Alternate expression for the "less than" relation. (dfpss3 4085 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π < π β (π β€ π β§ Β¬ π β€ π))) | ||
Theorem | pltnlt 18297 | The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) β β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ π < π) β Β¬ π < π) | ||
Theorem | pltn2lp 18298 | The less-than relation has no 2-cycle loops. (pssn2lp 4100 analog.) (Contributed by NM, 2-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β Β¬ (π < π β§ π < π)) | ||
Theorem | plttr 18299 | The less-than relation is transitive. (psstr 4103 analog.) (Contributed by NM, 2-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β π < π)) | ||
Theorem | pltletr 18300 | Transitive law for chained "less than" and "less than or equal to". (psssstr 4105 analog.) (Contributed by NM, 2-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π β€ π) β π < π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |