Add dftermo2

[zwang123]

#4142

Proved that |- TermO = ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) ) and |- InitO = ( c e. Cat |-> ( TermO ` ( oppCat ` c ) ) ). listed right after termoid

[tirix]

Great!
Usually contributions go first into the user's Mathbox, then get moved if used elsewhere or considered worthy, but I think here it's clearly the case.

[zwang123]

Great! Usually contributions go first into the user's Mathbox, then get moved if used elsewhere or considered worthy, but I think here it's clearly the case.

I see. Actually I added dfinito3 and dftermo3 and other dependent theorems for the original proposal in #4142. Do you think I need to put it in Mathbox first?

zwang123#1

[icecream17]

I think the theorems in zwang123#1 are useful enough to not be in a mathbox

[zwang123]

I think the theorems in zwang123#1 are useful enough to not be in a mathbox

Do I merge zwang123#1 before this PR or do I create a separate PR for the third definition?

[benjub]

Congratulations on your first contribution, @zwang123 !

It's indeed important enough to skip the mathbox stage, which is the default for contributions when one needs some time to evaluate their importance (for instance, to see what later theorems use it). Here, their importance is obvious so no need for that stage.

Actually, your dftermo2 should be the "official" definition, and we may make the change in a future PR. But, as you noticed, the variable-free definition does not work for the moment because of the domains. This is something we may want to fix first (simply by changing the domains of these functions).

[david-a-wheeler]

Congratulations on your first contribution, @zwang123 !

I'd also like to give congrats to @zwang123 !! We love to have new contributors. Welcome!

[tirix]

Welcome to the very select club of set.mm contributors @zwang123 !