Projection of set

Stream: new members

[Andre Hernandez-Espiet (Rutgers)]

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]

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)]

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

[Thomas Browning]

docs#finite.exists_max might be helpful

[Kevin Buzzard]

What if S is empty?

[Andre Hernandez-Espiet (Rutgers)]

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