mathlib
f253fa06 - feat(logic/basic): apply_dite2, apply_ite2 (#4050)

Commit
6 years ago
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`.
Author
Parents
Loading