2 variables functions

Stream: maths

[Patrick Massot]

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)

[Patrick Massot]

etc.

[Patrick Massot]

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]

you will notice that even regular ∘ is rarely used

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Cue link to my blog post