## Stream: new members

### Topic: Finite set literals

#### Martin C. Martin (Apr 26 2023 at 17:56):

Does Lean 3 have a way to write set literals, analogous to {3, 5}?

#### Martin C. Martin (Apr 26 2023 at 17:57):

example : {3, 5} = {5, 3} := sorry gives an error.

#### Yaël Dillies (Apr 26 2023 at 18:16):

That's because it's ambiguous. Do either

example : ({3, 5} : set ℕ) = {5, 3} := sorry


or

import data.finset.basic

example : ({3, 5} : finset ℕ) = {5, 3} := sorry


depending on which one you mean.

Thanks!

#### Shreyas Srinivas (Apr 27 2023 at 09:49):

Martin C. Martin said:

Thanks!

I have found it useful to write {5, 3}.toFinset (assuming lean 4)

#### Eric Wieser (Apr 27 2023 at 09:49):

I would not recommend using that spelling

#### Eric Wieser (Apr 27 2023 at 09:50):

Yaël Dillies' suggestion above is the right spelling

#### Shreyas Srinivas (Apr 27 2023 at 09:51):

Okay. I tried this. But when I dealt with definitions or theorems on finsets and I have to use set notation, adding type annotation (on the other side of :=) seemed cumbersome.

#### Shreyas Srinivas (Apr 27 2023 at 09:52):

what are the benefits?

#### Yaël Dillies (Apr 27 2023 at 09:53):

{5, 3}.toFinset isn't simp normal form.

#### Eric Wieser (Apr 27 2023 at 09:53):

The benefits is that the resulting tem is about insert 5 (singleton 3) and not toFinset (insert 5 (singleton 3))

Last updated: Dec 20 2023 at 11:08 UTC