mathlib3

de5d0387 - feat(logic/function): comp₂ -- useful for binary operations (#993)

feat(logic/function): comp₂ -- useful for binary operations (#993) * feat(logic/function): comp₂ -- useful for binary operations For example, when working with topological groups it does not suffice to look at `mul : G → G → G`; we need to require that `G × G → G` is continuous. This lemma helps with rewriting back and forth between the curried and the uncurried versions. * Fix: we are already in the function namespace, duh * Replace comp₂ with a generalisation of bicompr * fix error in bitraversable * partially open function namespace in bitraversable