Zulip Chat Archive

Stream: maths

Topic: I don't understand `infi`


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?

Kevin Buzzard (May 14 2020 at 15:35):

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

Bhavik Mehta (May 14 2020 at 15:35):

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

Reid Barton (May 14 2020 at 15:35):

infi s

Kevin Buzzard (May 14 2020 at 15:35):

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

Yury G. Kudryashov (May 14 2020 at 16:06):

You can also use ⨅ i, s i


Last updated: Dec 20 2023 at 11:08 UTC