## Stream: new members

### Topic: decidable disjoint

#### Bhavik Mehta (Dec 11 2019 at 13:13):

When I write:

import data.finset
import data.fintype

open fintype
open finset

variable {n : ℕ}
local notation X := fin n

variable {𝒜 : finset (finset X)}

def compress (U V : finset X) (A : finset X) :=
if (disjoint U A) ∧ (V ⊆ A)
then (A ∪ U) \ V
else A


I get an error saying "failed to synthesize type class instance" for "decidable (disjoint U A ∧ V ⊆ A)", but if I rewrite the condition with U ∩ A = ∅, it's fine... I'd like to keep the definition with disjoint though, since every time I use this definition I found myself converting the empty intersection to disjointness. How could I get around this?

#### Bhavik Mehta (Dec 11 2019 at 14:10):

I proved disjoint U V is decidable instead... Is there a reason this isn't already in data/finset.lean?

#### Simon Hudon (Dec 12 2019 at 01:39):

There's no reason not to have it in mathlib. People tend to add what they use so that might just never have come up before

#### Bhavik Mehta (Dec 12 2019 at 13:20):

Okay! Is there an issue with typeclass resolution, since this is saying disjoint on finsets is decidable, but might not be in other cases?

#### Simon Hudon (Dec 12 2019 at 19:38):

With decidable equality on α, disjointness on finset should always be decidable.

Last updated: May 14 2021 at 00:42 UTC