> but why?

Why not? I was curious, Haskell is the functional language I know. Lean is the language I do not know.

Since Lean leans even heavier towards mathematics, set builder style notation seems like a natural fit. Now whether or not such notation is actually needed or worth it, that is a whole different question.