Zulip Chat Archive

Stream: new members

Topic: Projection of set

Andre Hernandez-Espiet (Rutgers) (Sep 15 2022 at 15:47):

How do I access the projection of a set in lean? More specifically, say I have S: set(ℝ×ℝ), then how do I get all the first or second coordinates?

Kyle Miller (Sep 15 2022 at 15:51):

You could do prod.fst '' S or prod.snd '' S to respectively get the first or second coordinates. The '' notation is for docs#set.image

Andre Hernandez-Espiet (Rutgers) (Sep 15 2022 at 15:56):

Hmm, interesting. What if I additionally have Sfin: S.finite and want to find the maximum first coordinate?

Thomas Browning (Sep 15 2022 at 15:59):

docs#finite.exists_max might be helpful

Kevin Buzzard (Sep 16 2022 at 08:56):

What if S is empty?

Andre Hernandez-Espiet (Rutgers) (Sep 16 2022 at 19:55):

That is a good point, so we should also assume it's non-empty.

Last updated: Dec 20 2023 at 11:08 UTC