Constructing Types

Stream: new members

[Chase Norman]

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]

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]

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]

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