Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-07 07:49 f253fa06

View on Github →

feat(logic/basic): apply_dite2, apply_ite2 (#4050) Add variants of apply_dite and apply_ite for two-argument functions (in the case where I wanted apply_ite, the function was addition). I don't think there is any need for corresponding versions of dite_apply or ite_apply, as two-argument versions of those would be exactly the same as applying the one-argument version twice, whereas that's not the case with apply_dite2 and apply_ite2.

Estimated changes