mem in binder

Stream: general

[Patrick Massot]

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]

or is it some kind of Pi type?

[Reid Barton]

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

[Patrick Massot]

ok, this is consistent with stuff I saw

[Reid Barton]

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

[Patrick Massot]

Thank you

[Patrick Massot]

I'm writing really strange looking code

[Patrick Massot]

I hope Johannes will help me clean it up

[Patrick Massot]

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