Zulip Chat Archive

Stream: maths

Topic: I don't understand `infi`


view this post on Zulip Kevin Buzzard (May 14 2020 at 15:34):

This bit I understand:

/-- Indexed infimum -/
def infi [has_Inf α] (s : ι  α) : α := Inf (range s)

This bit, I don't at all:

notation `` binders `, ` r:(scoped f, infi f) := r

Can someone explain how to use \Glb?

view this post on Zulip Kevin Buzzard (May 14 2020 at 15:35):

If I have some s : ι → α what am I supposed to do with it?

view this post on Zulip Bhavik Mehta (May 14 2020 at 15:35):

Are you aware some people are talking to you in the twitch chat?

view this post on Zulip Reid Barton (May 14 2020 at 15:35):

infi s

view this post on Zulip Kevin Buzzard (May 14 2020 at 15:35):

But aren't I supposed to be using fancy notation?

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 16:06):

You can also use ⨅ i, s i


Last updated: May 09 2021 at 11:09 UTC