## Stream: maths

### Topic: 2 variables functions

#### Patrick Massot (Dec 15 2018 at 21:37):

Is it evil to do something like:

def function.comp₂ (f : α → β → γ) (g : γ → δ) : α → β → δ := λ  x y, g (f x y)

notation g ∘₂ f := function.comp₂ f g

def uniform_continuous₂ (f : α → β → γ) := uniform_continuous (function.uncurry f)

lemma uniform_continuous₂.comp {f : α → β → γ} {g : γ → δ}
(hf : uniform_continuous₂ f) (hg : uniform_continuous g) :
uniform_continuous₂ (g ∘₂ f)


etc.

#### Patrick Massot (Dec 15 2018 at 21:38):

It seems to be very convenient, but I fear there may be a reason why such a thing is not already used in mathlib

#### Mario Carneiro (Dec 15 2018 at 23:05):

you will notice that even regular ∘ is rarely used

#### Mario Carneiro (Dec 15 2018 at 23:05):

because it doesn't unfold as eagerly as one would like

#### Mario Carneiro (Dec 15 2018 at 23:06):

it's not particularly evil to make the definition (although you could use the crazy version (∘) ∘ (∘))

#### Kevin Buzzard (Dec 16 2018 at 09:58):

Cue link to my blog post

Last updated: May 09 2021 at 10:11 UTC