I don't understand `infi`

Stream: maths

[Kevin Buzzard]

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]

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

[Bhavik Mehta]

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

[Reid Barton]

infi s

[Kevin Buzzard]

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

[Yury G. Kudryashov]

You can also use ⨅ i, s i