## Stream: new members

### Topic: Constructing Types

#### Chase Norman (Dec 23 2020 at 22:06):

I have an existing fintype X. I would like to produce a Type that has all of the elements of X except a given element x. Is such a construction possible? If so, what route could I take to prove that the resulting type is a fintype? Thanks.

#### Yakov Pechersky (Dec 23 2020 at 22:26):

One simple way would be

import data.fintype.basic

variables {α : Type*} [fintype α] [decidable_eq α] {a : α}

example : fintype {x // x ≠ a} := by show_term {apply_instance}

/-
Try this: exact subtype.fintype (λ (x : α), x ≠ a)

-/


#### Yakov Pechersky (Dec 23 2020 at 22:27):

Without the decidable_eq, you don't have a decidable procedure for knowing whether two elements are the same or not, so you don't know if an element is really in your subtype.

#### Eric Wieser (Dec 23 2020 at 23:30):

But you can always use open_locale classical if you don't care about computably enumerating the values

Last updated: May 14 2021 at 21:11 UTC