Zulip Chat Archive

Stream: general

Topic: mem in binder


view this post on Zulip 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}?

view this post on Zulip Patrick Massot (Jun 15 2018 at 22:47):

or is it some kind of Pi type?

view this post on Zulip 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}

view this post on Zulip Patrick Massot (Jun 15 2018 at 22:48):

ok, this is consistent with stuff I saw

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 15 2018 at 22:54):

Thank you

view this post on Zulip Patrick Massot (Jun 15 2018 at 22:54):

I'm writing really strange looking code

view this post on Zulip Patrick Massot (Jun 15 2018 at 22:54):

I hope Johannes will help me clean it up

view this post on Zulip 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: May 13 2021 at 05:21 UTC