File tree Expand file tree Collapse file tree 1 file changed +3
-2
lines changed Expand file tree Collapse file tree 1 file changed +3
-2
lines changed Original file line number Diff line number Diff line change @@ -835625,8 +835625,9 @@ have GLB (expanded version). (Contributed by Zhi Wang,
835625
835625
RPUOUSRSLUTUQOTRKUQVASKUQQUTUTVBUORSFVCUQUTVDABCDEFGHIJKLMNOPQRSTUOUAUB
835626
835626
UCUDUEUFUGUHUIUJUKULUMUNVEVF $.
835627
835627
835628
- $( A universal property defines an essentially unique (strong form)
835629
- object if it exists. (Contributed by Zhi Wang, 19-Sep-2025.) $)
835628
+ $( A universal property defines an essentially unique (strong form) pair
835629
+ of object ` X ` and morphism ` M ` if it exists. (Contributed by Zhi
835630
+ Wang, 19-Sep-2025.) $)
835630
835631
upeu $p |- ( ph -> E! r e. ( X ( Iso ` D ) Y )
835631
835632
N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $=
835632
835633
( cv co cfv cop wceq ciso wrex wrmo wreu ccic wbr upciclem3 simprd eqid
You can’t perform that action at this time.
0 commit comments