## Stream: general

### Topic: mem in binder

#### Patrick Massot (Jun 15 2018 at 22:46):

I wrote the code ⨅ U ∈ nhd_zero R, principal {p : R×R | p.2 - p.1 ∈ U} but now I realize I don't quite understand what's going on under the hood. The inf notation is defined by:

def infi [complete_lattice α] (s : ι → α) : α := Inf {a : α | ∃i : ι, a = s i}
notation ⨅ binders ,  r:(scoped f, infi f) := r


What is ι in my case? {U : set R // U ∈ nhd_zero R}?

#### Patrick Massot (Jun 15 2018 at 22:47):

or is it some kind of Pi type?

#### Reid Barton (Jun 15 2018 at 22:48):

It magically becomes ⨅ U, ⨅ (H : U ∈ nhd_zero R), principal {p : R×R | p.2 - p.1 ∈ U}

#### Patrick Massot (Jun 15 2018 at 22:48):

ok, this is consistent with stuff I saw

#### Reid Barton (Jun 15 2018 at 22:50):

You can even refer to H after the comma, though this seems like a bad idea to me

Thank you

#### Patrick Massot (Jun 15 2018 at 22:54):

I'm writing really strange looking code

#### Patrick Massot (Jun 15 2018 at 22:54):

I hope Johannes will help me clean it up

#### Patrick Massot (Jun 15 2018 at 23:02):

It's getting really late here. I'll give up for today. If someone else wants to play with filters while I sleep, I think the lemma I need next is:

lemma filter.mem_sets_of_mem_infi {α : Type*} {ι : Sort*} {f : ι → filter α} {A : set α} :
A ∈ (⨅ i,f i).sets → ∃ i, A ∈ (f i).sets


Last updated: Dec 20 2023 at 11:08 UTC