## Stream: new members

### Topic: Defining a finset with two elements {x,y}

#### Sebastian Monnet (Mar 11 2022 at 16:00):

Given terms x y : X, I would like to define the set {x, y} as a finset. Here is a mwe for a way that doesn't work and a way that works:

import field_theory.galois

example (X : Type*) (x y : X) : X :=
begin
let S := ({x, y} : finset X),
end

example (X : Type*) (x y : X) (hxy : x ≠ y): X :=
begin
let S := finset.cons x ({y} : finset X) (finset.not_mem_singleton.mpr hxy),
end


I'm pretty sure the first method worked in a previous version of mathlib, and it had the advantage of not requiring x and y to be distinct (I assume it just made the set a singleton if they were equal). Is there a way to do something equivalent to the first method in current mathlib?

#### Yaël Dillies (Mar 11 2022 at 16:01):

You're missing a [decidable_eq X] assumption in the first case.

#### Sebastian Monnet (Mar 11 2022 at 16:36):

Yaël Dillies said:

You're missing a [decidable_eq X] assumption in the first case.

Thank you!

Last updated: Dec 20 2023 at 11:08 UTC