Finset.Nonempty

Stream: general

[Bolton Bailey]

From the docstring of docs#Finset.Nonempty:

The property s.Nonempty expresses the fact that the finset s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

Not sure if I get the rationale here. Wouldn't I rather the assumption just be s ≠ ∅ so I can do intro s_empty ; rw [s_empty] at *?

[Sebastien Gouezel]

Yet another way to formulate the assumption would be (h : ∃ a, a ∈ s). Or have the a explicit in (a : α) (ha : a ∈ s). In mathlib early days, we were jumping between these different formulations (and their negations to say that the set is empty) and it was quite painful. So we decided instead to standardize on the form s.Nonempty and to implement enough API that, from this one, everything would be readily available through dot notation -- this is the advantage of a new definition. This is just a convention, but it turned out to be extremely efficient and convenient.