Finitely Generated Sets

Stream: general

[Kevin Kuei]

Hi, I'm fairly new to Lean, and I had a question on how to define finitely generated sets. Particularly, if I want a set that is generated by (u_1, u_2, ..., u_n), how would I represent this?

[Adam Topaz]

What do you mean by "generated by"?

[Adam Topaz]

If you want a finite type of size n, you could use docs#fin .

[Adam Topaz]

We do have a #new members stream, where you might be able to get more help as a beginner.

[Patrick Johnson]

{x, y, z} is the finite set that contains only elements x, y and z. Is this what you mean by "generated by"?