Zulip Chat Archive

Stream: new members

Topic: Is there a built in function for function composition?


view this post on Zulip Rui Liu (Dec 09 2020 at 22:12):

Is there a built in function for function composition?

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:13):

\circ ?

view this post on Zulip Rui Liu (Dec 09 2020 at 22:14):

Right!

view this post on Zulip Rui Liu (Dec 09 2020 at 22:14):

I just found out as well!

view this post on Zulip Rui Liu (Dec 09 2020 at 22:15):

The mathlib documentation is a bit hard to use... I search composition but didn't find any.

view this post on Zulip Kenny Lau (Dec 09 2020 at 22:17):

\o is shorter, and it's function.comp

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:19):

But if you're like me, with years of latex-induced muscle memory, \circ works too :)

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 23:09):

One of the neatest things about the shortcuts is that most of the maths symbols are either the same as LaTeX, or the same as the LaTeX shortcut I usually use to define them (e.g. \Q).

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:10):

Sure, but who actually uses \McC?

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:10):

I use \Ccal

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 23:12):

yeah that's the exception. I always say to myself "MATHcal"

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:12):

OOOH! Now I'll actually remember it!

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 23:13):

Of course you can just add \Xcal to the list of shortcuts, there's just a file on github somewhere

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:14):

Yeah I learned that you can do this in your emacs config from @Jesse Michael Han

(lean-input-incorporate-changed-setting
 'lean-input-user-translations
 `( ("func" "⥤")
    ("tf" "⟨╯°□°⟩╯︵┻━┻")))

Last updated: May 12 2021 at 22:15 UTC