## 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: May 09 2021 at 11:09 UTC