How to initialize a Finset?

Stream: mathlib4

[ChenW]

open Set

def a : Set ℝ := Ioc 1 2
def b : Set ℝ := Ioc 2 3

def e : Finset ℕ := {1, 2}  -- works
def f : Finset (Set ℝ) := {a, b}  -- fails
def g : Finset (Set ℝ) := {Ioc 1 2, Ioc 2 3}  -- fails
def h : Finset (Set ℝ) := {Ioc 1 2}  -- works. Why?

I noticed that while I can initialize a Finset with basic types like ℕ or String, things seem to break when I try to use more complex types like Set ℝ.

• For example, e works as expected, but both f and g fail. Interestingly, h works fine when I include only one element.

Why does this happen? Is there a way to make Finset (Set ℝ) work for multiple elements?

Any insights or guidance would be greatly appreciated!

[Etienne Marion]

Writing a finset as {a, b, c} requires an docs#Insert instance for the type of a b and c. This instance exists for types with decidable equality (see docs#Finset.instInsert). However Set ℝ does not have this property (in fact neither has Set ℕ). To solve the issue, you need to open Classical at the top of the file and mark your definitions as noncomputable.

import Mathlib

open Set Classical

def a : Set ℝ := Ioc 1 2
def b : Set ℝ := Ioc 2 3

def e : Finset ℕ := {1, 2}
noncomputable def f : Finset (Set ℝ) := {a, b}
noncomputable def g : Finset (Set ℝ) := {Ioc 1 2, Ioc 2 3}
def h : Finset (Set ℝ) := {Ioc 1 2}

The last one works because there is only one element so it does not require Insert.

[Etienne Marion]

Note however that in practice open Classical at the top of a file is to be avoided because it can create issues. So in practice you should rather go for:

open Classical in
noncomputable def f : Finset (Set ℝ) := {a, b}

to open Classical only for this definition.

[Etienne Marion]

Also, note for further questions that your code is not a #mwe because it lacks imports and so does not compile in the web editor.

[Eric Wieser]

You could also use docs#Finset.cons, which both saves you using noncomputable, and is slightly easier to prove things about.

[Etienne Marion]

Ah indeed this seems better