Zulip Chat Archive

Stream: maths

Topic: 2 variables functions


view this post on Zulip 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)

view this post on Zulip Patrick Massot (Dec 15 2018 at 21:37):

etc.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 15 2018 at 23:05):

you will notice that even regular is rarely used

view this post on Zulip Mario Carneiro (Dec 15 2018 at 23:05):

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

view this post on Zulip Mario Carneiro (Dec 15 2018 at 23:06):

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

view this post on Zulip Kevin Buzzard (Dec 16 2018 at 09:58):

Cue link to my blog post


Last updated: May 09 2021 at 10:11 UTC